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 A3: ( 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;
A4: 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;
A7: 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;
( not Y in (bool (Tarski-Class X,A)) /\ (Tarski-Class X) 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 ) ) ) 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 ) ) ) by A3, A4, A7, XBOOLE_0:def 3; :: thesis: verum
end;
assume A13: ( ( 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)
A14: 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 A18: Z in Tarski-Class X,A and
A19: ( 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 A18;
reconsider y = Y as Element of Tarski-Class X by A18, A19, Th6, Th7;
A20: 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 A18;
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 A18;
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 A19, A20; :: thesis: verum
end;
hence Y in Tarski-Class X,(succ A) by A13, A14; :: thesis: verum