environ
vocabularies HIDDEN, FUNCT_1, TARSKI, ZFMISC_1, SETFAM_1, XBOOLE_0, CARD_1, SUBSET_1, ORDINAL1, ORDINAL2, RELAT_1, FUNCT_2, CLASSES1, NAT_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1, FUNCT_2, CARD_1, ORDINAL1, MCART_1, ORDINAL2;
definitions ORDINAL1, TARSKI, WELLORD2, FUNCT_1, XBOOLE_0, RELAT_1;
theorems TARSKI, SETFAM_1, ZFMISC_1, ORDINAL1, FUNCT_1, CARD_1, WELLORD2, ENUMSET1, XBOOLE_0, XBOOLE_1, ORDINAL2, RELAT_1, FUNCT_2, XTUPLE_0;
schemes ORDINAL1, ORDINAL2, TARSKI, PARTFUN1, XBOOLE_0, FUNCT_1, XFAMILY;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, FUNCT_1, FUNCT_2, RELSET_1, RELAT_1;
constructors HIDDEN, SETFAM_1, MCART_1, WELLORD2, ORDINAL2, CARD_1, FUNCT_2, RELSET_1;
requirements HIDDEN, SUBSET, BOOLE, NUMERALS;
equalities ORDINAL1, TARSKI, RELAT_1;
expansions ORDINAL1, TARSKI, FUNCT_1, XBOOLE_0;
Lm1:
now for X being set holds
( H1( 0 ) = {X} & ( for A being Ordinal holds H1( succ A) = H2(A,H1(A)) ) & ( for A being Ordinal
for L being Sequence st A <> 0 & A is limit_ordinal & dom L = A & ( for B being Ordinal st B in A holds
L . B = Tarski-Class (X,B) ) holds
Tarski-Class (X,A) = (union (rng L)) /\ (Tarski-Class X) ) )
let X be
set ;
( H1( 0 ) = {X} & ( for A being Ordinal holds H1( succ A) = H2(A,H1(A)) ) & ( for A being Ordinal
for L being Sequence st A <> 0 & A is limit_ordinal & dom L = A & ( for B being Ordinal st B in A holds
L . B = Tarski-Class (X,B) ) holds
Tarski-Class (X,A) = (union (rng L)) /\ (Tarski-Class X) ) )deffunc H1(
Ordinal)
-> set =
Tarski-Class (
X,$1);
deffunc H2(
Ordinal,
set )
-> set =
( { u where u is Element of Tarski-Class X : ex v being Element of Tarski-Class X st
( v in $2 & u c= v ) } \/ { (bool v) where v is Element of Tarski-Class X : v in $2 } ) \/ ((bool $2) /\ (Tarski-Class X));
deffunc H3(
Ordinal,
Sequence)
-> set =
(union (rng $2)) /\ (Tarski-Class X);
A1:
for
A being
Ordinal for
x being
object holds
(
x = H1(
A) iff ex
L being
Sequence st
(
x = last L &
dom L = succ A &
L . 0 = {X} & ( for
C being
Ordinal st
succ C in succ A holds
L . (succ C) = H2(
C,
L . C) ) & ( for
C being
Ordinal st
C in succ A &
C <> 0 &
C is
limit_ordinal holds
L . C = H3(
C,
L | C) ) ) )
by Def5;
thus
H1(
0 )
= {X}
from ORDINAL2:sch 8(A1); ( ( for A being Ordinal holds H1( succ A) = H2(A,H1(A)) ) & ( for A being Ordinal
for L being Sequence st A <> 0 & A is limit_ordinal & dom L = A & ( for B being Ordinal st B in A holds
L . B = Tarski-Class (X,B) ) holds
Tarski-Class (X,A) = (union (rng L)) /\ (Tarski-Class X) ) )thus
for
A being
Ordinal holds
H1(
succ A)
= H2(
A,
H1(
A))
from ORDINAL2:sch 9(A1); for A being Ordinal
for L being Sequence st A <> 0 & A is limit_ordinal & dom L = A & ( for B being Ordinal st B in A holds
L . B = Tarski-Class (X,B) ) holds
Tarski-Class (X,A) = (union (rng L)) /\ (Tarski-Class X)thus
for
A being
Ordinal for
L being
Sequence st
A <> 0 &
A is
limit_ordinal &
dom L = A & ( for
B being
Ordinal st
B in A holds
L . B = Tarski-Class (
X,
B) ) holds
Tarski-Class (
X,
A)
= (union (rng L)) /\ (Tarski-Class X)
verum
end;
deffunc H1( Ordinal) -> set = Rank $1;
deffunc H2( set , set ) -> set = union $2;
Lm3:
for F being Function
for x being object st not x in rng F holds
Coim (F,x) = {}