let X be set ; :: thesis: for A being Ordinal st X in Rank A holds
union X in Rank A
let A be Ordinal; :: thesis: ( X in Rank A implies union X in Rank A )
assume A1: X in Rank A ; :: thesis: union X in Rank A
A2: now :: thesis: ( ex B being Ordinal st A = succ B implies union X in Rank A )
given B being Ordinal such that A3: A = succ B ; :: thesis: union X in Rank A
A4: union X c= union (Rank B) by ZFMISC_1:77, A1, A3, Th32;
union (Rank B) c= Rank B by Th34;
hence union X in Rank A by A3, Th32, A4, XBOOLE_1:1; :: thesis: verum
end;
now :: thesis: ( A <> {} & ( for B being Ordinal holds A <> succ B ) implies union X in Rank A )
assume that
A5: A <> {} and
A6: for B being Ordinal holds A <> succ B ; :: thesis: union X in Rank A
A7: A is limit_ordinal by A6, ORDINAL1:29;
then consider B being Ordinal such that
A8: B in A and
A9: X in Rank B by A1, A5, Th31;
A10: union X c= union (Rank B) by ZFMISC_1:77, A9, ORDINAL1:def 2;
A11: union (Rank B) c= Rank B by Th34;
succ B <> A by A6;
then A12: succ B c< A by A8, ORDINAL1:21;
A13: union X in Rank (succ B) by A11, Th32, A10, XBOOLE_1:1;
succ B in A by A12, ORDINAL1:11;
hence union X in Rank A by A7, A13, Th31; :: thesis: verum
end;
hence union X in Rank A by A1, A2, Lm2; :: thesis: verum