:: The Reflection Theorem
:: by Grzegorz Bancerek
::
:: Received August 10, 1990
:: Copyright (c) 1990-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies CLASSES2, ZF_LANG, FUNCT_1, SUBSET_1, ZF_MODEL, TARSKI, ORDINAL1,
XBOOLE_0, ZFMISC_1, CARD_1, BVFUNC_2, XBOOLEAN, ZFMODEL1, RELAT_1,
ORDINAL2, ORDINAL4, CARD_3, CLASSES1, NUMBERS, NAT_1, ARYTM_3, XXREAL_0,
REALSET1, FUNCT_2, ZF_REFLE, CARD_FIL, CARD_5;
notations TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, CARD_1, ORDINAL1, XCMPLX_0,
NAT_1, RELAT_1, FUNCT_1, RELSET_1, FUNCT_2, ZF_MODEL, ZFMODEL1, ORDINAL2,
NUMBERS, CARD_3, CLASSES1, CLASSES2, ZF_LANG, ORDINAL4, ZF_LANG1, CARD_5,
CARD_FIL, CARD_LAR, XXREAL_0;
constructors ENUMSET1, WELLORD2, XXREAL_0, XREAL_0, NAT_1, CLASSES1, CARD_3,
ORDINAL4, ZF_MODEL, ZFMODEL1, ZF_LANG1, RELSET_1, CARD_LAR, CARD_FIL,
CARD_5, NUMBERS;
registrations SUBSET_1, FUNCT_1, ORDINAL1, RELSET_1, ORDINAL2, XREAL_0,
CARD_1, CLASSES2, ZF_LANG, ZF_LANG1, CLASSES1, ORDINAL4, CARD_5,
CARD_LAR, CARD_3, RELAT_1;
requirements NUMERALS, BOOLE, SUBSET;
definitions TARSKI, FUNCT_1, ZF_LANG, ZF_MODEL, WELLORD2, ORDINAL2, RELAT_1,
XBOOLE_0, ORDINAL1;
equalities ZF_LANG, ORDINAL2, XBOOLE_0, ORDINAL1;
expansions TARSKI, ORDINAL2, XBOOLE_0;
theorems TARSKI, ZFMISC_1, NAT_1, FUNCT_1, FUNCT_2, ORDINAL1, ORDINAL2,
ORDINAL3, ORDINAL4, CARD_1, CLASSES1, CLASSES2, ZF_LANG, ZF_MODEL,
CARD_3, ZFMODEL1, FUNCT_5, ZF_LANG1, RELAT_1, RELSET_1, XBOOLE_0,
XBOOLE_1, XCMPLX_1, FUNCT_7, CARD_LAR;
schemes CLASSES1, PARTFUN1, ORDINAL1, ORDINAL2, ZF_LANG, CARD_2, NAT_1;
begin
reserve W for Universe,
H for ZF-formula,
x,y,z,X for set,
k for Variable,
f for Function of VAR,W,
u,v for Element of W;
theorem Th1:
W |= the_axiom_of_pairs
proof
for u,v holds {u,v} in W;
hence thesis by ZFMODEL1:2;
end;
theorem Th2:
W |= the_axiom_of_unions
proof
for u holds union u in W;
hence thesis by ZFMODEL1:4;
end;
theorem Th3:
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;
succ A in omega by A1,ORDINAL1:28;
then succ A c= u 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:6;
then v c= w & v <> w by ORDINAL1:def 2;
hence v c< w & w in u by A1,ORDINAL1:28;
end;
hence thesis by ZFMODEL1:6;
end;
theorem Th4:
W |= the_axiom_of_power_sets
proof
for u holds W /\ bool u in W by CLASSES1:def 1,XBOOLE_1:17;
hence thesis by ZFMODEL1:8;
end;
theorem Th5:
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 and
W,f |= All(x.3,Ex(x.0,All(x.4,H <=> x.4 '=' x.0)));
let u;
card u in card W by CLASSES2:1;
then card (def_func'(H,f).:u) in card W by CARD_1:67,ORDINAL1:12;
hence thesis by CLASSES1:1;
end;
hence thesis by ZFMODEL1:15;
end;
theorem Th6:
omega in W implies W is being_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 Th1,Th2,Th3,Th4,Th5;
end;
reserve F for Function,
A,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;
scheme
ALFA9Universe { 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
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 ORDINAL1:sch 6(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] and
A7: for B st P[d,B] holds A c= B by A5;
consider a being Ordinal of W() such that
A8: P[d,a] by A1;
A c= a by A7,A8;
then reconsider a = A as Ordinal of W() by CLASSES1:def 1;
take a;
thus thesis by A6,A7;
end;
theorem
x is Ordinal of W iff x in On W by ORDINAL1:def 9;
reserve psi for Ordinal-Sequence;
scheme
OrdSeqOfUnivEx { W()->Universe, P[object,object] }:
ex phi being Ordinal-Sequence
of W() st for a being Ordinal of W() holds P[a,phi.a]
provided
A1: for a being Ordinal of W() ex b being Ordinal of W() st P[a,b];
defpred Q[object,object] means P[$1,$2] & $2 is Ordinal of W();
A2: for x being object st x in On W() ex y being object st Q[x,y]
proof
let x be object;
assume x in On W();
then reconsider a = x as Ordinal of W() by ORDINAL1:def 9;
consider b being Ordinal of W() such that
A3: P[a,b] by A1;
reconsider y = b as set;
take y;
thus thesis by A3;
end;
consider f being Function such that
A4: dom f = On W() &
for x being object st x in On W() holds Q[x,f.x] from CLASSES1:
sch 1(A2);
reconsider phi = f as Sequence by A4,ORDINAL1:def 7;
A5: rng phi c= On W()
proof
let x be object;
assume x in rng phi;
then ex y being object st y in dom phi & x = phi.y by FUNCT_1:def 3;
then reconsider x as Ordinal of W() by A4;
x in W();
hence thesis by ORDINAL1:def 9;
end;
then reconsider phi as Ordinal-Sequence by ORDINAL2:def 4;
reconsider phi as Ordinal-Sequence of W() by A4,A5,FUNCT_2:def 1,RELSET_1:4;
take phi;
let a be Ordinal of W();
a in On W() by ORDINAL1:def 9;
hence thesis by A4;
end;
scheme
UOSExist { W()->Universe, a()->Ordinal of W(), C(Ordinal,Ordinal)->Ordinal
of W(), D(Ordinal,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
consider phi being Ordinal-Sequence such that
A1: dom phi = On W() and
A2: 0 in On W() implies phi.0 = 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 <> 0 & A is limit_ordinal holds phi.A = D(
A,phi|A) from ORDINAL2:sch 11;
rng phi c= On W()
proof
let x be object;
assume x in rng phi;
then consider y being object such that
A5: y in dom phi and
A6: x = phi.y by FUNCT_1:def 3;
reconsider y as Ordinal of W() by A1,A5,ORDINAL1:def 9;
A7: now
assume not ex A st y = succ A;
then
A8: y is limit_ordinal by ORDINAL1:29;
assume y <> {};
then x = D(y,phi|y) by A1,A4,A5,A6,A8;
hence thesis by ORDINAL1:def 9;
end;
now
given A such that
A9: y = succ A;
reconsider B = phi.A as Ordinal;
x = C(A,B) by A1,A3,A5,A6,A9;
hence thesis by ORDINAL1:def 9;
end;
hence thesis by A2,A6,A7,ORDINAL1:def 9;
end;
then reconsider phi as Ordinal-Sequence of W() by A1,FUNCT_2:def 1,RELSET_1:4
;
take phi;
0-element_of W() in dom phi by ORDINAL4:34;
hence phi.0-element_of W() = a() by A1,A2,ORDINAL4:33;
thus for a being Ordinal of W() holds phi.(succ a) = C(a,phi.a) by A1,A3,
ORDINAL4:34;
let a be Ordinal of W();
a in dom phi & {} = 0-element_of W() by ORDINAL4:33,34;
hence thesis by A4;
end;
scheme
UniverseInd { 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: for A st A <> 0 & A is limit_ordinal & for B st B in A holds Q[B]
holds Q[A]
proof
let A such that
A5: A <> 0 & A is limit_ordinal and
A6: 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 A6,ORDINAL4:33;
hence thesis by A3,A5;
end;
A7: for A st Q[A] holds Q[succ A]
proof
let A such that
A8: A is Ordinal of W() implies P[A] and
A9: succ A is Ordinal of W();
A in succ A & succ A in On W() by A9,ORDINAL1:6,def 9;
then A in On W() by ORDINAL1:10;
then reconsider a = A as Ordinal of W() by ORDINAL1:def 9;
P[succ a] by A2,A8;
hence thesis;
end;
A10: Q[0] by A1,ORDINAL4:33;
Q[A] from ORDINAL2:sch 1(A10,A7,A4);
hence thesis;
end;
definition
let f be Function, W be Universe, a be Ordinal of W;
func union(f,a) -> set equals
Union (W|`(f|Rank a));
correctness;
end;
theorem Th8:
for L being Sequence,A holds L|Rank A is Sequence
proof
let L be Sequence, A;
A1: dom(L|Rank A) = dom L /\ Rank A by RELAT_1:61;
now
let X;
assume
A2: X in dom(L|Rank A);
then
A3: X in dom L by A1,XBOOLE_0:def 4;
hence X is Ordinal;
X in Rank A by A1,A2,XBOOLE_0:def 4;
then
A4: X c= Rank A by ORDINAL1:def 2;
X c= dom L by A3,ORDINAL1:def 2;
hence X c= dom(L|Rank A) by A1,A4,XBOOLE_1:19;
end;
then dom(L|Rank A) is epsilon-transitive epsilon-connected set
by ORDINAL1:19;
hence thesis by ORDINAL1:31;
end;
theorem Th9:
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 Sequence by Th8;
consider B such that
A1: rng L c= B by ORDINAL2:def 4;
rng K c= rng L by RELAT_1:70;
then rng K c= B by A1;
hence thesis by ORDINAL2:def 4;
end;
theorem
Union psi is Ordinal;
theorem Th11:
Union (X|`psi) is epsilon-transitive epsilon-connected set
proof
consider A such that
A1: rng psi c= A by ORDINAL2:def 4;
A2: rng (X|`psi) c= rng psi by RELAT_1:87;
A3: now
let x be object;
assume x in rng (X|`psi);
then x in A by A1,A2;
hence x is Ordinal;
end;
Union (X|`psi) = union rng (X|`psi) by CARD_3:def 4;
hence thesis by A3,ORDINAL1:23;
end;
theorem Th12:
On Rank A = A
proof
thus On Rank A c= A
proof
let x be object;
assume
A1: x in On Rank A;
then reconsider B = x as Ordinal by ORDINAL1:def 9;
x in Rank A by A1,ORDINAL1:def 9;
then the_rank_of B in A by CLASSES1:66;
hence thesis by CLASSES1:73;
end;
On A c= On Rank A by CLASSES1:38,ORDINAL2:9;
hence thesis by ORDINAL2:8;
end;
theorem Th13:
psi|Rank A = psi|A
proof
dom (psi|Rank A) c= dom psi by RELAT_1:60;
then
On dom (psi|Rank A) c= On Rank A & On dom (psi|Rank A) = dom (psi| Rank
A) by ORDINAL2:9,ORDINAL3:6,RELAT_1:58;
then
A1: dom (psi|Rank A) c= A by Th12;
A c= Rank A by CLASSES1:38;
then (psi|Rank A)|A = psi|A by FUNCT_1:51;
hence thesis by A1,RELAT_1:68;
end;
definition
let phi be Ordinal-Sequence, W be Universe, a be Ordinal of W;
redefine func union(phi,a) -> Ordinal of W; :: redefines union (ZF_REFLE, definition)
coherence
proof
reconsider K = phi|Rank a as Ordinal-Sequence by Th9;
reconsider A = Union (W|`K) as Ordinal by Th11;
a in On W by ORDINAL1:def 9;
then dom K c= Rank a & Rank a in W by CLASSES2:25,RELAT_1:58;
then dom (W|`K) c= dom K & dom K in W by CLASSES1:def 1,FUNCT_1:56;
then dom (W|`K) in W by CLASSES1:def 1;
then
A1: card dom (W|`K) in card W by CLASSES2:1;
(W|`K).:dom(W|`K) = rng(W|`K) by RELAT_1:113;
then rng (W|`K) c= W & card rng (W|`K) in card W
by A1,CARD_1:67,ORDINAL1:12,RELAT_1:85;
then
A2: rng (W|`K) in W by CLASSES1:1;
union rng (W|`K) = Union (W|`K) by CARD_3:def 4;
then A in W by A2,CLASSES2:59;
hence thesis;
end;
end;
theorem Th14:
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;
On W c= W by ORDINAL2:7;
then rng (phi|a) c= rng phi & rng phi c= W by RELAT_1:70;
then a c= Rank a & phi|a = W|`(phi|a) by CLASSES1:38,RELAT_1:94,XBOOLE_1:1;
hence thesis by Th13,FUNCT_1:51;
end;
definition
let W be Universe, a,b be Ordinal of W;
redefine func a \/ b -> Ordinal of W; :: redefines \/ (XBOOLE_0, definition)
coherence
proof
a c= b or b c= a;
hence thesis by XBOOLE_1:12;
end;
end;
registration
let W;
cluster non empty for Element of W;
existence
proof
set u = the Element of W;
{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 Sequence of W;
attr IT is DOMAIN-yielding means
: Def2:
dom IT = On W;
end;
registration
let W;
cluster DOMAIN-yielding non-empty for Sequence of W;
existence
proof
set D = the non empty Element of W;
deffunc F(set) = D;
consider L being Sequence such that
A1: dom L = On W & for A for L1 being Sequence st A in On W & L1 = L
|A holds L.A = F(L1) from ORDINAL1:sch 4;
rng L c= W
proof
let x be object;
assume x in rng L;
then consider y being object such that
A2: y in dom L and
A3: x = L.y by FUNCT_1:def 3;
reconsider y as Ordinal by A2;
L|y = L|y;
then x = D by A1,A2,A3;
hence thesis;
end;
then reconsider L as Sequence of W by RELAT_1:def 19;
take L;
thus dom L = On W by A1;
assume {} in rng L;
then consider x being object such that
A4: x in dom L and
A5: {} = L.x by FUNCT_1:def 3;
reconsider x as Ordinal by A4;
L|x = L|x;
hence contradiction by A1,A4,A5;
end;
end;
definition
let W;
mode DOMAIN-Sequence of W is non-empty DOMAIN-yielding Sequence of W;
end;
definition
let W;
let L be DOMAIN-Sequence of W;
redefine func Union L -> Subclass of W; :: redefines Union (CARD_3, definition)
coherence
proof
set a = the Ordinal of W;
a in On W by ORDINAL1:def 9;
then a in dom L by Def2;
then L.a in rng L by FUNCT_1:def 3;
then L.a c= union rng L & L.a <> {} by ZFMISC_1:74;
then union rng L <> {};
then reconsider S = Union L as non empty set by CARD_3:def 4;
rng L c= W & Union L = union rng L by CARD_3:def 4;
then
A1: Union L c= union W by ZFMISC_1:77;
S c= W
proof
let x be object;
assume x in S;
then consider X such that
A2: x in X and
A3: X in W by A1,TARSKI:def 4;
X c= W by A3,ORDINAL1:def 2;
hence thesis by A2;
end;
hence thesis;
end;
let a;
redefine func L.a -> non empty Element of W; :: redefines . (FUNCT_1, definition)
coherence
proof
a in On W by ORDINAL1:def 9;
then a in dom L by Def2;
then
A4: L.a in rng L by FUNCT_1:def 3;
thus thesis by A4,RELAT_1:def 9;
end;
end;
reserve L for DOMAIN-Sequence of W,
n for Element of NAT,
f for Function of VAR,L.a;
theorem Th15:
a in dom L
proof
a in On W by ORDINAL1:def 9;
hence thesis by Def2;
end;
theorem Th16:
L.a c= Union L
proof
a in dom L by Th15;
then
A1: L.a in rng L by FUNCT_1:def 3;
union rng L = Union L by CARD_3:def 4;
hence thesis by A1,ZFMISC_1:74;
end;
theorem Th17:
NAT,VAR are_equipotent
proof
deffunc F(Nat,set) = 5+($1+1);
consider f being sequence of NAT such that
A1: f.0 = 5+0 & for n being Nat holds f.(n+1) = F(n,f.n) from NAT_1:sch
12;
A2: now
let n;
(ex j be Nat st n = j+1) implies f.n = 5+n by A1;
then n = 0 or f.n = 5+n by NAT_1:6;
hence f.n = 5+n by A1;
end;
A3: dom f = NAT by FUNCT_2:def 1;
thus NAT,VAR are_equipotent
proof
reconsider g = f as Function;
take g;
thus g is one-to-one
proof
let x,y be object;
assume x in dom g & y in dom g;
then reconsider n1 = x, n2 = y as Element of NAT by FUNCT_2:def 1;
f.n1 = 5+n1 & f.n2 = 5+n2 by A2;
hence thesis by XCMPLX_1:2;
end;
thus dom g = NAT by FUNCT_2:def 1;
thus rng g c= VAR
proof
let x be object;
assume x in rng g;
then consider y being object such that
A4: y in dom f and
A5: x = f.y by FUNCT_1:def 3;
reconsider y as Element of NAT by A4;
A6: 5+y >= 5 by NAT_1:11;
x = 5+y by A2,A5;
hence thesis by A6;
end;
let x be object;
assume x in VAR;
then ex n st x = n & 5 <= n;
then consider n be Nat such that
A7: x = 5+n by NAT_1:10;
A8: n in NAT by ORDINAL1:def 12;
then f.n = x by A2,A7;
hence thesis by A3,A8,FUNCT_1:def 3;
end;
end;
theorem
sup X c= succ union On X by ORDINAL3:72;
theorem Th19:
X in W implies sup X in W
proof
reconsider a = union On X as Ordinal by ORDINAL3:5;
A1: On X c= X by ORDINAL2:7;
assume X in W;
then On X in W by A1,CLASSES1:def 1;
then reconsider a as Ordinal of W by CLASSES2:59;
sup X c= succ a by ORDINAL3:72;
hence thesis by CLASSES1:def 1;
end;
reserve x1 for Variable;
::$N Reflection Theorem
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 that
A1: omega in W and
A2: for a,b st a in b holds L.a c= L.b and
A3: for a st a <> {} & a is limit_ordinal holds L.a = Union (L|a);
set M = Union L;
A4: union rng L = M by CARD_3:def 4;
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;
A5: dom L = On W by Def2;
A6: for H st H is universal & RT[the_scope_of H] holds RT[H]
proof
deffunc D(Ordinal of W, Ordinal-Sequence) = union($2,$1);
let H;
set x0 = bound_in H;
set H9 = the_scope_of H;
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' H9) or $2 = 0-element_of
W & not ex m being Element of M st M,f/(x0,m) |= 'not' H9);
assume H is universal;
then
A7: H = All(bound_in H,the_scope_of H) by ZF_LANG:44;
A8: 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' H9;
hence thesis;
end;
suppose
A9: not for m being Element of M holds not M,f/(x0,m) |= 'not' H9;
thus thesis
proof
consider m being Element of M such that
A10: M,f/(x0,m) |= 'not' H9 by A9;
consider X be set such that
A11: m in X and
A12: X in rng L by A4,TARSKI:def 4;
consider x being object such that
A13: x in dom L and
A14: X = L.x by A12,FUNCT_1:def 3;
reconsider x as Ordinal by A13;
reconsider b = x as Ordinal of W by A5,A13,ORDINAL1:def 9;
take b, f;
thus thesis by A10,A11,A14;
end;
end;
end;
hence thesis;
end;
consider rho being Function such that
A15: dom rho = Funcs(VAR,M) qua non empty set and
A16: 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 ALFA9Universe(A8);
defpred SI[Ordinal of W,Ordinal of W] means $2 = sup (rho.:Funcs(VAR,L.$1)
);
A17: for a ex b st SI[a, b]
proof
let a;
set X = rho.:Funcs(VAR,L.a);
A18: X c= W
proof
let x be object;
assume x in X;
then consider h being object such that
h in dom rho and
A19: h in Funcs(VAR,L.a) and
A20: x = rho.h by FUNCT_1:def 6;
Funcs(VAR,L.a) c= Funcs(VAR,M) by Th16,FUNCT_5:56;
then reconsider h as Element of Funcs(VAR,M) qua non empty set by A19;
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' H9) or a =
0-element_of W & not ex m being Element of M st M,f/(x0,m) |= 'not' H9)) & 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' H9) or b = 0-element_of W & not ex m being Element of
M st M,f/(x0,m) |= 'not' H9) holds a c= b by A16;
hence thesis by A20;
end;
Funcs(omega,L.a) in W by A1,CLASSES2:61;
then
A21: card Funcs(omega,L.a) in card W by CLASSES2:1;
card VAR = card omega & card(L.a) = card(L.a) by Th17,CARD_1:5;
then card Funcs(VAR,L.a) = card Funcs(omega,L.a) by FUNCT_5:61;
then card X in card W by A21,CARD_1:67,ORDINAL1:12;
then X in W by A18,CLASSES1:1;
then reconsider b = sup X as Ordinal of W by Th19;
take b;
thus thesis;
end;
consider si being Ordinal-Sequence of W such that
A22: for a holds SI[a, si.a] from OrdSeqOfUnivEx(A17);
deffunc C(Ordinal of W, Ordinal of W) = succ((si.succ $1) \/ $2);
consider ksi being Ordinal-Sequence of W such that
A23: ksi.0-element_of W = si.0-element_of W and
A24: for a holds ksi.(succ a) = C(a,ksi.a) and
A25: for a st a <> 0-element_of W & a is limit_ordinal holds ksi.a =
D(a,ksi|a) from UOSExist;
defpred P[Ordinal] means si.$1 c= ksi.$1;
given phi such that
A26: phi is increasing and
A27: phi is continuous and
A28: 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;
A29: ksi is increasing
proof
let A,B;
assume that
A30: A in B and
A31: B in dom ksi;
A in dom ksi by A30,A31,ORDINAL1:10;
then reconsider a = A, b = B as Ordinal of W by A31,ORDINAL1:def 9;
defpred Theta[Ordinal of W] means a in $1 implies ksi.a in ksi.$1;
A32: Theta[c] implies Theta[succ c]
proof
assume that
A33: a in c implies ksi.a in ksi.c and
A34: a in succ c;
A35: a c= c by A34,ORDINAL1:22;
A36: ksi.a in ksi.c or ksi.a = ksi.c
proof
per cases;
suppose
a <> c;
then a c< c by A35;
hence thesis by A33,ORDINAL1:11;
end;
suppose
a = c;
hence thesis;
end;
end;
A37: ksi.c c= (si.succ c) \/ ksi.c by XBOOLE_1:7;
ksi.succ c = succ((si.succ c) \/ ksi.c) & (si.succ c) \/ ksi.c
in succ((si. succ c) \/ ksi.c) by A24,ORDINAL1:22;
hence thesis by A37,A36,ORDINAL1:10,12;
end;
A38: 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
ksi.succ a = succ((si.succ a) \/ ksi.a) by A24;
then (si.succ a) \/ ksi.a in ksi.succ a by ORDINAL1:6;
then
A39: ksi.a in ksi.succ a by ORDINAL1:12,XBOOLE_1:7;
let b such that
A40: b <> 0-element_of W and
A41: b is limit_ordinal and
for c st c in b holds Theta[c] and
A42: a in b;
succ a in dom ksi & succ a in b by A41,A42,ORDINAL1:28,ORDINAL4:34;
then
A43: ksi.succ a in rng(ksi|b) by FUNCT_1:50;
ksi.b = union(ksi|b,b) by A25,A40,A41
.= Union (ksi|b) by Th14
.= union rng (ksi|b) by CARD_3:def 4;
hence thesis by A43,A39,TARSKI:def 4;
end;
A44: Theta[0-element_of W] by ORDINAL4:33;
Theta[c] from UniverseInd(A44,A32,A38);
then ksi.a in ksi.b by A30;
hence thesis;
end;
A45: 0-element_of W = {} by ORDINAL4:33;
A46: ksi is continuous
proof
let A,B;
assume that
A47: A in dom ksi and
A48: A <> 0 and
A49: A is limit_ordinal and
A50: B = ksi.A;
A c= dom ksi by A47,ORDINAL1:def 2;
then
A51: dom (ksi|A) = A by RELAT_1:62;
reconsider a = A as Ordinal of W by A47,ORDINAL1:def 9;
A52: B = union(ksi|a,a) by A25,A45,A48,A49,A50
.= Union (ksi|a) by Th14
.= union rng (ksi|a) by CARD_3:def 4;
A53: B c= sup (ksi|A)
proof
let C;
assume C in B;
then consider X such that
A54: C in X and
A55: X in rng (ksi|A) by A52,TARSKI:def 4;
rng(ksi|A) c= rng ksi by RELAT_1:70;
then X in rng ksi by A55;
then reconsider X as Ordinal;
X in sup (ksi|A) by A55,ORDINAL2:19;
hence thesis by A54,ORDINAL1:10;
end;
A56: ksi|A is increasing by A29,ORDINAL4:15;
A57: sup (ksi|A) c= B
proof
let C;
assume C in sup (ksi|A);
then consider D being Ordinal such that
A58: D in rng (ksi|A) and
A59: C c= D by ORDINAL2:21;
consider x being object such that
A60: x in dom (ksi|A) and
A61: D = (ksi|A).x by A58,FUNCT_1:def 3;
reconsider x as Ordinal by A60;
A62: succ x in A by A49,A60,ORDINAL1:28;
then
A63: (ksi|A).succ x in rng (ksi|A) by A51,FUNCT_1:def 3;
x in succ x by ORDINAL1:6;
then D in (ksi|A).succ x by A51,A56,A61,A62;
then D in B by A52,A63,TARSKI:def 4;
hence thesis by A59,ORDINAL1:12;
end;
sup (ksi|A) is_limes_of ksi|A by A48,A49,A51,A56,ORDINAL4:8;
hence thesis by A53,A57,XBOOLE_0:def 10;
end;
A64: a <> 0-element_of W & a is limit_ordinal implies si.a c= sup (si|a)
proof
defpred C[object] means $1 in Free 'not' H9;
assume that
A65: a <> 0-element_of W and
A66: a is limit_ordinal;
A67: si.a = sup (rho.:Funcs(VAR,L.a)) by A22;
let A;
assume A in si.a;
then consider B such that
A68: B in rho.:Funcs(VAR,L.a) and
A69: A c= B by A67,ORDINAL2:21;
consider x being object such that
A70: x in dom rho and
A71: x in Funcs(VAR,L.a) and
A72: B = rho.x by A68,FUNCT_1:def 6;
reconsider h = x as Element of Funcs(VAR,M) qua non empty set by A15,A70;
consider a1 being Ordinal of W such that
A73: a1 = rho.h and
A74: 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' H9) or a1 = 0-element_of W & not ex m
being Element of M st M,f/(x0,m) |= 'not' H9) and
A75: 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' H9) or b = 0-element_of W & not
ex m being Element of M st M,f/(x0,m) |= 'not' H9) holds a1 c= b by A16;
consider f being Function of VAR,M such that
A76: h = f and
A77: (ex m being Element of M st m in L.a1 & M,f/(x0,m) |= 'not' H9
) or a1 = 0-element_of W & not ex m being Element of M st M,f/(x0,m) |= 'not'
H9 by A74;
defpred P[object,object] means
for a st f.$1 in L.a holds f.$2 in L.a;
A78: now
A79: for x,y being object holds P[x,y] or P[y,x]
proof
let x,y be object;
given a such that
A80: f.x in L.a & not f.y in L.a;
let b such that
A81: f.y in L.b;
a in b or a = b or b in a by ORDINAL1:14;
then L.a c= L.b or L.b c= L.a by A2;
hence thesis by A80,A81;
end;
assume Free 'not' H9 <> {};
then
A82: Free 'not' H9 <> {};
A83: L.a = Union (L|a) & Union (L|a) = union rng (L|a ) by A3,A45,A65,A66,
CARD_3:def 4;
A84: for x,y,z being object st P[x,y] & P[y,z] holds P[x,z];
consider z being object such that
A85: z in Free 'not' H9 &
for y being object st y in Free 'not' H9 holds P[z,y
] from CARD_2:sch 2(A82,A79,A84);
reconsider z as Variable by A85;
A86: dom (L|a) c= a by RELAT_1:58;
A87: ex s being Function st f = s & dom s = VAR & rng s c= L.a by A71,A76,
FUNCT_2:def 2;
then f.z in rng f by FUNCT_1:def 3;
then consider X such that
A88: f.z in X and
A89: X in rng (L|a) by A87,A83,TARSKI:def 4;
consider x being object such that
A90: x in dom (L|a) and
A91: X = (L|a).x by A89,FUNCT_1:def 3;
A92: (L|a).x = L.x by A90,FUNCT_1:47;
reconsider x as Ordinal by A90;
a in On W by ORDINAL1:def 9;
then x in On W by A90,A86,ORDINAL1:10;
then reconsider x as Ordinal of W by ORDINAL1:def 9;
take x;
thus x in a by A90,A86;
let y be Variable;
assume y in Free 'not' H9;
hence f.y in L.x by A85,A88,A91,A92;
end;
now
assume
A93: Free 'not' H9 = {};
take b = 0-element_of W;
thus b in a by A45,A65,ORDINAL3:8;
thus for x1 st x1 in Free 'not' H9 holds f.x1 in L.b by A93;
end;
then consider c such that
A94: c in a and
A95: for x1 st x1 in Free 'not' H9 holds f.x1 in L.c by A78;
A96: si.c = sup (rho.:Funcs(VAR,L.c)) by A22;
c in dom si & dom (si|a) = dom si /\ a by ORDINAL4:34,RELAT_1:61;
then
A97: c in dom (si|a) by A94,XBOOLE_0:def 4;
si.c = (si|a).c by A94,FUNCT_1:49;
then si.c in rng (si|a) by A97,FUNCT_1:def 3;
then
A98: si.c in sup (si|a) by ORDINAL2:19;
deffunc F(object) = f.$1;
set e = the Element of L.c;
deffunc G(object) = e;
consider v being Function such that
A99: dom v = VAR & for x being object st x in VAR
holds (C[x] implies v.x = F(x)
) & (not C[x] implies v.x = G(x)) from PARTFUN1:sch 1;
A100: rng v c= L.c
proof
let x be object;
assume x in rng v;
then consider y being object such that
A101: y in dom v and
A102: x = v.y by FUNCT_1:def 3;
reconsider y as Variable by A99,A101;
y in Free 'not' H9 or not y in Free 'not' H9;
then x = f.y & f.y in L.c or x = e by A95,A99,A102;
hence thesis;
end;
then reconsider v as Function of VAR,L.c by A99,FUNCT_2:def 1,RELSET_1:4;
A103: v in Funcs(VAR,L.c) by A99,A100,FUNCT_2:def 2;
Funcs(VAR,L.c) c= Funcs(VAR,M) by Th16,FUNCT_5:56;
then reconsider
v9 = v as Element of Funcs(VAR,M) qua non empty set by A103;
consider a2 being Ordinal of W such that
A104: a2 = rho.v9 and
A105: ex f being Function of VAR,M st v9 = f & ((ex m being Element
of M st m in L.a2 & M,f/(x0,m) |= 'not' H9) or a2 = 0-element_of W & not ex m
being Element of M st M,f/(x0,m) |= 'not' H9) and
A106: for b st ex f being Function of VAR,M st v9 = f & ((ex m being
Element of M st m in L.b & M,f/(x0,m) |= 'not' H9) or b = 0-element_of W & not
ex m being Element of M st M,f/(x0,m) |= 'not' H9) holds a2 c= b by A16;
consider f9 being Function of VAR,M such that
A107: v9 = f9 and
A108: (ex m being Element of M st m in L.a2 & M,f9/(x0,m) |= 'not'
H9) or a2 = 0-element_of W & not ex m being Element of M st M,f9/(x0,m) |=
'not' H9 by A105;
A109: v = M!v by Th16,ZF_LANG1:def 1;
A110: now
given m being Element of M such that
A111: m in L.a1 and
A112: M,f/(x0,m) |= 'not' H9;
A113: now
let x1;
A114: f/(x0,m).x0 = m by FUNCT_7:128;
A115: x1 <> x0 implies f/(x0,m).x1 = f.x1 & (M!v)/(x0,m).x1 = (M!v).
x1 by FUNCT_7:32;
assume x1 in Free 'not' H9;
hence f/(x0,m).x1 = (M!v)/(x0,m).x1 by A99,A109,A114,A115,FUNCT_7:128
;
end;
then M,(M!v)/(x0,m) |= 'not' H9 by A112,ZF_LANG1:75;
then consider m9 being Element of M such that
A116: m9 in L.a2 & M,f9/(x0,m9) |= 'not' H9 by A109,A107,A108;
now
let x1;
A117: f/(x0,m9).x0 = m9 by FUNCT_7:128;
A118: x1 <> x0 implies f/(x0,m9).x1 = f.x1 & (M!v)/(x0,m9).x1 = (M!v
).x1 by FUNCT_7:32;
assume x1 in Free 'not' H9;
hence f/(x0,m9).x1 = f9/(x0,m9).x1 by A99,A109,A107,A117,A118,
FUNCT_7:128;
end;
then
A119: a1 c= a2 by A75,A76,A116,ZF_LANG1:75;
a2 c= a1 by A109,A106,A111,A112,A113,ZF_LANG1:75;
hence a1 = a2 by A119;
end;
now
assume
A120: not ex m being Element of M st M,f/(x0,m) |= 'not' H9;
now
let m be Element of M;
now
let x1;
A121: f/(x0,m).x0 = m by FUNCT_7:128;
A122: x1 <> x0 implies f/(x0,m).x1 = f.x1 & (M!v)/(x0,m).x1 = (M!v
).x1 by FUNCT_7:32;
assume x1 in Free 'not' H9;
hence f/(x0,m).x1 = (M!v)/(x0,m).x1 by A99,A109,A121,A122,
FUNCT_7:128;
end;
hence not M,(M!v)/(x0,m) |= 'not' H9 by A120,ZF_LANG1:75;
end;
hence a1 = a2 by A77,A109,A107,A108,A120;
end;
then B in rho.:Funcs(VAR,L.c) by A15,A72,A73,A74,A76,A103,A104,A110,
FUNCT_1:def 6;
then B in si.c by A96,ORDINAL2:19;
then B in sup (si|a) by A98,ORDINAL1:10;
hence thesis by A69,ORDINAL1:12;
end;
A123: a <> 0-element_of W & a is limit_ordinal & (for b st b in a holds P[
b]) implies P[a]
proof
assume that
A124: a <> 0-element_of W & a is limit_ordinal and
A125: for b st b in a holds si.b c= ksi.b;
thus si.a c= ksi.a
proof
A126: si.a c= sup (si|a) by A64,A124;
let A;
assume A in si.a;
then consider B such that
A127: B in rng (si|a) and
A128: A c= B by A126,ORDINAL2:21;
consider x being object such that
A129: x in dom (si|a) and
A130: B = (si|a).x by A127,FUNCT_1:def 3;
reconsider x as Ordinal by A129;
A131: a in On W by ORDINAL1:def 9;
x in dom si by A129,RELAT_1:57;
then x in On W;
then reconsider x as Ordinal of W by ORDINAL1:def 9;
A132: si.x = B by A129,A130,FUNCT_1:47;
A133: si.x c= ksi.x by A125,A129;
dom ksi = On W by FUNCT_2:def 1;
then ksi.x in ksi.a by A29,A129,A131;
hence thesis by A128,A132,A133,ORDINAL1:12,XBOOLE_1:1;
end;
end;
A134: 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)) by A24,ORDINAL1:6;
then si.succ a in ksi.succ a by ORDINAL1:12,XBOOLE_1:7;
hence si.succ a c= ksi.succ a by ORDINAL1:def 2;
end;
A135: P[0-element_of W] by A23;
A136: P[a] from UniverseInd(A135,A134,A123);
A137: now
assume x0 in Free H9;
thus thesis
proof
take gamma = phi*ksi;
ex f being Ordinal-Sequence st f = phi*ksi & f is increasing by A26,A29
,ORDINAL4:13;
hence gamma is increasing & gamma is continuous by A27,A29,A46,
ORDINAL4:17;
let a such that
A138: gamma.a = a and
A139: {} <> a;
let f;
a in dom gamma by ORDINAL4:34;
then
A140: phi.(ksi.a) = gamma.a by FUNCT_1:12;
a in dom ksi by ORDINAL4:34;
then
A141: a c= ksi.a by A29,ORDINAL4:10;
ksi.a in dom phi by ORDINAL4:34;
then
A142: ksi.a c= phi.(ksi.a) by A26,ORDINAL4:10;
then
A143: ksi.a = a by A138,A141,A140;
A144: phi.a = a by A138,A142,A141,A140,XBOOLE_0:def 10;
thus M,M!f |= H implies L.a,f |= H
proof
assume
A145: M,M!f |= H;
now
let g be Function of VAR,L.a such that
A146: for k st g.k <> f.k holds x0 = k;
now
let k;
M!f = f & M!g = g by Th16,ZF_LANG1:def 1;
hence (M!g).k <> (M!f).k implies x0 = k by A146;
end;
then M,(M!g) |= H9 by A7,A145,ZF_MODEL:16;
hence L.a,g |= H9 by A28,A139,A144;
end;
hence thesis by A7,ZF_MODEL:16;
end;
assume that
A147: L.a,f |= H and
A148: not M,M!f |= H;
consider m being Element of M such that
A149: not M,(M!f)/(x0,m) |= H9 by A7,A148,ZF_LANG1:71;
A150: si.a c= ksi.a by A136;
A151: si.a = sup (rho.:Funcs(VAR,L.a)) by A22;
reconsider h = M!f as Element of Funcs(VAR,M) qua non empty set by
FUNCT_2:8;
consider a1 being Ordinal of W such that
A152: a1 = rho.h and
A153: 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' H9) or a1 = 0-element_of W & not ex m
being Element of M st M,f/(x0,m) |= 'not' H9) and
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' H9) or b = 0-element_of W & not
ex m being Element of M st M,f/(x0,m) |= 'not' H9) holds a1 c= b by A16;
A154: M!f = f by Th16,ZF_LANG1:def 1;
M,(M!f)/(x0,m) |= 'not' H9 by A149,ZF_MODEL:14;
then consider m being Element of M such that
A155: m in L.a1 and
A156: M,(M!f)/(x0,m) |= 'not' H9 by A153;
f in Funcs(VAR,L.a) by FUNCT_2:8;
then a1 in rho.:Funcs(VAR,L.a) by A15,A152,A154,FUNCT_1:def 6;
then a1 in si.a by A151,ORDINAL2:19;
then L.a1 c= L.a by A2,A143,A150;
then reconsider m9 = m as Element of L.a by A155;
(M!f)/(x0,m) = M!(f/(x0,m9)) by A154,Th16,ZF_LANG1:def 1;
then not M,M!(f/(x0,m9)) |= H9 by A156,ZF_MODEL:14;
then not L.a,f/(x0,m9) |= H9 by A28,A139,A144;
hence contradiction by A7,A147,ZF_LANG1:71;
end;
end;
now
assume
A157: not x0 in Free H9;
thus thesis
proof
take phi;
thus phi is increasing & phi is continuous by A26,A27;
let a such that
A158: phi.a = a & {} <> a;
let f;
thus M,M!f |= H implies L.a,f |= H
proof
A159: for k st (M!f).k <> (M!f).k holds x0 = k;
assume M,M!f |= H;
then M,M!f |= H9 by A7,A159,ZF_MODEL:16;
then L.a,f |= H9 by A28,A158;
hence thesis by A7,A157,ZFMODEL1:10;
end;
A160: for k st f.k <> f.k holds x0 = k;
assume L.a,f |= H;
then L.a,f |= H9 by A7,A160,ZF_MODEL:16;
then M,M!f |= H9 by A28,A158;
hence thesis by A7,A157,ZFMODEL1:10;
end;
end;
hence thesis by A137;
end;
A161: 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
A162: H = (the_left_argument_of H) '&' (the_right_argument_of H) by ZF_LANG:40;
given fi1 being Ordinal-Sequence of W such that
A163: fi1 is increasing and
A164: fi1 is continuous and
A165: 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
A166: fi2 is increasing and
A167: fi2 is continuous and
A168: 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 A163,A166,ORDINAL4:13;
hence phi is increasing & phi is continuous by A163,A164,A167,ORDINAL4:17;
let a such that
A169: phi.a = a and
A170: {} <> a;
a in dom fi1 by ORDINAL4:34;
then
A171: a c= fi1.a by A163,ORDINAL4:10;
let f;
A172: a in dom phi by ORDINAL4:34;
A173: a in dom fi2 by ORDINAL4:34;
A174: now
assume fi1.a <> a;
then a c< fi1.a by A171;
then
A175: a in fi1.a by ORDINAL1:11;
A176: phi.a = fi2.(fi1.a) by A172,FUNCT_1:12;
fi1.a in dom fi2 by ORDINAL4:34;
then fi2.a in fi2.(fi1.a) by A166,A175;
hence contradiction by A166,A169,A173,A176,ORDINAL1:5,ORDINAL4:10;
end;
then
A177: fi2.a = a by A169,A172,FUNCT_1:12;
thus M,M!f |= H implies L.a,f |= H
proof
assume
A178: M,M!f |= H;
then M,M!f |= the_right_argument_of H by A162,ZF_MODEL:15;
then
A179: L.a,f |= the_right_argument_of H by A168,A170,A177;
M,M!f |= the_left_argument_of H by A162,A178,ZF_MODEL:15;
then L.a,f |= the_left_argument_of H by A165,A170,A174;
hence thesis by A162,A179,ZF_MODEL:15;
end;
assume
A180: L.a,f |= H;
then L.a,f |= the_right_argument_of H by A162,ZF_MODEL:15;
then
A181: M,M!f |= the_right_argument_of H by A168,A170,A177;
L.a,f |= the_left_argument_of H by A162,A180,ZF_MODEL:15;
then M,M!f |= the_left_argument_of H by A165,A170,A174;
hence thesis by A162,A181,ZF_MODEL:15;
end;
A182: for H st H is atomic holds RT[H]
proof
A183: dom id On W = On W;
then reconsider phi = id On W as Sequence by ORDINAL1:def 7;
A184: rng id On W = On W;
reconsider phi as Ordinal-Sequence;
reconsider phi as Ordinal-Sequence of W by A183,A184,FUNCT_2:def 1
,RELSET_1:4;
let H such that
A185: H is being_equality or H is being_membership;
take phi;
thus
A186: phi is increasing
proof
let A,B;
assume
A187: A in B & B in dom phi;
then phi.A = A by FUNCT_1:18,ORDINAL1:10;
hence thesis by A187,FUNCT_1:18;
end;
thus phi is continuous
proof
let A,B;
assume that
A188: A in dom phi and
A189: A <> 0 & A is limit_ordinal and
A190: B = phi.A;
A191: A c= dom phi by A188,ORDINAL1:def 2;
phi|A = phi*(id A) by RELAT_1:65
.= id((dom phi) /\ A) by FUNCT_1:22
.= id A by A191,XBOOLE_1:28;
then
A192: rng(phi|A) = A;
phi.A = A by A188,FUNCT_1:18;
then
A193: sup(phi|A) = B by A190,A192,ORDINAL2:18;
A194: phi|A is increasing by A186,ORDINAL4:15;
dom (phi|A) = A by A191,RELAT_1:62;
hence thesis by A189,A193,A194,ORDINAL4:8;
end;
let a such that
phi.a = a and
{} <> a;
let f;
thus M,M!f |= H implies L.a,f |= H
proof
assume
A195: M,M!f |= H;
A196: M!f = f by Th16,ZF_LANG1:def 1;
A197: now
assume H is being_membership;
then
A198: H = (Var1 H) 'in' (Var2 H) by ZF_LANG:37;
then (M!f).Var1 H in (M!f).Var2 H by A195,ZF_MODEL:13;
hence thesis by A196,A198,ZF_MODEL:13;
end;
now
assume H is being_equality;
then
A199: H = (Var1 H) '=' (Var2 H) by ZF_LANG:36;
then (M!f).Var1 H = (M!f).Var2 H by A195,ZF_MODEL:12;
hence thesis by A196,A199,ZF_MODEL:12;
end;
hence thesis by A185,A197;
end;
assume
A200: L.a,f |= H;
A201: M!f = f by Th16,ZF_LANG1:def 1;
A202: now
assume H is being_membership;
then
A203: H = (Var1 H) 'in' (Var2 H) by ZF_LANG:37;
then f.Var1 H in f.Var2 H by A200,ZF_MODEL:13;
hence thesis by A201,A203,ZF_MODEL:13;
end;
now
assume H is being_equality;
then
A204: H = (Var1 H) '=' (Var2 H) by ZF_LANG:36;
then f.Var1 H = f.Var2 H by A200,ZF_MODEL:12;
hence thesis by A201,A204,ZF_MODEL:12;
end;
hence thesis by A185,A202;
end;
A205: for H st H is negative & RT[the_argument_of H] holds RT[H]
proof
let H;
assume H is negative;
then
A206: H = 'not' the_argument_of H by ZF_LANG:def 30;
given phi such that
A207: phi is increasing & phi is continuous and
A208: 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 A207;
let a such that
A209: phi.a = a & {} <> a;
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 by A206,ZF_MODEL:14;
then not L.a,f |= the_argument_of H by A208,A209;
hence thesis by A206,ZF_MODEL:14;
end;
assume L.a,f |= H;
then not L.a,f |= the_argument_of H by A206,ZF_MODEL:14;
then not M,M!f |= the_argument_of H by A208,A209;
hence thesis by A206,ZF_MODEL:14;
end;
thus RT[H] from ZF_LANG:sch 1(A182,A205,A161,A6);
end;
begin :: Addenda
:: from CARD_LAR, 2010.03.11, A.T.
reserve M for non countable Aleph;
theorem
M is strongly_inaccessible implies Rank M is being_a_model_of_ZF
proof
assume M is strongly_inaccessible;
then
A1: Rank M is Universe by CARD_LAR:38;
omega c= M;
then omega c< M;
then
A2: omega in M by ORDINAL1:11;
M c= Rank M by CLASSES1:38;
hence thesis by A1,A2,Th6;
end;