let X be set ; :: thesis: ( X is epsilon-transitive implies for A being Ordinal st A <> {} holds
Tarski-Class (X,A) is epsilon-transitive )
assume A1: for Y being set st Y in X holds
Y c= X ; :: according to ORDINAL1:def 2 :: thesis: for A being Ordinal st A <> {} holds
Tarski-Class (X,A) is epsilon-transitive
defpred S1[ Ordinal] means ( $1 <> {} implies Tarski-Class (X,$1) is epsilon-transitive );
A2: for A being Ordinal st ( for B being Ordinal st B in A holds
S1[B] ) holds
S1[A]
proof
let A be Ordinal; :: thesis: ( ( for B being Ordinal st B in A holds
S1[B] ) implies S1[A] )
assume that
A3: for B being Ordinal st B in A holds
S1[B] and
A4: A <> {} ; :: thesis: Tarski-Class (X,A) is epsilon-transitive
let Y be set ; :: according to ORDINAL1:def 2 :: thesis: ( not Y in Tarski-Class (X,A) or Y c= Tarski-Class (X,A) )
assume A5: Y in Tarski-Class (X,A) ; :: thesis: Y c= Tarski-Class (X,A)
A6: now :: thesis: ( ex B being Ordinal st A = succ B implies Y c= Tarski-Class (X,A) )
given B being Ordinal such that A7: A = succ B ; :: thesis: Y c= Tarski-Class (X,A)
A8: B c= A by ORDINAL1:6, ORDINAL1:def 2, A7;
A9: S1[B] by A3, A7, ORDINAL1:6;
A10: Tarski-Class (X,B) c= Tarski-Class (X,A) by A8, Th16;
now :: thesis: ( not Y c= Tarski-Class (X,B) implies Y c= Tarski-Class (X,A) )
assume not Y c= Tarski-Class (X,B) ; :: thesis: Y c= Tarski-Class (X,A)
then consider Z being set such that
A11: Z in Tarski-Class (X,B) and
A12: ( Y c= Z or Y = bool Z ) by A5, A7, Th10;
A13: ( Y = bool Z implies Y c= Tarski-Class (X,A) ) by A7, A11, Th10;
now :: thesis: ( Y c= Z implies Y c= Tarski-Class (X,A) )
assume A14: Y c= Z ; :: thesis: Y c= Tarski-Class (X,A)
thus Y c= Tarski-Class (X,A) :: thesis: verum
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Y or x in Tarski-Class (X,A) )
reconsider xx = x as set by TARSKI:1;
assume A15: x in Y ; :: thesis: x in Tarski-Class (X,A)
then A16: x in Z by A14;
A17: now :: thesis: ( B = {} implies x in Tarski-Class (X,A) )
assume B = {} ; :: thesis: x in Tarski-Class (X,A)
then Tarski-Class (X,B) = {X} by Lm1;
then Z = X by A11, TARSKI:def 1;
hence x in Tarski-Class (X,A) by A7, A11, Th10, A1, A14, A15; :: thesis: verum
end;
hence x in Tarski-Class (X,A) by A17; :: thesis: verum
end;
end;
hence Y c= Tarski-Class (X,A) by A12, A13; :: thesis: verum
end;
hence Y c= Tarski-Class (X,A) by A10; :: thesis: verum
end;
now :: thesis: ( ( for B being Ordinal holds A <> succ B ) implies Y c= Tarski-Class (X,A) )
assume A18: for B being Ordinal holds A <> succ B ; :: thesis: Y c= Tarski-Class (X,A)
then A is limit_ordinal by ORDINAL1:29;
then consider B being Ordinal such that
A19: B in A and
A20: Y in Tarski-Class (X,B) by A4, A5, Th13;
A21: succ B <> A by A18;
A22: Tarski-Class (X,B) c= Tarski-Class (X,(succ B)) by Th15;
A23: succ B c< A by A19, ORDINAL1:21, A21;
A24: Tarski-Class (X,(succ B)) c= Tarski-Class (X,A) by A19, ORDINAL1:21, Th16;
Tarski-Class (X,(succ B)) is epsilon-transitive by A3, A23, ORDINAL1:11;
then Y c= Tarski-Class (X,(succ B)) by A20, A22;
hence Y c= Tarski-Class (X,A) by A24; :: thesis: verum
end;
hence Y c= Tarski-Class (X,A) by A6; :: thesis: verum
end;
thus for A being Ordinal holds S1[A] from ORDINAL1:sch 2(A2); :: thesis: verum