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

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

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

card (dom fi) in card W
by A1, CLASSES2:1;
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;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

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