let Y, X be set ; :: thesis: for A being Ordinal holds
( Y in Tarski-Class X,(succ A) iff ( ( Y c= Tarski-Class X,A & Y in Tarski-Class X ) or ex Z being set st
( Z in Tarski-Class X,A & ( Y c= Z or Y = bool Z ) ) ) )
let A be Ordinal; :: thesis: ( Y in Tarski-Class X,(succ A) iff ( ( Y c= Tarski-Class X,A & Y in Tarski-Class X ) or ex Z being set st
( Z in Tarski-Class X,A & ( Y c= Z or Y = bool Z ) ) ) )
set T1 = { u where u is Element of Tarski-Class X : ex v being Element of Tarski-Class X st
( v in Tarski-Class X,A & u c= v ) } ;
set T2 = { (bool v) where v is Element of Tarski-Class X : v in Tarski-Class X,A } ;
set T3 = (bool (Tarski-Class X,A)) /\ (Tarski-Class X);
A1: Tarski-Class X,(succ A) = ({ u where u is Element of Tarski-Class X : ex v being Element of Tarski-Class X st
( v in Tarski-Class X,A & u c= v ) } \/ { (bool v) where v is Element of Tarski-Class X : v in Tarski-Class X,A } ) \/ ((bool (Tarski-Class X,A)) /\ (Tarski-Class X)) by Lm1;
thus ( not Y in Tarski-Class X,(succ A) or ( Y c= Tarski-Class X,A & Y in Tarski-Class X ) or ex Z being set st
( Z in Tarski-Class X,A & ( Y c= Z or Y = bool Z ) ) ) :: thesis: ( ( ( Y c= Tarski-Class X,A & Y in Tarski-Class X ) or ex Z being set st
( Z in Tarski-Class X,A & ( Y c= Z or Y = bool Z ) ) ) implies Y in Tarski-Class X,(succ A) )
proof
assume Y in Tarski-Class X,(succ A) ; :: thesis: ( ( Y c= Tarski-Class X,A & Y in Tarski-Class X ) or ex Z being set st
( Z in Tarski-Class X,A & ( Y c= Z or Y = bool Z ) ) )
then A2: ( Y in { u where u is Element of Tarski-Class X : ex v being Element of Tarski-Class X st
( v in Tarski-Class X,A & u c= v ) } \/ { (bool v) where v is Element of Tarski-Class X : v in Tarski-Class X,A } or Y in (bool (Tarski-Class X,A)) /\ (Tarski-Class X) ) by A1, XBOOLE_0:def 3;
A3: now
assume Y in { u where u is Element of Tarski-Class X : ex v being Element of Tarski-Class X st
( v in Tarski-Class X,A & u c= v ) } ; :: thesis: ex Z being set st
( Z in Tarski-Class X,A & ( Y c= Z or Y = bool Z ) )
then ex u being Element of Tarski-Class X st
( Y = u & ex v being Element of Tarski-Class X st
( v in Tarski-Class X,A & u c= v ) ) ;
hence ex Z being set st
( Z in Tarski-Class X,A & ( Y c= Z or Y = bool Z ) ) ; :: thesis: verum
end;
A4: now
assume Y in { (bool v) where v is Element of Tarski-Class X : v in Tarski-Class X,A } ; :: thesis: ex Z being set st
( Z in Tarski-Class X,A & ( Y c= Z or Y = bool Z ) )
then ex v being Element of Tarski-Class X st
( Y = bool v & v in Tarski-Class X,A ) ;
hence ex Z being set st
( Z in Tarski-Class X,A & ( Y c= Z or Y = bool Z ) ) ; :: thesis: verum
end;
now
assume Y in (bool (Tarski-Class X,A)) /\ (Tarski-Class X) ; :: thesis: ( ( Y c= Tarski-Class X,A & Y in Tarski-Class X ) or ex Z being set st
( Z in Tarski-Class X,A & ( Y c= Z or Y = bool Z ) ) )
then ( Y in bool (Tarski-Class X,A) & Y in Tarski-Class X ) by XBOOLE_0:def 4;
hence ( ( Y c= Tarski-Class X,A & Y in Tarski-Class X ) or ex Z being set st
( Z in Tarski-Class X,A & ( Y c= Z or Y = bool Z ) ) ) ; :: thesis: verum
end;
hence ( ( Y c= Tarski-Class X,A & Y in Tarski-Class X ) or ex Z being set st
( Z in Tarski-Class X,A & ( Y c= Z or Y = bool Z ) ) ) by A2, A3, A4, XBOOLE_0:def 3; :: thesis: verum
end;
assume A5: ( ( Y c= Tarski-Class X,A & Y in Tarski-Class X ) or ex Z being set st
( Z in Tarski-Class X,A & ( Y c= Z or Y = bool Z ) ) ) ; :: thesis: Y in Tarski-Class X,(succ A)
A6: now
assume ( Y c= Tarski-Class X,A & Y in Tarski-Class X ) ; :: thesis: Y in Tarski-Class X,(succ A)
then Y in (bool (Tarski-Class X,A)) /\ (Tarski-Class X) by XBOOLE_0:def 4;
hence Y in Tarski-Class X,(succ A) by A1, XBOOLE_0:def 3; :: thesis: verum
end;
now
given Z being set such that A7: ( Z in Tarski-Class X,A & ( Y c= Z or Y = bool Z ) ) ; :: thesis: Y in Tarski-Class X,(succ A)
reconsider Z = Z as Element of Tarski-Class X by A7;
reconsider y = Y as Element of Tarski-Class X by A7, Th6, Th7;
A8: now
assume Y c= Z ; :: thesis: Y in Tarski-Class X,(succ A)
then y in { u where u is Element of Tarski-Class X : ex v being Element of Tarski-Class X st
( v in Tarski-Class X,A & u c= v ) } by A7;
then Y in { u where u is Element of Tarski-Class X : ex v being Element of Tarski-Class X st
( v in Tarski-Class X,A & u c= v ) } \/ { (bool v) where v is Element of Tarski-Class X : v in Tarski-Class X,A } by XBOOLE_0:def 3;
hence Y in Tarski-Class X,(succ A) by A1, XBOOLE_0:def 3; :: thesis: verum
end;
now
assume Y = bool Z ; :: thesis: Y in Tarski-Class X,(succ A)
then y in { (bool v) where v is Element of Tarski-Class X : v in Tarski-Class X,A } by A7;
then Y in { u where u is Element of Tarski-Class X : ex v being Element of Tarski-Class X st
( v in Tarski-Class X,A & u c= v ) } \/ { (bool v) where v is Element of Tarski-Class X : v in Tarski-Class X,A } by XBOOLE_0:def 3;
hence Y in Tarski-Class X,(succ A) by A1, XBOOLE_0:def 3; :: thesis: verum
end;
hence Y in Tarski-Class X,(succ A) by A7, A8; :: thesis: verum
end;
hence Y in Tarski-Class X,(succ A) by A5, A6; :: thesis: verum