let fi be Ordinal-Sequence; :: thesis: for W being Universe st dom fi in W & rng fi c= W holds
sup fi in W
let W be Universe; :: thesis: ( dom fi in W & rng fi c= W implies sup fi in W )
assume that
A1: dom fi in W and
A2: rng fi c= W ; :: thesis: sup fi in W
ex A being Ordinal st rng fi c= A by ORDINAL2:def 4;
then for x being object st x in rng fi holds
x is Ordinal ;
then reconsider B = union (rng fi) as epsilon-transitive epsilon-connected set by ORDINAL1:23;
A3: rng fi = fi .: (dom fi) by RELAT_1:113;
A4: sup fi c= succ B
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in sup fi or x in succ B )
assume A5: x in sup fi ; :: thesis: x in succ B
then reconsider A = x as Ordinal ;
consider C being Ordinal such that
A6: C in rng fi and
A7: A c= C by A5, ORDINAL2:21;
C c= union (rng fi) by A6, ZFMISC_1:74;
then A c= B by A7;
hence x in succ B by ORDINAL1:22; :: thesis: verum
end;
card (dom fi) in card W by A1, CLASSES2:1;
then card (rng fi) in card W by A3, CARD_1:67, ORDINAL1:12;
then rng fi in W by A2, CLASSES1:1;
then union (rng fi) in W by CLASSES2:59;
then succ B in W by CLASSES2:5;
hence sup fi in W by A4, CLASSES1:def 1; :: thesis: verum