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 A2: 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 ) ) )
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, A2, XBOOLE_0:def 3;
A4: now
assume A5: 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 ) )
A6: 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 ) ) by A5;
thus ex Z being set st
( Z in Tarski-Class X,A & ( Y c= Z or Y = bool Z ) ) by A6; :: thesis: verum
end;
A7: now
assume A8: 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 ) )
A9: ex v being Element of Tarski-Class X st
( Y = bool v & v in Tarski-Class X,A ) by A8;
thus ex Z being set st
( Z in Tarski-Class X,A & ( Y c= Z or Y = bool Z ) ) by A9; :: thesis: verum
end;
A10: now
assume A11: 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 ) ) )
A12: Y in bool (Tarski-Class X,A) by A11, XBOOLE_0:def 4;
thus ( ( 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 A11, A12, XBOOLE_0:def 4; :: thesis: verum
end;
thus ( ( 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, A10, 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 A15: ( Y c= Tarski-Class X,A & Y in Tarski-Class X ) ; :: thesis: Y in Tarski-Class X,(succ A)
A16: Y in (bool (Tarski-Class X,A)) /\ (Tarski-Class X) by A15, XBOOLE_0:def 4;
thus Y in Tarski-Class X,(succ A) by A1, A16, XBOOLE_0:def 3; :: thesis: verum
end;
A17: 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 A21: Y c= Z ; :: thesis: Y in Tarski-Class X,(succ A)
A22: 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, A21;
A23: 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 A22, XBOOLE_0:def 3;
thus Y in Tarski-Class X,(succ A) by A1, A23, XBOOLE_0:def 3; :: thesis: verum
end;
A24: now
assume A25: Y = bool Z ; :: thesis: Y in Tarski-Class X,(succ A)
A26: y in { (bool v) where v is Element of Tarski-Class X : v in Tarski-Class X,A } by A18, A25;
A27: 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 A26, XBOOLE_0:def 3;
thus Y in Tarski-Class X,(succ A) by A1, A27, XBOOLE_0:def 3; :: thesis: verum
end;
thus Y in Tarski-Class X,(succ A) by A19, A20, A24; :: thesis: verum
end;
thus Y in Tarski-Class X,(succ A) by A13, A14, A17; :: thesis: verum