let x be set ; :: thesis: ( x is ordinal implies ( union x is epsilon-transitive & union x is epsilon-connected ) )
assume x is ordinal ; :: thesis: ( union x is epsilon-transitive & union x is epsilon-connected )
then reconsider A = x as Ordinal ;
thus for y being set st y in union x holds
y c= union x :: according to ORDINAL1:def 2 :: thesis: union x is epsilon-connected
proof
let y be set ; :: thesis: ( y in union x implies y c= union x )
assume y in union x ; :: thesis: y c= union x
then consider z being set such that
A1: y in z and
A2: z in x by TARSKI:def 4;
z in A by A2;
then reconsider z = z as Ordinal by Th9;
z c= A by A2, Def2;
hence y c= union x by A1, ZFMISC_1:74; :: thesis: verum
end;
let y be set ; :: according to ORDINAL1:def 3 :: thesis: for y being set st y in union x & y in union x & not y in y & not y = y holds
y in y
let z be set ; :: thesis: ( y in union x & z in union x & not y in z & not y = z implies z in y )
assume that
A3: y in union x and
A4: z in union x ; :: thesis: ( y in z or y = z or z in y )
consider X being set such that
A5: y in X and
A6: X in x by A3, TARSKI:def 4;
A7: X in A by A6;
consider Y being set such that
A8: z in Y and
A9: Y in x by A4, TARSKI:def 4;
reconsider X = X, Y = Y as Ordinal by A9, A7, Th9;
z in Y by A8;
then A10: z is Ordinal by Th9;
y in X by A5;
then y is Ordinal by Th9;
hence ( y in z or y = z or z in y ) by A10, Th10; :: thesis: verum