Copyright (c) 1990 Association of Mizar Users
environ
vocabulary CLASSES2, ZF_LANG, FUNCT_1, ZF_MODEL, ORDINAL1, TARSKI, ORDINAL2,
BOOLE, ZFMODEL1, RELAT_1, CARD_1, ORDINAL4, PROB_1, CLASSES1, ZFMISC_1,
QC_LANG1, FUNCT_2, ARYTM_3, ZF_REFLE;
notation TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, NUMBERS, XREAL_0, NAT_1,
RELAT_1, FUNCT_1, FUNCT_2, FRAENKEL, ZF_MODEL, ZFMODEL1, ORDINAL1,
ORDINAL2, CARD_1, PROB_1, CLASSES1, CLASSES2, ZF_LANG, ORDINAL4,
ZF_LANG1;
constructors ENUMSET1, NAT_1, FRAENKEL, ZF_MODEL, ZFMODEL1, WELLORD2, PROB_1,
CLASSES1, ORDINAL4, ZF_LANG1, MEMBERED, XBOOLE_0;
clusters SUBSET_1, FUNCT_1, ZF_LANG, ORDINAL1, ORDINAL2, CLASSES2, ZF_LANG1,
RELSET_1, CARD_1, ZFMISC_1, XBOOLE_0;
requirements NUMERALS, BOOLE, SUBSET;
definitions TARSKI, FUNCT_1, ZF_LANG, ZF_MODEL, WELLORD2, ORDINAL2, RELAT_1,
XBOOLE_0;
theorems TARSKI, ZFMISC_1, NAT_1, FUNCT_1, FUNCT_2, ORDINAL1, ORDINAL2,
ORDINAL3, ORDINAL4, CARD_1, CARD_2, CLASSES1, CLASSES2, ZF_LANG,
ZF_MODEL, PROB_1, ZFMODEL1, FUNCT_5, ZF_LANG1, RELAT_1, RELSET_1,
XBOOLE_0, XBOOLE_1, XCMPLX_1;
schemes FUNCT_1, PARTFUN1, RECDEF_1, ORDINAL1, ORDINAL2, ZF_LANG, CARD_3;
begin
reserve W for Universe,
H for ZF-formula,
x,y,z,X,Y for set,
k for Variable,
f for Function of VAR,W,
u,v for Element of W;
canceled;
theorem
Th2: W |= the_axiom_of_pairs
proof
W is epsilon-transitive & for u,v holds {u,v} in W;
hence thesis by ZFMODEL1:2;
end;
theorem
Th3: W |= the_axiom_of_unions
proof
W is epsilon-transitive & for u holds union u in W;
hence thesis by ZFMODEL1:4;
end;
theorem
Th4: omega in W implies W |= the_axiom_of_infinity
proof assume omega in W;
then reconsider u = omega as Element of W;
now take u;
thus u <> {};
let v; assume
A1: v in u;
then reconsider A = v as Ordinal by ORDINAL1:23;
succ A in omega by A1,ORDINAL1:41,ORDINAL2:19;
then succ A c= u & u in W by ORDINAL1:def 2;
then reconsider w = succ A as Element of W by CLASSES1:def 1;
take w;
A in succ A by ORDINAL1:10;
then v c= w & v <> w & w in u by A1,ORDINAL1:41,def 2,ORDINAL2:19;
hence v c< w & w in u by XBOOLE_0:def 8;
end;
hence thesis by ZFMODEL1:6;
end;
theorem
Th5: W |= the_axiom_of_power_sets
proof
now let u; bool u in W & W /\ bool u c= bool u by XBOOLE_1:17;
hence W /\ bool u in W by CLASSES1:def 1;
end;
hence thesis by ZFMODEL1:8;
end;
theorem
Th6: for H st { x.0,x.1,x.2 } misses Free H holds
W |= the_axiom_of_substitution_for H
proof
for H,f st { x.0,x.1,x.2 } misses Free H &
W,f |= All(x.3,Ex(x.0,All(x.4,H <=> x.4 '=' x.0)))
for u holds def_func'(H,f).:u in W
proof let H,f such that { x.0,x.1,x.2 } misses Free H &
W,f |= All(x.3,Ex(x.0,All(x.4,H <=> x.4 '=' x.0)));
let u;
Card u <` Card W & def_func'(H,f).:u c= W &
Card (def_func'(H,f).:u) <=` Card u
by CARD_2:3,CLASSES2:1;
then Card (def_func'(H,f).:u) <` Card W by ORDINAL1:22;
hence thesis by CLASSES1:2;
end;
hence thesis by ZFMODEL1:19;
end;
theorem
omega in W implies W is_a_model_of_ZF
proof assume omega in W;
hence
W is epsilon-transitive &
W |= the_axiom_of_pairs &
W |= the_axiom_of_unions &
W |= the_axiom_of_infinity &
W |= the_axiom_of_power_sets &
for H st { x.0,x.1,x.2 } misses Free H holds
W |= the_axiom_of_substitution_for H
by Th2,Th3,Th4,Th5,Th6;
end;
reserve
F for Function,
A,A1,A2,B,C for Ordinal,
a,b,b1,b2,c for Ordinal of W,
fi for Ordinal-Sequence,
phi for Ordinal-Sequence of W,
H for ZF-formula;
definition let A,B;
redefine pred A c= B means for C st C in A holds C in B;
compatibility
proof
thus A c= B implies for C st C in A holds C in B;
assume
A1: for C st C in A holds C in B;
let x; assume
A2: x in A;
then reconsider C = x as Ordinal by ORDINAL1:23;
C in B by A1,A2;
hence thesis;
end;
end;
scheme ALFA { D() -> non empty set, P[set,set] }:
ex F st dom F = D() &
for d being Element of D() ex A st A = F.d & P[d,A] &
for B st P[d,B] holds A c= B
provided
A1: for d being Element of D() ex A st P[d,A]
proof
defpred Q[set,set] means
ex A st A = $2 & P[$1,A] & for B st P[$1,B] holds A c= B;
A2: for x,y,z st x in D() & Q[x,y] & Q[x,z] holds y = z
proof let x,y,z such that x in D();
given A1 such that
A3: A1 = y & P[x,A1] & for B st P[x,B] holds A1 c= B;
given A2 such that
A4: A2 = z & P[x,A2] & for B st P[x,B] holds A2 c= B;
A1 c= A2 & A2 c= A1 by A3,A4;
hence thesis by A3,A4,XBOOLE_0:def 10;
end;
A5: for x st x in D() ex y st Q[x,y]
proof let x; assume x in D(); then
reconsider d = x as Element of D();
defpred Q[Ordinal] means P[d,$1];
A6: ex A st Q[A] by A1;
consider A such that
A7: Q[A] & for B st Q[B] holds A c= B from Ordinal_Min(A6);
reconsider y = A as set;
take y,A; thus thesis by A7;
end;
consider F such that
A8: dom F = D() & for x st x in D() holds Q[x,F.x] from FuncEx(A2,A5);
take F; thus dom F = D() by A8;
let d be Element of D();
thus Q[d,F.d] by A8;
end;
scheme ALFA'Universe { W()->Universe, D() -> non empty set, P[set,set] }:
ex F st dom F = D() &
for d being Element of D() ex a being Ordinal of W() st a = F.d & P[d,a] &
for b being Ordinal of W() st P[d,b] holds a c= b
provided
A1: for d being Element of D() ex a being Ordinal of W() st P[d,a]
proof defpred p[set,set] means P[$1,$2];
A2: for d being Element of D() ex A st p[d,A]
proof let d be Element of D();
consider a being Ordinal of W() such that
A3: P[d,a] by A1;
reconsider a as Ordinal;
take a; thus thesis by A3;
end;
consider F such that
A4: dom F = D() and
A5: for d being Element of D() ex A st A = F.d & p[d,A] &
for B st p[d,B] holds A c= B from ALFA(A2);
take F; thus dom F = D() by A4;
let d be Element of D();
consider A such that
A6: A = F.d & P[d,A] & for B st P[d,B] holds A c= B by A5;
consider a being Ordinal of W() such that
A7: P[d,a] by A1;
A c= a & a in W() by A6,A7,ORDINAL4:def 2;
then A in W() by CLASSES1:def 1;
then reconsider a = A as Ordinal of W() by ORDINAL4:def 2;
take a; thus thesis by A6;
end;
theorem
Th8: x is Ordinal of W iff x in On W
proof
(x is Ordinal of W iff x is Ordinal & x in W) &
(x in On W iff x is Ordinal & x in W) by ORDINAL2:def 2,ORDINAL4:def 2;
hence thesis;
end;
reserve psi for Ordinal-Sequence;
scheme OrdSeqOfUnivEx { W()->Universe, P[set,set] }:
ex phi being Ordinal-Sequence of W() st
for a being Ordinal of W() holds P[a,phi.a]
provided
A1: for a,b1,b2 being Ordinal of W() st P[a,b1] & P[a,b2] holds b1 = b2 and
A2: for a being Ordinal of W() ex b being Ordinal of W() st P[a,b]
proof defpred Q[set,set] means P[$1,$2] & $2 is Ordinal of W();
A3: for x,y,z st x in On W() & Q[x,y] & Q[x,z] holds y = z
proof let x,y,z; assume x in On W();
then reconsider a = x as Ordinal of W() by Th8;
assume
A4: (P[x,y] & y is Ordinal of W()) & (P[x,z] & z is Ordinal of W());
then reconsider b1 = y, b2 = z as Ordinal of W();
P[a,b1] & P[a,b2] by A4;
hence thesis by A1;
end;
A5: for x st x in On W() ex y st Q[x,y]
proof let x; assume x in On W();
then reconsider a = x as Ordinal of W() by Th8;
consider b being Ordinal of W() such that
A6: P[a,b] by A2;
reconsider y = b as set;
take y; thus thesis by A6;
end;
consider f being Function such that
A7: dom f = On W() &
for x st x in On W() holds Q[x,f.x] from FuncEx(A3,A5);
reconsider phi = f as T-Sequence by A7,ORDINAL1:def 7;
A8: rng phi c= On W()
proof let x; assume x in rng phi;
then ex y st y in dom phi & x = phi.y by FUNCT_1:def 5;
then reconsider x as Ordinal of W() by A7;
x in W() by ORDINAL4:def 2;
hence thesis by ORDINAL2:def 2;
end;
then reconsider phi as Ordinal-Sequence by ORDINAL2:def 8;
reconsider phi as Ordinal-Sequence of W() by A7,A8,ORDINAL4:def 3;
take phi; let a be Ordinal of W();
a in W() by ORDINAL4:def 2;
then a in On W() by ORDINAL2:def 2;
hence P[a,phi.a] by A7;
end;
scheme UOS_Exist { W()->Universe, a()->Ordinal of W(),
C(Ordinal,Ordinal)->Ordinal of W(),
D(Ordinal,T-Sequence)->Ordinal of W() } :
ex phi being Ordinal-Sequence of W() st
phi.0-element_of W() = a() &
(for a being Ordinal of W() holds phi.(succ a) = C(a,phi.a)) &
(for a being Ordinal of W() st a <> 0-element_of W() & a is_limit_ordinal
holds phi.a = D(a,phi|a))
proof
deffunc c(Ordinal,Ordinal) = C($1,$2);
deffunc d(Ordinal,T-Sequence) = D($1,$2);
consider phi being Ordinal-Sequence such that
A1: dom phi = On W() and
A2: {} in On W() implies phi.{} = a() and
A3: for A st succ A in On W() holds phi.(succ A) = c(A,phi.A) and
A4: for A st A in On W() & A <> {} & A is_limit_ordinal
holds phi.A = d(A,phi|A) from OS_Exist;
rng phi c= On W()
proof let x; assume x in rng phi;
then consider y such that
A5: y in dom phi & x = phi.y by FUNCT_1:def 5;
reconsider y as Ordinal of W() by A1,A5,Th8;
A6: now given A such that
A7: y = succ A;
reconsider B = phi.A as Ordinal;
x = C(A,B) by A1,A3,A5,A7;
hence thesis by Th8;
end;
now assume not ex A st y = succ A;
then A8: y is_limit_ordinal by ORDINAL1:42;
assume y <> {};
then x = D(y,phi|y) by A1,A4,A5,A8;
hence thesis by Th8;
end;
hence thesis by A2,A5,A6,Th8;
end;
then reconsider phi as Ordinal-Sequence of W() by A1,ORDINAL4:def 3;
take phi; 0-element_of W() in dom phi by ORDINAL4:36;
hence phi.0-element_of W() = a() by A1,A2,ORDINAL4:35;
thus for a being Ordinal of W() holds phi.(succ a) = C(a,phi.a)
proof let a be Ordinal of W();
succ a in dom phi by ORDINAL4:36;
hence thesis by A1,A3;
end;
let a be Ordinal of W();
a in dom phi & {} = 0-element_of W() by ORDINAL4:35,36;
hence thesis by A1,A4;
end;
scheme Universe_Ind { W()->Universe, P[Ordinal] }:
for a being Ordinal of W() holds P[a]
provided
A1: P[0-element_of W()] and
A2: for a being Ordinal of W() st P[a] holds P[succ a] and
A3: for a being Ordinal of W() st a <> 0-element_of W() & a is_limit_ordinal &
for b being Ordinal of W() st b in a holds P[b] holds P[a]
proof defpred Q[Ordinal] means $1 is Ordinal of W() implies P[$1];
A4: Q[{}] by A1,ORDINAL4:35;
A5: for A st Q[A] holds Q[succ A]
proof let A such that
A6: A is Ordinal of W() implies P[A] and
A7: succ A is Ordinal of W();
A in succ A & succ A in On W() by A7,Th8,ORDINAL1:10;
then A in On W() by ORDINAL1:19;
then reconsider a = A as Ordinal of W() by Th8;
P[succ a] by A2,A6;
hence thesis;
end;
A8: for A st A <> {} & A is_limit_ordinal & for B st B in A holds Q[B]
holds Q[A]
proof let A such that
A9: A <> {} & A is_limit_ordinal and
A10: for B st B in A holds B is Ordinal of W() implies P[B];
assume A is Ordinal of W();
then reconsider a = A as Ordinal of W();
{} = 0-element_of W() & for b be Ordinal of W() st b in a holds P[b]
by A10,ORDINAL4:35;
hence P[A] by A3,A9;
end;
Q[A] from Ordinal_Ind(A4,A5,A8);
hence thesis;
end;
definition let f be Function, W be Universe, a be Ordinal of W;
func union(f,a) -> set equals:
Def2: Union (W|(f|Rank a));
correctness;
end;
canceled;
theorem
Th10: for L being T-Sequence,A holds L|Rank A is T-Sequence
proof let L be T-Sequence, A;
A1: dom(L|Rank A) = dom L /\ Rank A by RELAT_1:90;
now let X; assume X in dom(L|Rank A);
then A2: X in dom L & X in Rank A by A1,XBOOLE_0:def 3;
hence X is Ordinal by ORDINAL1:23;
X c= dom L & X c= Rank A by A2,ORDINAL1:def 2;
hence X c= dom(L|Rank A) by A1,XBOOLE_1:19;
end;
then dom(L|Rank A) is Ordinal by ORDINAL1:31;
hence thesis by ORDINAL1:46;
end;
theorem
Th11: for L being Ordinal-Sequence,A holds L|Rank A is Ordinal-Sequence
proof let L be Ordinal-Sequence, A;
reconsider K = L|Rank A as T-Sequence by Th10;
consider B such that
A1: rng L c= B by ORDINAL2:def 8;
rng K c= rng L by FUNCT_1:76;
then rng K c= B by A1,XBOOLE_1:1;
hence thesis by ORDINAL2:def 8;
end;
theorem
Union psi is Ordinal
proof consider A such that
A1: rng psi c= A by ORDINAL2:def 8;
A2: Union psi = union rng psi by PROB_1:def 3;
for x st x in rng psi holds x is Ordinal by A1,ORDINAL1:23;
hence thesis by A2,ORDINAL1:35;
end;
theorem
Th13: Union (X|psi) is Ordinal
proof consider A such that
A1: rng psi c= A by ORDINAL2:def 8;
A2: Union (X|psi) = union rng (X|psi) & rng (X|psi) c= rng psi
by FUNCT_1:89,PROB_1:def 3;
now let x; assume x in rng (X|psi);
then x in A by A1,A2,TARSKI:def 3;
hence x is Ordinal by ORDINAL1:23;
end;
hence thesis by A2,ORDINAL1:35;
end;
theorem
Th14: On Rank A = A
proof
thus On Rank A c= A
proof let x; assume A1: x in On Rank A;
then A2: x is Ordinal & x in Rank A by ORDINAL2:def 2;
reconsider B = x as Ordinal by A1,ORDINAL2:def 2;
the_rank_of B in A by A2,CLASSES1:74;
hence x in A by CLASSES1:81;
end;
A c= Rank A by CLASSES1:44;
then On A c= On Rank A by ORDINAL2:11;
hence thesis by ORDINAL2:10;
end;
theorem
Th15: psi|Rank A = psi|A
proof
A c= Rank A by CLASSES1:44;
then A1: (psi|Rank A)|A = psi|A & dom (psi|Rank A) c= Rank A &
dom (psi|Rank A) c= dom psi by FUNCT_1:76,82,RELAT_1:87;
then On dom (psi|Rank A) c= On Rank A & On dom (psi|Rank A) = dom (psi|
Rank A)
by ORDINAL2:11,ORDINAL3:8;
then dom (psi|Rank A) c= A by Th14;
hence psi|Rank A = psi|A by A1,RELAT_1:97;
end;
definition let phi be Ordinal-Sequence, W be Universe, a be Ordinal of W;
redefine func union(phi,a) -> Ordinal of W;
coherence
proof
reconsider K = phi|Rank a as Ordinal-Sequence by Th11;
reconsider A = Union (W|K) as Ordinal by Th13;
A1: a in On W & W is_Tarski-Class & rng (W|K) c= W & dom (W|K) c= dom K
by Th8,FUNCT_1:89,RELAT_1:116;
then dom K c= Rank a & Rank a in W by CLASSES2:26,RELAT_1:87;
then dom K in W by CLASSES1:def 1;
then dom (W|K) in W by A1,CLASSES1:def 1;
then Card dom (W|K) <` Card W & Card ((W|K).:dom(W|K)) <=` Card dom(W|K)
&
(W|K).:dom(W|K) = rng(W|K) by CARD_2:3,CLASSES2:1,RELAT_1:146;
then Card rng (W|K) <` Card W by ORDINAL1:22;
then rng (W|K) in W & union rng (W|K) = Union (W|K)
by A1,CLASSES1:2,PROB_1:def 3;
then A in W & A = union (phi,a) by Def2,CLASSES2:65;
hence thesis by ORDINAL4:def 2;
end;
end;
canceled;
theorem
Th17: for phi being Ordinal-Sequence of W holds
union(phi,a) = Union (phi|a) & union(phi|a,a) = Union (phi|a)
proof let phi be Ordinal-Sequence of W;
rng phi c= On W & On W c= W by ORDINAL2:9,ORDINAL4:def 3;
then rng (phi|Rank a) c= rng phi & rng (phi|a) c= rng phi &
rng phi c= W by FUNCT_1:76,XBOOLE_1:1;
then rng (phi|Rank a) c= W & rng (phi|a) c= W & a c= Rank a
by CLASSES1:44,XBOOLE_1:1;
then (phi|a)|Rank a = phi|a & W|(phi|Rank a) = phi|Rank a &
phi|a = W|(phi|a) by FUNCT_1:82,RELAT_1:125;
then union(phi,a) = Union (phi|Rank a) &
union(phi|a,a) = Union (phi|a) by Def2;
hence thesis by Th15;
end;
definition let W be Universe, a,b be Ordinal of W;
redefine func a \/ b -> Ordinal of W;
coherence
proof
a,b are_c=-comparable by ORDINAL1:25;
then a c= b or b c= a by XBOOLE_0:def 9;
hence thesis by XBOOLE_1:12;
end;
end;
definition let W;
cluster non empty Element of W;
existence
proof consider u;
{u} is non empty Element of W;
hence thesis;
end;
end;
definition let W;
mode Subclass of W is non empty Subset of W;
end;
definition let W;
let IT be T-Sequence of W;
canceled 2;
attr IT is DOMAIN-yielding means:
Def5: dom IT = On W;
end;
definition let W;
cluster DOMAIN-yielding non-empty T-Sequence of W;
existence
proof consider D being non empty Element of W;
deffunc F(set) = D;
consider L being T-Sequence such that
A1: dom L = On W &
for A for L1 being T-Sequence st A in On W & L1 = L|A holds L.A = F(L1)
from TS_Exist;
rng L c= W
proof let x; assume x in rng L;
then consider y such that
A2: y in dom L & x = L.y by FUNCT_1:def 5;
reconsider y as Ordinal by A2,ORDINAL1:23;
L|y = L|y;
then x = D by A1,A2;
hence thesis;
end;
then reconsider L as T-Sequence of W by ORDINAL1:def 8;
take L; thus dom L = On W by A1;
assume {} in rng L;
then consider x such that
A3: x in dom L & {} = L.x by FUNCT_1:def 5;
reconsider x as Ordinal by A3,ORDINAL1:23;
L|x = L|x;
hence contradiction by A1,A3;
end;
end;
definition let W;
mode DOMAIN-Sequence of W is non-empty DOMAIN-yielding T-Sequence of W;
end;
Lm1: X <> {} & X c= Y implies Y <> {}
proof assume A1: X <> {};
consider x being Element of X;
A2: x in X by A1;
assume y in X implies y in Y;
hence thesis by A2;
end;
definition let W; let L be DOMAIN-Sequence of W;
redefine func Union L -> Subclass of W;
coherence
proof rng L c= W & Union L = union rng L by ORDINAL1:def 8,PROB_1:def 3;
then A1: Union L c= union W by ZFMISC_1:95;
consider a; a in W by ORDINAL4:def 2;
then a in On W by ORDINAL2:def 2;
then a in dom L by Def5;
then L.a in rng L & L.a = L.a by FUNCT_1:def 5;
then L.a c= union rng L & L.a <> {} by RELAT_1:def 9,ZFMISC_1:92;
then union rng L <> {} & union rng L = Union L by Lm1,PROB_1:def 3;
then reconsider S = Union L as non empty set;
S c= W
proof let x; assume x in S;
then consider X such that
A2: x in X & X in W by A1,TARSKI:def 4;
X c= W by A2,ORDINAL1:def 2;
hence thesis by A2;
end;
hence thesis;
end;
let a;
func L.a -> non empty Element of W;
coherence
proof a in W by ORDINAL4:def 2; then a in On W by ORDINAL2:def 2;
then a in dom L by Def5;
then L.a in rng L & rng L c= W by FUNCT_1:def 5,ORDINAL1:def 8;
hence thesis by RELAT_1:def 9;
end;
end;
reserve L for DOMAIN-Sequence of W,
n,j for Nat,
f for Function of VAR,L.a;
canceled 5;
theorem
Th23: a in dom L
proof a in W by ORDINAL4:def 2; then a in On W by ORDINAL2:def 2;
hence thesis by Def5;
end;
theorem
Th24: L.a c= Union L
proof a in dom L by Th23;
then L.a in rng L & union rng L = Union L by FUNCT_1:def 5,PROB_1:def 3;
hence thesis by ZFMISC_1:92;
end;
theorem
Th25: NAT,VAR are_equipotent
proof deffunc F(Nat,set) = 5+($1+1);
consider f being Function of NAT,NAT such that
A1: f.0 = 5+0 & for n holds f.(n+1) = F(n,f.n) from LambdaRecExD;
A2: dom f = NAT by FUNCT_2:def 1;
A3: now let n;
now given j such that A4: n = j+1;
thus f.n = 5+n by A1,A4;
end;
then n = 0 or f.n = 5+n by NAT_1:22;
hence f.n = 5+n by A1;
end;
thus NAT,VAR are_equipotent
proof reconsider g = f as Function; take g;
thus g is one-to-one
proof let x,y; assume x in dom g & y in dom g;
then reconsider n1 = x, n2 = y as Nat by FUNCT_2:def 1;
f.n1 = 5+n1 & f.n2 = 5+n2 by A3;
hence thesis by XCMPLX_1:2;
end;
thus dom g = NAT by FUNCT_2:def 1;
thus rng g c= VAR
proof let x; assume x in rng g;
then consider y such that
A5: y in dom f & x = f.y by FUNCT_1:def 5;
reconsider y as Nat by A5,FUNCT_2:def 1;
x = 5+y & 5+y >= 5 by A3,A5,NAT_1:29;
hence thesis by ZF_LANG:def 1;
end;
let x; assume x in VAR;
then ex n st x = n & 5 <= n by ZF_LANG:def 1;
then consider n such that
A6: x = 5+n by NAT_1:28;
f.n = x & n in NAT by A3,A6;
hence thesis by A2,FUNCT_1:def 5;
end;
end;
canceled;
theorem
Th27: sup X c= succ union On X
proof reconsider A = union On X as Ordinal by ORDINAL3:7;
On X c= succ A
proof let x; assume
A1: x in On X;
then reconsider a = x as Ordinal by ORDINAL2:def 2;
a c= A by A1,ZFMISC_1:92;
hence x in succ A by ORDINAL1:34;
end;
hence thesis by ORDINAL2:def 7;
end;
theorem
Th28: X in W implies sup X in W
proof assume
A1: X in W;
reconsider a = union On X as Ordinal by ORDINAL3:7;
On X c= X by ORDINAL2:9;
then On X in W by A1,CLASSES1:def 1;
then a in W by CLASSES2:65;
then reconsider a as Ordinal of W by ORDINAL4:def 2;
sup X c= succ a & succ a in W by Th27,ORDINAL4:def 2;
hence thesis by CLASSES1:def 1;
end;
reserve x1 for Variable;
theorem
omega in W & (for a,b st a in b holds L.a c= L.b) &
(for a st a <> {} & a is_limit_ordinal holds L.a = Union (L|a)) implies
for H ex phi st phi is increasing & phi is continuous &
for a st phi.a = a & {} <> a
for f holds Union L,(Union L)!f |= H iff L.a,f |= H
proof assume
A1: omega in W & (for a,b st a in b holds L.a c= L.b) &
for a st a <> {} & a is_limit_ordinal holds L.a = Union (L|a);
set M = Union L;
A2: dom L = On W by Def5;
A3: union rng L = M by PROB_1:def 3;
defpred RT[ZF-formula] means
ex phi st phi is increasing & phi is continuous &
for a st phi.a = a & {} <> a for f holds M,M!f |= $1 iff L.a,f |= $1;
A4: for H st H is atomic holds RT[H]
proof let H such that
A5: H is_equality or H is_membership;
A6: dom id On W = On W & rng id On W = On W by RELAT_1:71;
then reconsider phi = id On W as T-Sequence by ORDINAL1:def 7;
reconsider phi as Ordinal-Sequence by A6,ORDINAL2:def 8;
reconsider phi as Ordinal-Sequence of W by A6,ORDINAL4:def 3;
take phi;
thus
A7: phi is increasing
proof let A,B; assume
A8: A in B & B in dom phi;
then A in dom phi by ORDINAL1:19;
then phi.A = A & phi.B = B by A6,A8,FUNCT_1:35;
hence thesis by A8;
end;
thus phi is continuous
proof let A,B; assume
A9: A in dom phi & A <> {} & A is_limit_ordinal & B = phi.A;
then A10: phi.A = A & A c= dom phi by A6,FUNCT_1:35,ORDINAL1:def 2;
phi|A = phi*(id A) by RELAT_1:94
.= id((dom phi) /\ A) by A6,FUNCT_1:43
.= id A by A10,XBOOLE_1:28;
then rng(phi|A) = A by RELAT_1:71;
then A11: sup(phi|A) = sup A by ORDINAL2:35 .= B by A9,A10,ORDINAL2:26;
dom (phi|A) = A & phi|A is increasing
by A7,A10,ORDINAL4:15,RELAT_1:91;
hence thesis by A9,A11,ORDINAL4:8;
end;
let a such that phi.a = a & {} <> a;
A12: L.a c= M by Th24;
let f;
thus M,M!f |= H implies L.a,f |= H
proof assume
A13: M,M!f |= H;
A14: M!f = f by A12,ZF_LANG1:def 2;
A15: now assume H is_equality;
then A16: H = (Var1 H) '=' (Var2 H) by ZF_LANG:53;
then (M!f).Var1 H = (M!f).Var2 H by A13,ZF_MODEL:12;
hence thesis by A14,A16,ZF_MODEL:12;
end;
now assume H is_membership;
then A17: H = (Var1 H) 'in' (Var2 H) by ZF_LANG:54;
then (M!f).Var1 H in (M!f).Var2 H by A13,ZF_MODEL:13;
hence thesis by A14,A17,ZF_MODEL:13;
end;
hence thesis by A5,A15;
end;
assume
A18: L.a,f |= H;
A19: M!f = f by A12,ZF_LANG1:def 2;
A20: now assume H is_equality;
then A21: H = (Var1 H) '=' (Var2 H) by ZF_LANG:53;
then f.Var1 H = f.Var2 H by A18,ZF_MODEL:12;
hence thesis by A19,A21,ZF_MODEL:12;
end;
now assume H is_membership;
then A22: H = (Var1 H) 'in' (Var2 H) by ZF_LANG:54;
then f.Var1 H in f.Var2 H by A18,ZF_MODEL:13;
hence thesis by A19,A22,ZF_MODEL:13;
end;
hence M,M!f |= H by A5,A20;
end;
A23: for H st H is negative & RT[the_argument_of H] holds RT[H]
proof let H; assume H is negative;
then A24: H = 'not' the_argument_of H by ZF_LANG:def 30;
given phi such that
A25: phi is increasing & phi is continuous and
A26: for a st phi.a = a & {} <> a
for f holds M,M!f |= the_argument_of H iff L.a,f |= the_argument_of H;
take phi;
thus phi is increasing & phi is continuous by A25;
let a such that
A27: phi.a = a & {} <> a;
A28: L.a c= M by Th24;
let f;
thus M,M!f |= H implies L.a,f |= H
proof assume
M,M!f |= H;
then not M,M!f |= the_argument_of H & f = M!f
by A24,A28,ZF_LANG1:def 2,ZF_MODEL:14;
then not L.a,f |= the_argument_of H by A26,A27;
hence thesis by A24,ZF_MODEL:14;
end;
assume L.a,f |= H;
then not L.a,f |= the_argument_of H by A24,ZF_MODEL:14;
then not M,M!f |= the_argument_of H by A26,A27;
hence thesis by A24,ZF_MODEL:14;
end;
A29: for H st H is conjunctive &
RT[the_left_argument_of H] & RT[the_right_argument_of H] holds RT[H]
proof let H; assume H is conjunctive;
then A30: H = (the_left_argument_of H) '&' (the_right_argument_of H)
by ZF_LANG:58;
given fi1 being Ordinal-Sequence of W such that
A31: fi1 is increasing & fi1 is continuous and
A32: for a st fi1.a = a & {} <> a for f holds
M,M!f |= the_left_argument_of H iff L.a,f |= the_left_argument_of H;
given fi2 being Ordinal-Sequence of W such that
A33: fi2 is increasing & fi2 is continuous and
A34: for a st fi2.a = a & {} <> a for f holds
M,M!f |= the_right_argument_of H iff L.a,f |= the_right_argument_of H;
take phi = fi2*fi1;
ex fi st fi = fi2*fi1 & fi is increasing by A31,A33,ORDINAL4:13;
hence phi is increasing & phi is continuous
by A31,A33,ORDINAL4:17;
let a such that
A35: phi.a = a & {} <> a;
A36: a in dom fi1 & a in dom fi2 & a in dom phi by ORDINAL4:36;
then A37: a c= fi1.a & a c= fi2.a by A31,A33,ORDINAL4:10;
A38: now assume fi1.a <> a;
then a c< fi1.a by A37,XBOOLE_0:def 8;
then A39: a in fi1.a by ORDINAL1:21;
fi1.a in dom fi2 by ORDINAL4:36;
then A40: fi2.a in fi2.(fi1.a) by A33,A39,ORDINAL2:def 16;
phi.a = fi2.(fi1.a) by A36,FUNCT_1:22;
hence contradiction by A35,A37,A40,ORDINAL1:7;
end;
then A41: fi2.a = a by A35,A36,FUNCT_1:22;
A42: L.a c= M by Th24;
let f;
thus M,M!f |= H implies L.a,f |= H
proof assume
M,M!f |= H;
then M,M!f |= the_left_argument_of H & M,M!f |=
the_right_argument_of H &
f = M!f by A30,A42,ZF_LANG1:def 2,ZF_MODEL:15;
then L.a,f |= the_left_argument_of H & L.a,f |=
the_right_argument_of H
by A32,A34,A35,A38,A41;
hence thesis by A30,ZF_MODEL:15;
end;
assume L.a,f |= H;
then L.a,f |= the_left_argument_of H & L.a,f |= the_right_argument_of H
by A30,ZF_MODEL:15;
then M,M!f |= the_left_argument_of H & M,M!f |= the_right_argument_of H
by A32,A34,A35,A38,A41;
hence thesis by A30,ZF_MODEL:15;
end;
A43: for H st H is universal & RT[the_scope_of H] holds RT[H]
proof let H; assume H is universal;
then A44: H = All(bound_in H,the_scope_of H) by ZF_LANG:62;
given phi such that
A45: phi is increasing & phi is continuous and
A46: for a st phi.a = a & {} <> a for f holds
M,M!f |= the_scope_of H iff L.a,f |= the_scope_of H;
set x0 = bound_in H;
set H' = the_scope_of H;
A47: now assume
A48: not x0 in Free H';
thus thesis
proof take phi;
thus phi is increasing & phi is continuous by A45;
let a such that
A49: phi.a = a & {} <> a;
let f;
thus M,M!f |= H implies L.a,f |= H
proof assume
A50: M,M!f |= H;
for k st (M!f).k <> (M!f).k holds x0 = k;
then M,M!f |= H' by A44,A50,ZF_MODEL:16;
then L.a,f |= H' by A46,A49;
hence L.a,f |= H by A44,A48,ZFMODEL1:10;
end;
assume
A51: L.a,f |= H;
for k st f.k <> f.k holds x0 = k;
then L.a,f |= H' by A44,A51,ZF_MODEL:16;
then M,M!f |= H' by A46,A49;
hence M,M!f |= H by A44,A48,ZFMODEL1:10;
end;
end;
defpred P[set,set] means
ex f being Function of VAR,M st $1 = f &
((ex m being Element of M st m in L.$2 & M,f/(x0,m) |= 'not' H') or
$2 = 0-element_of W & not ex m being Element of M st
M,f/(x0,m) |= 'not' H');
A52: for h being Element of Funcs(VAR,M) qua non empty set
ex a st P[h,a]
proof let h be Element of Funcs(VAR,M) qua non empty set;
reconsider f = h as Element of Funcs(VAR,M);
reconsider f as Function of VAR,M;
now per cases;
suppose
for m being Element of M holds not M,f/(x0,m) |= 'not' H';
hence thesis;
suppose
A53: not for m being Element of M holds not M,f/(x0,m) |= 'not' H';
thus thesis
proof consider m being Element of M such that
A54: M,f/(x0,m) |= 'not' H' by A53;
consider X be set such that
A55: m in X & X in rng L by A3,TARSKI:def 4;
consider x such that
A56: x in dom L & X = L.x by A55,FUNCT_1:def 5;
reconsider x as Ordinal by A56,ORDINAL1:23;
x in W by A2,A56,ORDINAL2:def 2;
then reconsider b = x as Ordinal of W by ORDINAL4:def 2;
take b, f; thus thesis by A54,A55,A56;
end;
end;
hence thesis;
end;
consider rho being Function such that
A57: dom rho = Funcs(VAR,M) qua non empty set and
A58: for h being Element of Funcs(VAR,M) qua non empty set
ex a st a = rho.h & P[h,a] &
for b st P[h,b] holds a c= b from ALFA'Universe(A52);
defpred SI[Ordinal of W,Ordinal of W] means
$2 = sup (rho.:Funcs(VAR,L.$1));
A59: for a,b1,b2 st SI[a, b1] & SI[a, b2] holds b1 = b2;
A60: for a ex b st SI[a, b]
proof let a; set X = rho.:Funcs(VAR,L.a);
A61: X c= W
proof let x; assume x in X;
then consider h being set such that
A62: h in dom rho & h in Funcs(VAR,L.a) & x = rho.h by FUNCT_1:def 12;
L.a c= M by Th24;
then Funcs(VAR,L.a) c= Funcs(VAR,M) by FUNCT_5:63;
then reconsider h as Element of Funcs(VAR,M) qua non empty set by
A62;
ex a st a = rho.h &
(ex f being Function of VAR,M st h = f & ((ex m being Element of
M st m in L.a & M,f/(x0,m) |= 'not'
H') or a = 0-element_of W & not ex m being
Element of M st M,f/(x0,m) |= 'not' H')) & for b st ex f being
Function of VAR,M st h = f & ((ex m being Element of M st m in L.b
& M,f/(x0,m) |= 'not'
H') or b = 0-element_of W & not ex m being Element of M
st M,f/(x0,m) |= 'not' H') holds a c= b by A58;
hence x in W by A62,ORDINAL4:def 2;
end;
L.a in W & Card VAR = Card omega & Card(L.a) = Card(L.a)
by Th25,CARD_1:21;
then Card Funcs(VAR,L.a) = Card Funcs(omega,L.a) & Funcs(omega,L.a)
in W
by A1,CLASSES2:67,FUNCT_5:68;
then Card X <=` Card Funcs(omega,L.a) & Card Funcs(omega,L.a) <`
Card W
by CARD_2:3,CLASSES2:1;
then Card X <` Card W & W is_Tarski-Class by ORDINAL1:22;
then X in W by A61,CLASSES1:2;
then sup X in W by Th28;
then reconsider b = sup X as Ordinal of W by ORDINAL4:def 2;
take b; thus thesis;
end;
consider si being Ordinal-Sequence of W such that
A63: for a holds SI[a, si.a] from OrdSeqOfUnivEx(A59,A60);
deffunc C(Ordinal of W, Ordinal of W) = succ((si.succ $1) \/ $2);
deffunc D(Ordinal of W, Ordinal-Sequence) = union($2,$1);
consider ksi being Ordinal-Sequence of W such that
A64: ksi.0-element_of W = si.0-element_of W and
A65: for a holds ksi.(succ a) = C(a,ksi.a) and
A66: for a st a <> 0-element_of W & a is_limit_ordinal
holds ksi.a = D(a,ksi|a) from UOS_Exist;
A67: dom ksi = On W by ORDINAL4:def 3;
A68: 0-element_of W = {} by ORDINAL4:35;
A69: ksi is increasing
proof let A,B; assume
A70: A in B & B in dom ksi;
then A in dom ksi by ORDINAL1:19;
then reconsider a = A, b = B as Ordinal of W by A67,A70,Th8;
defpred Theta[Ordinal of W] means a in $1 implies ksi.a in ksi.$1;
A71: Theta[0-element_of W] by ORDINAL4:35;
A72: Theta[c] implies Theta[succ c]
proof assume that
A73: a in c implies ksi.a in ksi.c and
A74: a in succ c;
A75: a c= c & ksi.succ c = succ((si.succ c) \/ ksi.c) &
(si.succ c) \/ ksi.c in succ((si.succ c) \/ ksi.c) &
ksi.c c= (si.succ c) \/ ksi.c
by A65,A74,ORDINAL1:34,XBOOLE_1:7;
ksi.a in ksi.c or ksi.a = ksi.c
proof
per cases;
suppose a <> c;
then a c< c by A75,XBOOLE_0:def 8;
hence thesis by A73,ORDINAL1:21;
suppose a = c;
hence thesis;
end;
hence thesis by A75,ORDINAL1:19,22;
end;
A76: for b st b <> 0-element_of W & b is_limit_ordinal &
for c st c in b holds Theta[c] holds Theta[b]
proof let b such that
A77: b <> 0-element_of W & b is_limit_ordinal and
for c st c in b holds Theta[c] and
A78: a in b;
A79: ksi.b = union(ksi|b,b) by A66,A77 .= Union (ksi|b) by Th17
.= union rng (ksi|b) by PROB_1:def 3;
succ a in dom ksi & succ a in b
by A77,A78,ORDINAL1:41,ORDINAL4:36;
then A80: ksi.succ a in rng(ksi|b) by FUNCT_1:73;
ksi.succ a = succ((si.succ a) \/ ksi.a) by A65;
then (si.succ a) \/ ksi.a in ksi.succ a &
ksi.a c= (si.succ a) \/ ksi.a by ORDINAL1:10,XBOOLE_1:7;
then ksi.a in ksi.succ a by ORDINAL1:22;
hence thesis by A79,A80,TARSKI:def 4;
end;
Theta[c] from Universe_Ind(A71,A72,A76);
then ksi.a in ksi.b by A70;
hence thesis;
end;
defpred P[Ordinal] means si.$1 c= ksi.$1;
A81: P[0-element_of W] by A64;
A82: P[a] implies P[succ a]
proof assume si.a c= ksi.a;
ksi.succ a = succ((si.succ a) \/ (ksi.a)) &
(si.succ a) \/ (ksi.a) in succ((si.succ a) \/ (ksi.a)) &
si.succ a c= (si.succ a) \/ (ksi.a)
by A65,ORDINAL1:10,XBOOLE_1:7;
then si.succ a in ksi.succ a by ORDINAL1:22;
hence si.succ a c= ksi.succ a by ORDINAL1:def 2;
end;
A83: a <> 0-element_of W & a is_limit_ordinal implies si.a c= sup (si|a)
proof assume
A84: a <> 0-element_of W & a is_limit_ordinal;
let A such that
A85: A in si.a;
si.a = sup (rho.:Funcs(VAR,L.a)) by A63;
then consider B such that
A86: B in rho.:Funcs(VAR,L.a) & A c= B by A85,ORDINAL2:29;
consider x such that
A87: x in dom rho & x in Funcs(VAR,L.a) & B = rho.x by A86,FUNCT_1:def 12;
reconsider h = x as Element of Funcs(VAR,M) qua non empty set
by A57,A87;
consider a1 being Ordinal of W such that
A88: a1 = rho.h &
(ex f being Function of VAR,M st h = f &
((ex m being Element of M st m in L.a1 & M,f/(x0,m) |= 'not' H') or
a1 = 0-element_of W & not ex m being Element of M st
M,f/(x0,m) |= 'not' H'))&
for b st
ex f being Function of VAR,M st h = f &
((ex m being Element of M st m in L.b & M,f/(x0,m) |= 'not' H') or
b = 0-element_of W & not ex m being Element of M st
M,f/(x0,m) |= 'not' H')
holds a1 c= b by A58;
consider f being Function of VAR,M such that
A89: h = f &
((ex m being Element of M st m in L.a1 & M,f/(x0,m) |= 'not' H') or
a1 = 0-element_of W & not ex m being Element of M st
M,f/(x0,m) |= 'not' H') by A88;
defpred P[set,set] means for a st f.$1 in L.a holds f.$2 in L.a;
A90: now assume Free 'not' H' <> {}; then
A91: Free 'not' H' <> {};
A92: for x,y holds P[x,y] or P[y,x]
proof let x,y; given a such that
A93: f.x in L.a & not f.y in L.a;
let b such that
A94: f.y in L.b; a in b or a = b or b in a by ORDINAL1:24;
then L.a c= L.b or L.b c= L.a by A1;
hence thesis by A93,A94;
end;
A95: for x,y,z st P[x,y] & P[y,z] holds P[x,z]
proof let x,y,z such that
A96: (for a st f.x in L.a holds f.y in L.a) &
(for a st f.y in L.a holds f.z in L.a);
let a; assume f.x in L.a; then f.y in L.a by A96;
hence f.z in L.a by A96;
end;
consider z such that
A97: z in Free 'not' H' & for y st y in Free 'not' H' holds P[z,y]
from MaxFinSetElem(A91,A92,A95);
reconsider z as Variable by A97;
A98: ex s being Function st f = s & dom s = VAR & rng s c= L.a
by A87,A89,FUNCT_2:def 2;
then f.z in rng f by FUNCT_1:def 5;
then f.z in L.a & L.a = Union (L|a) & Union (L|a) = union rng (L|a
)
by A1,A68,A84,A98,PROB_1:def 3;
then consider X such that
A99: f.z in X & X in rng (L|a) by TARSKI:def 4;
consider x such that
A100: x in dom (L|a) & X = (L|a).x by A99,FUNCT_1:def 5;
A101: dom (L|a) c= a & (L|a).x = L.x by A100,FUNCT_1:70,RELAT_1:87;then
A102: x in a & a in On W by A100,Th8;
reconsider x as Ordinal by A100,ORDINAL1:23;
x in On W by A102,ORDINAL1:19;
then reconsider x as Ordinal of W by Th8;
take x; thus x in a by A100,A101;
let y be Variable; assume y in Free 'not' H';
hence f.y in L.x by A97,A99,A100,A101;
end;
now assume
A103: Free 'not' H' = {};
take b = 0-element_of W; thus b in a by A68,A84,ORDINAL3:10;
thus for x1 st x1 in Free 'not' H' holds f.x1 in L.b by A103;
end;
then consider c such that
A104: c in a & for x1 st x1 in Free 'not' H' holds f.x1 in L.c by A90;
consider e being Element of L.c;
defpred C[set] means $1 in Free 'not' H';
deffunc F(set) = f.$1;
deffunc G(set) = e;
consider v being Function such that
A105: dom v = VAR & for x st x in VAR holds
(C[x] implies v.x = F(x)) &
(not C[x] implies v.x = G(x)) from LambdaC;
A106: rng v c= L.c
proof let x; assume x in rng v;
then consider y such that
A107: y in dom v & x = v.y by FUNCT_1:def 5;
reconsider y as Variable by A105,A107;
y in Free 'not' H' or not y in Free 'not' H';
then x = f.y & f.y in L.c or x = e by A104,A105,A107;
hence x in L.c;
end; then
reconsider v as Function of VAR,L.c by A105,FUNCT_2:def 1,RELSET_1:11;
A108: L.c c= M by Th24; then
A109: v in Funcs(VAR,L.c) & v = M!v & Funcs(VAR,L.c) c= Funcs(VAR,M)
by A105,A106,FUNCT_2:def 2,FUNCT_5:63,ZF_LANG1:def 2;
then reconsider v' = v as Element of Funcs(VAR,M) qua non empty set;
consider a2 being Ordinal of W such that
A110: a2 = rho.v' &
(ex f being Function of VAR,M st v' = f &
((ex m being Element of M st m in L.a2 & M,f/(x0,m) |= 'not' H') or
a2 = 0-element_of W & not ex m being Element of M st
M,f/(x0,m) |= 'not' H'))&
for b st
ex f being Function of VAR,M st v' = f &
((ex m being Element of M st m in L.b & M,f/(x0,m) |= 'not' H') or
b = 0-element_of W & not ex m being Element of M st
M,f/(x0,m) |= 'not' H')
holds a2 c= b by A58;
consider f' being Function of VAR,M such that
A111: v' = f' &
((ex m being Element of M st m in L.a2 & M,f'/(x0,m) |= 'not' H') or
a2 = 0-element_of W & not ex m being Element of M st
M,f'/(x0,m) |= 'not' H') by A110;
A112: now assume
A113: not ex m being Element of M st M,f/(x0,m) |= 'not' H';
now let m be Element of M;
A114: not M,f/(x0,m) |= 'not' H' by A113;
now let x1; assume
x1 in Free 'not' H';
then f.x1 = (M!v).x1 & f/(x0,m).x0 = m & (M!v)/(x0,m).x0 = m &
(x1 <> x0 implies f/(x0,m).x1 = f.x1 &
(M!v)/(x0,m).x1 = (M!v).x1)
by A105,A109,ZF_LANG1:def 1;
hence f/(x0,m).x1 = (M!v)/(x0,m).x1;
end;
hence not M,(M!v)/(x0,m) |= 'not' H' by A114,ZF_LANG1:84;
end;
hence a1 = a2 by A89,A109,A111,A113;
end;
now given m being Element of M such that
A115: m in L.a1 & M,f/(x0,m) |= 'not' H';
now let x1; assume
x1 in Free 'not' H';
then f.x1 = (M!v).x1 & f/(x0,m).x0 = m & (M!v)/(x0,m).x0 = m &
(x1 <> x0 implies f/(x0,m).x1 = f.x1 &
(M!v)/(x0,m).x1 = (M!v).x1)
by A105,A109,ZF_LANG1:def 1;
hence f/(x0,m).x1 = (M!v)/(x0,m).x1;
end;
then A116: M,(M!v)/(x0,m) |= 'not' H' by A115,ZF_LANG1:84;
then consider m' being Element of M such that
A117: m' in L.a2 & M,f'/(x0,m') |= 'not' H' by A109,A111;
now let x1; assume
x1 in Free 'not' H';
then f.x1 = (M!v).x1 & f/(x0,m').x0 = m' & (M!v)/(x0,m').x0 = m'
&
(x1 <> x0 implies f/(x0,m').x1 = f.x1 &
(M!v)/(x0,m').x1 = (M!v).x1)
by A105,A109,ZF_LANG1:def 1;
hence f/(x0,m').x1 = f'/(x0,m').x1 by A108,A111,ZF_LANG1:def 2;
end;
then M,f/(x0,m') |= 'not' H' by A117,ZF_LANG1:84;
then a1 c= a2 & a2 c= a1 by A88,A89,A109,A110,A115,A116,A117;
hence a1 = a2 by XBOOLE_0:def 10;
end;
then B in rho.:Funcs(VAR,L.c) & si.c = sup (rho.:Funcs(VAR,L.c)) &
c in dom si & dom (si|a) = dom si /\ a
by A57,A63,A87,A88,A89,A109,A110,A112,FUNCT_1:def 12,ORDINAL4:36,
RELAT_1:90;
then A118: B in si.c & si.c = (si|a).c & c in dom (si|a)
by A104,FUNCT_1:72,ORDINAL2:27,XBOOLE_0:def 3;
then si.c in rng (si|a) & sup (si|a) = sup rng (si|a)
by FUNCT_1:def 5,ORDINAL2:35;
then si.c in sup (si|a) by ORDINAL2:27;
then B in sup (si|a) by A118,ORDINAL1:19;
hence thesis by A86,ORDINAL1:22;
end;
A119: a <> 0-element_of W & a is_limit_ordinal &
(for b st b in a holds P[b]) implies P[a]
proof assume that
A120: a <> 0-element_of W & a is_limit_ordinal and
A121: for b st b in a holds si.b c= ksi.b;
thus si.a c= ksi.a
proof let A such that
A122: A in si.a;
si.a c= sup (si|a) by A83,A120;
then A in sup (si|a) & sup (si|a) = sup rng (si|a)
by A122,ORDINAL2:35;
then consider B such that
A123: B in rng (si|a) & A c= B by ORDINAL2:29;
consider x such that
A124: x in dom (si|a) & B = (si|a).x by A123,FUNCT_1:def 5;
reconsider x as Ordinal by A124,ORDINAL1:23;
A125: dom (si|a) c= a by RELAT_1:87; then
A126: x in a & a in On W by A124,Th8;
then x in On W by ORDINAL1:19;
then reconsider x as Ordinal of W by Th8;
si.x = B & si.x c= ksi.x & dom ksi = On W
by A121,A124,A125,FUNCT_1:70,ORDINAL4:def 3;
then A c= ksi.x & ksi.x in ksi.a
by A69,A123,A126,ORDINAL2:def 16,XBOOLE_1:1;
hence thesis by ORDINAL1:22;
end;
end;
A127: P[a] from Universe_Ind(A81,A82,A119);
A128: ksi is continuous
proof let A,B; assume
A129: A in dom ksi & A <> {} & A is_limit_ordinal & B = ksi.A;
then reconsider a = A as Ordinal of W by A67,Th8;
A c= dom ksi by A129,ORDINAL1:def 2;
then A130: dom (ksi|A) = A & ksi|A is increasing
by A69,ORDINAL4:15,RELAT_1:91;
then A131: sup (ksi|A) is_limes_of ksi|A & sup (ksi|A) = sup rng (ksi|A)
by A129,ORDINAL2:35,ORDINAL4:8;
A132: B = union(ksi|a,a) by A66,A68,A129 .= Union (ksi|a) by Th17
.= union rng (ksi|a) by PROB_1:def 3;
A133: B c= sup (ksi|A)
proof let C; assume C in B;
then consider X such that
A134: C in X & X in rng (ksi|A) by A132,TARSKI:def 4;
consider A1 being Ordinal such that
A135: rng (ksi|A) c= A1 by ORDINAL2:def 8;
reconsider X as Ordinal by A134,A135,ORDINAL1:23;
X in sup (ksi|A) by A131,A134,ORDINAL2:27;
hence C in sup (ksi|A) by A134,ORDINAL1:19;
end;
sup (ksi|A) c= B
proof let C; assume C in sup (ksi|A);
then consider D being Ordinal such that
A136: D in rng (ksi|A) & C c= D by A131,ORDINAL2:29;
consider x such that
A137: x in dom (ksi|A) & D = (ksi|A).x by A136,FUNCT_1:def 5;
reconsider x as Ordinal by A137,ORDINAL1:23;
x in succ x & succ x in A by A129,A130,A137,ORDINAL1:10,41;
then D in (ksi|A).succ x & (ksi|A).succ x in rng (ksi|A)
by A130,A137,FUNCT_1:def 5,ORDINAL2:def 16;
then D in B by A132,TARSKI:def 4;
hence thesis by A136,ORDINAL1:22;
end;
hence thesis by A131,A133,XBOOLE_0:def 10;
end;
now assume x0 in Free H';
thus thesis
proof take gamma = phi*ksi;
ex f being Ordinal-Sequence st f = phi*ksi & f is increasing
by A45,A69,ORDINAL4:13;
hence gamma is increasing & gamma is continuous
by A45,A69,A128,ORDINAL4:17;
let a such that
A138: gamma.a = a & {} <> a;
a in dom gamma & ksi.a in dom phi & a in
dom ksi by ORDINAL4:36;
then ksi.a c= phi.(ksi.a) & a c= ksi.a & phi.(ksi.a) = gamma.a
by A45,A69,FUNCT_1:22,ORDINAL4:10;
then A139: ksi.a = a & phi.a = a by A138,XBOOLE_0:def 10;
A140: L.a c= M by Th24;
let f;
thus M,M!f |= H implies L.a,f |= H
proof assume A141: M,M!f |= H;
now let g be Function of VAR,L.a such that
A142: for k st g.k <> f.k holds x0 = k;
now let k; L.a c= M by Th24;
then M!f = f & M!g = g by ZF_LANG1:def 2;
hence (M!g).k <> (M!f).k implies x0 = k by A142;
end;
then M,(M!g) |= H' by A44,A141,ZF_MODEL:16;
hence L.a,g |= H' by A46,A138,A139;
end;
hence thesis by A44,ZF_MODEL:16;
end;
assume that
A143: L.a,f |= H and
A144: not M,M!f |= H;
consider m being Element of M such that
A145: not M,(M!f)/(x0,m) |= H' by A44,A144,ZF_LANG1:80;
A146: M,(M!f)/(x0,m) |= 'not' H' by A145,ZF_MODEL:14;
A147: M!f in Funcs(VAR,M) & f in Funcs(VAR,L.a) by FUNCT_2:11;
reconsider h = M!f as Element of Funcs(VAR,M) qua non empty set by
FUNCT_2:11;
consider a1 being Ordinal of W such that
A148: a1 = rho.h &
(ex f being Function of VAR,M st h = f &
((ex m being Element of M st m in L.a1 & M,f/(x0,m) |= 'not' H') or
a1 = 0-element_of W & not ex m being Element of M st
M,f/(x0,m) |= 'not' H'))&
for b st
ex f being Function of VAR,M st h = f &
((ex m being Element of M st m in L.b & M,f/(x0,m) |= 'not' H') or
b = 0-element_of W & not ex m being Element of M st
M,f/(x0,m) |= 'not' H')
holds a1 c= b by A58;
consider m being Element of M such that
A149: m in L.a1 & M,(M!f)/(x0,m) |= 'not' H' by A146,A148;
A150: M!f = f by A140,ZF_LANG1:def 2;
then a1 in rho.:Funcs(VAR,L.a) & si.a = sup (rho.:Funcs(VAR,L.a))
by A57,A63,A147,A148,FUNCT_1:def 12;
then a1 in si.a & si.a c= ksi.a by A127,ORDINAL2:27;
then L.a1 c= L.a by A1,A139;
then reconsider m' = m as Element of L.a by A149;
dom ((M!f)/(x0,m)) = VAR & rng ((M!f)/(x0,m)) c= L.a
proof thus
dom ((M!f)/(x0,m)) = VAR by FUNCT_2:def 1;
let x; assume x in rng ((M!f)/(x0,m));
then consider y such that
A151: y in
dom ((M!f)/(x0,m)) & x = ((M!f)/(x0,m)).y by FUNCT_1:def 5;
reconsider y as Variable by A151,FUNCT_2:def 1;
y = x0 or y <> x0;
then x = m' or x = f.y by A150,A151,ZF_LANG1:def 1;
hence thesis;
end;
then reconsider g = (M!f)/(x0,m) as Function of VAR,L.a by FUNCT_2:
def 1,RELSET_1:11;
g.x0 = m' & for y be Variable holds g.y <> f.y implies x0 = y
by A150,ZF_LANG1:def 1;
then (M!f)/(x0,m) = f/(x0,m') by ZF_LANG1:def 1;
then (M!f)/(x0,m) = M!(f/(x0,m')) by A140,ZF_LANG1:def 2;
then not M,M!(f/(x0,m')) |= H' by A149,ZF_MODEL:14;
then not L.a,f/(x0,m') |= H' by A46,A138,A139;
hence contradiction by A44,A143,ZF_LANG1:80;
end;
end;
hence thesis by A47;
end;
thus RT[H] from ZF_Ind(A4,A23,A29,A43);
end;