let X, Y 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 :: thesis: ( 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 ) } implies ex Z being set st
( Z in Tarski-Class (X,A) & ( Y c= Z or Y = bool Z ) ) )
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;
now :: thesis: ( Y in { (bool v) where v is Element of Tarski-Class X : v in Tarski-Class (X,A) } implies ex Z being set st
( Z in Tarski-Class (X,A) & ( Y c= Z or Y = bool Z ) ) )
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;
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, XBOOLE_0:def 3, XBOOLE_0:def 4; :: thesis: verum
end;
assume A4: ( ( 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))
A5: now :: thesis: ( Y c= Tarski-Class (X,A) & Y in Tarski-Class X implies Y in Tarski-Class (X,(succ A)) )
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 :: thesis: ( 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)) )
given Z being set such that A6: Z in Tarski-Class (X,A) and
A7: ( 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 A6;
reconsider y = Y as Element of Tarski-Class X by A6, A7, Th3, Th4;
A8: now :: thesis: ( Y c= Z implies Y in Tarski-Class (X,(succ A)) )
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 A6;
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 :: thesis: ( Y = bool Z implies Y in Tarski-Class (X,(succ A)) )
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 A6;
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 A4, A5; :: thesis: verum