Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990 Association of Mizar Users

### Consequences of the Reflection Theorem

by
Grzegorz Bancerek

MML identifier: ZFREFLE1
[ Mizar article, MML identifier index ]

```environ

vocabulary ZF_LANG, ZF_MODEL, QMAX_1, BOOLE, FUNCT_1, QC_LANG1, CLASSES2,
ORDINAL1, ZF_REFLE, ORDINAL2, CARD_1, FINSET_1, RELAT_1, CLASSES1,
TARSKI, FUNCT_2, ORDINAL4, FUNCT_5, PROB_1, ZFREFLE1;
notation TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1,
FUNCT_2, FINSET_1, NUMBERS, NAT_1, ORDINAL1, ZF_LANG, ZF_MODEL, WELLORD2,
CARD_1, ORDINAL2, PROB_1, FUNCT_5, ORDINAL3, CLASSES1, CLASSES2,
ORDINAL4, ZF_LANG1, ZF_REFLE;
constructors ENUMSET1, NAT_1, ZF_MODEL, WELLORD2, FUNCT_5, ORDINAL3, CLASSES1,
ZF_LANG1, ZF_REFLE, MEMBERED, PARTFUN1, RELAT_2, XBOOLE_0;
clusters ORDINAL1, ZF_LANG, ORDINAL2, CLASSES2, ZF_LANG1, RELSET_1, ORDINAL3,
CARD_1, ZFMISC_1, FUNCT_2, PARTFUN1, XBOOLE_0;
requirements NUMERALS, BOOLE, SUBSET;

begin

reserve H,S for ZF-formula,
x for Variable,
X,Y for set,
i for Nat,
e,u for set;

definition let M be non empty set, F be Subset of WFF;
pred M |= F means
:: ZFREFLE1:def 1
for H st H in F holds M |= H;
end;

definition let M1,M2 be non empty set;
pred M1 <==> M2 means
:: ZFREFLE1:def 2
for H st Free H = {} holds M1 |= H iff M2 |= H;
reflexivity;
symmetry;
pred M1 is_elementary_subsystem_of M2 means
:: ZFREFLE1:def 3
M1 c= M2 &
for H for v being Function of VAR,M1 holds M1,v |= H iff M2,M2!v |= H;
reflexivity;
end;

definition
func ZF-axioms -> set means
:: ZFREFLE1:def 4
e in it iff e in WFF & (e = the_axiom_of_extensionality or
e = the_axiom_of_pairs or e = the_axiom_of_unions or
e = the_axiom_of_infinity or e = the_axiom_of_power_sets or
ex H st {x.0,x.1,x.2} misses Free H &
e = the_axiom_of_substitution_for H);
end;

definition
redefine func ZF-axioms -> Subset of WFF;
end;

reserve M,M1,M2 for non empty set,
f for Function,
v1 for Function of VAR,M1,
v2 for Function of VAR,M2,
F,F1,F2 for Subset of WFF,
W for Universe,
a,b,c for Ordinal of W,
A,B,C for Ordinal,
L for DOMAIN-Sequence of W,
v_a for Function of VAR,L.a,
phi,xi for Ordinal-Sequence of W;

theorem :: ZFREFLE1:1
M |= {} WFF;

theorem :: ZFREFLE1:2
F1 c= F2 & M |= F2 implies M |= F1;

theorem :: ZFREFLE1:3
M |= F1 & M |= F2 implies M |= F1 \/ F2;

theorem :: ZFREFLE1:4
M is_a_model_of_ZF implies M |= ZF-axioms;

theorem :: ZFREFLE1:5
M |= ZF-axioms & M is epsilon-transitive implies M is_a_model_of_ZF;

theorem :: ZFREFLE1:6
ex S st Free S = {} & for M holds M |= S iff M |= H;

theorem :: ZFREFLE1:7
M1 <==> M2 iff for H holds M1 |= H iff M2 |= H;

theorem :: ZFREFLE1:8
M1 <==> M2 iff for F holds M1 |= F iff M2 |= F;

theorem :: ZFREFLE1:9
M1 is_elementary_subsystem_of M2 implies M1 <==> M2;

theorem :: ZFREFLE1:10
M1 is_a_model_of_ZF & M1 <==> M2 & M2 is epsilon-transitive implies
M2 is_a_model_of_ZF;

scheme NonUniqFuncEx { X() -> set, P[set,set] }:
ex f being Function st dom f = X() & for e st e in X() holds P[e,f.e]
provided
for e st e in X() ex u st P[e,u];

canceled;

theorem :: ZFREFLE1:12
dom f in W & rng f c= W implies rng f in W;

theorem :: ZFREFLE1:13
X,Y are_equipotent or Card X = Card Y implies
bool X,bool Y are_equipotent & Card bool X = Card bool Y;

theorem :: ZFREFLE1:14
for D being non empty set, Phi being Function of D, Funcs(On W, On W) st
Card D <` Card W
ex phi st phi is increasing & phi is continuous &
phi.0-element_of W = 0-element_of W &
(for a holds phi.succ a = sup ({phi.a} \/ (uncurry Phi).:[:D,{succ a}:])) &
(for a st a <> 0-element_of W & a is_limit_ordinal holds
phi.a = sup (phi|a));

theorem :: ZFREFLE1:15
for phi being Ordinal-Sequence st
phi is increasing holds C+^phi is increasing;

theorem :: ZFREFLE1:16
for xi being Ordinal-Sequence holds (C+^xi)|A = C+^(xi|A);

theorem :: ZFREFLE1:17
for phi being Ordinal-Sequence st
phi is increasing & phi is continuous holds C+^phi is continuous;

definition let A,B be Ordinal;
pred A is_cofinal_with B means
:: ZFREFLE1:def 5
ex xi being Ordinal-Sequence st
dom xi = B & rng xi c= A & xi is increasing & A = sup xi;
reflexivity;
end;

reserve psi for Ordinal-Sequence;

canceled;

theorem :: ZFREFLE1:19
e in rng psi implies e is Ordinal;

theorem :: ZFREFLE1:20
rng psi c= sup psi;

theorem :: ZFREFLE1:21
A is_cofinal_with B & B is_cofinal_with C implies A is_cofinal_with C;

theorem :: ZFREFLE1:22
A is_cofinal_with B implies B c= A;

theorem :: ZFREFLE1:23
A is_cofinal_with B & B is_cofinal_with A implies A = B;

theorem :: ZFREFLE1:24
dom psi <> {} & dom psi is_limit_ordinal & psi is increasing &
A is_limes_of psi implies A is_cofinal_with dom psi;

theorem :: ZFREFLE1:25
succ A is_cofinal_with one;

theorem :: ZFREFLE1:26
A is_cofinal_with succ B implies ex C st A = succ C;

theorem :: ZFREFLE1:27
A is_cofinal_with B implies (A is_limit_ordinal iff B is_limit_ordinal);

theorem :: ZFREFLE1:28
A is_cofinal_with {} implies A = {};

theorem :: ZFREFLE1:29
not On W is_cofinal_with a;

theorem :: ZFREFLE1:30
omega in W & phi is increasing & phi is continuous implies
ex b st a in b & phi.b = b;

theorem :: ZFREFLE1:31
omega in W & phi is increasing & phi is continuous implies
ex a st b in a & phi.a = a & a is_cofinal_with omega;

theorem :: ZFREFLE1:32
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
ex phi st phi is increasing & phi is continuous &
for a st phi.a = a & {} <> a holds
L.a is_elementary_subsystem_of Union L;

theorem :: ZFREFLE1:33
Rank a in W;

theorem :: ZFREFLE1:34
a <> {} implies Rank a is non empty Element of W;

theorem :: ZFREFLE1:35
omega in W implies ex phi st phi is increasing & phi is continuous &
for a,M st phi.a = a & {} <> a & M = Rank a holds
M is_elementary_subsystem_of W;

theorem :: ZFREFLE1:36
omega in W implies ex b,M st a in b & M = Rank b &
M is_elementary_subsystem_of W;

theorem :: ZFREFLE1:37
omega in W implies ex a,M st a is_cofinal_with omega & M = Rank a &
M is_elementary_subsystem_of W;

theorem :: ZFREFLE1:38
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
ex phi st phi is increasing & phi is continuous &
for a st phi.a = a & {} <> a holds L.a <==> Union L;

theorem :: ZFREFLE1:39
omega in W implies ex phi st phi is increasing & phi is continuous &
for a,M st phi.a = a & {} <> a & M = Rank a holds M <==> W;

theorem :: ZFREFLE1:40
omega in W implies ex b,M st a in b & M = Rank b & M <==> W;

theorem :: ZFREFLE1:41
omega in W implies ex a,M st a is_cofinal_with omega & M = Rank a & M <==> W;

theorem :: ZFREFLE1:42
omega in W implies ex a,M st a is_cofinal_with omega & M = Rank a &
M is_a_model_of_ZF;

theorem :: ZFREFLE1:43
omega in W & X in W implies ex M st X in M & M in W & M is_a_model_of_ZF;
```