let X be set ; for A being Ordinal st A <> {} & A is limit_ordinal holds
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) ) }
let A be Ordinal; ( A <> {} & A is limit_ordinal implies 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) ) } )
assume A1:
( A <> {} & A is limit_ordinal )
; 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) ) }
deffunc H1( Ordinal) -> Subset of (Tarski-Class X) = Tarski-Class (X,$1);
consider L being Sequence such that
A2:
( dom L = A & ( for B being Ordinal st B in A holds
L . B = H1(B) ) )
from ORDINAL2:sch 2();
A3:
Tarski-Class (X,A) = (union (rng L)) /\ (Tarski-Class X)
by A1, A2, Lm1;
thus
Tarski-Class (X,A) c= { u where u is Element of Tarski-Class X : ex B being Ordinal st
( B in A & u in Tarski-Class (X,B) ) }
XBOOLE_0:def 10 { u where u is Element of Tarski-Class X : ex B being Ordinal st
( B in A & u in Tarski-Class (X,B) ) } c= Tarski-Class (X,A)proof
let x be
object ;
TARSKI:def 3 ( not x in Tarski-Class (X,A) or x in { u where u is Element of Tarski-Class X : ex B being Ordinal st
( B in A & u in Tarski-Class (X,B) ) } )
assume
x in Tarski-Class (
X,
A)
;
x in { u where u is Element of Tarski-Class X : ex B being Ordinal st
( B in A & u in Tarski-Class (X,B) ) }
then
x in union (rng L)
by A3, XBOOLE_0:def 4;
then consider Y being
set such that A4:
x in Y
and A5:
Y in rng L
by TARSKI:def 4;
consider y being
object such that A6:
y in dom L
and A7:
Y = L . y
by A5, FUNCT_1:def 3;
reconsider y =
y as
Ordinal by A6;
Y = Tarski-Class (
X,
y)
by A2, A6, A7;
hence
x in { u where u is Element of Tarski-Class X : ex B being Ordinal st
( B in A & u in Tarski-Class (X,B) ) }
by A2, A4, A6;
verum
end;
let x be object ; TARSKI:def 3 ( not x in { u where u is Element of Tarski-Class X : ex B being Ordinal st
( B in A & u in Tarski-Class (X,B) ) } or x in Tarski-Class (X,A) )
assume
x in { u where u is Element of Tarski-Class X : ex B being Ordinal st
( B in A & u in Tarski-Class (X,B) ) }
; x in Tarski-Class (X,A)
then consider u being Element of Tarski-Class X such that
A8:
x = u
and
A9:
ex B being Ordinal st
( B in A & u in Tarski-Class (X,B) )
;
consider B being Ordinal such that
A10:
B in A
and
A11:
u in Tarski-Class (X,B)
by A9;
L . B = Tarski-Class (X,B)
by A2, A10;
then
Tarski-Class (X,B) in rng L
by A2, A10, FUNCT_1:def 3;
then
u in union (rng L)
by A11, TARSKI:def 4;
hence
x in Tarski-Class (X,A)
by A3, A8, XBOOLE_0:def 4; verum