let L be Sequence; :: thesis: ( dom L is limit_ordinal & ( for A being Ordinal st A in dom L holds
L . A = Rank A ) implies Rank (dom L) = Union L )
assume that
A1: dom L is limit_ordinal and
A2: for A being Ordinal st A in dom L holds
L . A = Rank A ; :: thesis: Rank (dom L) = Union L
A3: union (rng L) = Union L by CARD_3:def 4;
now :: thesis: ( dom L <> {} implies ( Rank (dom L) c= Union L & Union L c= Rank (dom L) ) )
assume A4: dom L <> {} ; :: thesis: ( Rank (dom L) c= Union L & Union L c= Rank (dom L) )
thus Rank (dom L) c= Union L :: thesis: Union L c= Rank (dom L)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Rank (dom L) or x in Union L )
assume x in Rank (dom L) ; :: thesis: x in Union L
then consider A being Ordinal such that
A5: A in dom L and
A6: x in Rank A by A1, A4, CLASSES1:31;
L . A = Rank A by A2, A5;
then Rank A in rng L by A5, FUNCT_1:def 3;
hence x in Union L by A3, A6, TARSKI:def 4; :: thesis: verum
end;
thus Union L c= Rank (dom L) :: thesis: verum
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Union L or x in Rank (dom L) )
assume x in Union L ; :: thesis: x in Rank (dom L)
then consider X being set such that
A7: x in X and
A8: X in rng L by A3, TARSKI:def 4;
consider y being object such that
A9: y in dom L and
A10: X = L . y by A8, FUNCT_1:def 3;
reconsider y = y as Ordinal by A9;
X = Rank y by A2, A9, A10;
hence x in Rank (dom L) by A1, A7, A9, CLASSES1:31; :: thesis: verum
end;
end;
hence Rank (dom L) = Union L by A3, CLASSES1:29, RELAT_1:42, ZFMISC_1:2; :: thesis: verum