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