let X, x be set ; :: thesis: for A being Ordinal st A <> {} & A is limit_ordinal holds
( x in Tarski-Class (X,A) iff ex B being Ordinal st
( B in A & x in Tarski-Class (X,B) ) )
let A be Ordinal; :: thesis: ( A <> {} & A is limit_ordinal implies ( x in Tarski-Class (X,A) iff ex B being Ordinal st
( B in A & x in Tarski-Class (X,B) ) ) )
assume A1: ( A <> {} & A is limit_ordinal ) ; :: thesis: ( x in Tarski-Class (X,A) iff ex B being Ordinal st
( B in A & x in Tarski-Class (X,B) ) )
then A2: Tarski-Class (X,A) = { u where u is Element of Tarski-Class X : ex B being Ordinal st
( B in A & u in Tarski-Class (X,B) ) } by Th9;
thus ( x in Tarski-Class (X,A) implies ex B being Ordinal st
( B in A & x in Tarski-Class (X,B) ) ) :: thesis: ( ex B being Ordinal st
( B in A & x in Tarski-Class (X,B) ) implies x in Tarski-Class (X,A) )
proof
assume x in Tarski-Class (X,A) ; :: thesis: ex B being Ordinal st
( B in A & x in Tarski-Class (X,B) )
then ex u being Element of Tarski-Class X st
( x = u & ex B being Ordinal st
( B in A & u in Tarski-Class (X,B) ) ) by A2;
hence ex B being Ordinal st
( B in A & x in Tarski-Class (X,B) ) ; :: thesis: verum
end;
given B being Ordinal such that A3: B in A and
A4: x in Tarski-Class (X,B) ; :: thesis: x in Tarski-Class (X,A)
reconsider u = x as Element of Tarski-Class X by A4;
u in { v where v is Element of Tarski-Class X : ex B being Ordinal st
( B in A & v in Tarski-Class (X,B) ) } by A3, A4;
hence x in Tarski-Class (X,A) by A1, Th9; :: thesis: verum