:: Consequences of the Reflection Theorem
:: by Grzegorz Bancerek
::
:: Received August 13, 1990
:: Copyright (c) 1990-2016 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 XBOOLE_0, ORDINAL1, ZF_LANG, SUBSET_1, NUMBERS, ZF_MODEL, TARSKI,
FUNCT_1, REALSET1, CARD_1, CLASSES2, ZF_REFLE, ORDINAL2, ARYTM_3,
BVFUNC_2, RELAT_1, ZFMISC_1, FUNCT_2, ORDINAL4, FUNCT_5, CARD_3,
CLASSES1, ZFREFLE1, NAT_1;
notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1,
FUNCT_2, BINOP_1, CARD_1, ORDINAL1, XCMPLX_0, NAT_1, ZF_LANG, ZF_MODEL,
ORDINAL2, NUMBERS, CARD_3, FUNCT_5, ORDINAL3, CLASSES1, CLASSES2,
ORDINAL4, ZF_LANG1, ZF_REFLE;
constructors ENUMSET1, WELLORD2, BINOP_1, ORDINAL3, XXREAL_0, XREAL_0, NAT_1,
FUNCT_5, CLASSES1, ZF_MODEL, ZF_LANG1, ZF_REFLE, ORDINAL4, RELSET_1,
NUMBERS;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, ORDINAL2, XREAL_0,
CARD_1, CLASSES2, ZF_LANG, ZF_LANG1, CLASSES1, ORDINAL4, FUNCT_1, NAT_1;
requirements NUMERALS, BOOLE, SUBSET;
begin
reserve H,S for ZF-formula,
x for Variable,
X,Y for set,
i for Element of 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
for e being object holds 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,
va 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 being_a_model_of_ZF implies M |= ZF-axioms;
theorem :: ZFREFLE1:5
M |= ZF-axioms & M is epsilon-transitive implies M is being_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 being_a_model_of_ZF & M1 <==> M2 & M2 is
epsilon-transitive implies M2 is being_a_model_of_ZF;
theorem :: ZFREFLE1:11
dom f in W & rng f c= W implies rng f in W;
theorem :: ZFREFLE1:12
X,Y are_equipotent or card X = card Y implies bool X,bool Y
are_equipotent & card bool X = card bool Y;
theorem :: ZFREFLE1:13
for D being non empty set, Phi being Function of D, Funcs(On W,
On W) st card D in 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:14
for phi being Ordinal-Sequence st phi is increasing holds C+^phi
is increasing;
theorem :: ZFREFLE1:15
for xi being Ordinal-Sequence holds (C+^xi)|A = C+^(xi|A);
theorem :: ZFREFLE1:16
for phi being Ordinal-Sequence st phi is increasing & phi is
continuous holds C+^phi is continuous;
reserve psi for Ordinal-Sequence;
theorem :: ZFREFLE1:17
e in rng psi implies e is Ordinal;
theorem :: ZFREFLE1:18
rng psi c= sup psi;
theorem :: ZFREFLE1:19
A is_cofinal_with B & B is_cofinal_with C implies A is_cofinal_with C;
theorem :: ZFREFLE1:20
A is_cofinal_with B implies B c= A;
theorem :: ZFREFLE1:21
A is_cofinal_with B & B is_cofinal_with A implies A = B;
theorem :: ZFREFLE1:22
dom psi <> {} & dom psi is limit_ordinal & psi is increasing & A
is_limes_of psi implies A is_cofinal_with dom psi;
theorem :: ZFREFLE1:23
succ A is_cofinal_with 1;
theorem :: ZFREFLE1:24
A is_cofinal_with succ B implies ex C st A = succ C;
theorem :: ZFREFLE1:25
A is_cofinal_with B implies (A is limit_ordinal iff B is limit_ordinal
);
theorem :: ZFREFLE1:26
A is_cofinal_with {} implies A = {};
theorem :: ZFREFLE1:27
not On W is_cofinal_with a;
theorem :: ZFREFLE1:28
omega in W & phi is increasing & phi is continuous implies ex b
st a in b & phi.b = b;
theorem :: ZFREFLE1:29
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:30
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:31
Rank a in W;
theorem :: ZFREFLE1:32
a <> {} implies Rank a is non empty Element of W;
theorem :: ZFREFLE1:33
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:34
omega in W implies ex b,M st a in b & M = Rank b & M
is_elementary_subsystem_of W;
theorem :: ZFREFLE1:35
omega in W implies ex a,M st a is_cofinal_with omega & M = Rank
a & M is_elementary_subsystem_of W;
theorem :: ZFREFLE1:36
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:37
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:38
omega in W implies ex b,M st a in b & M = Rank b & M <==> W;
theorem :: ZFREFLE1:39
omega in W implies ex a,M st a is_cofinal_with omega & M = Rank a & M <==> W;
theorem :: ZFREFLE1:40
omega in W implies ex a,M st a is_cofinal_with omega & M = Rank a & M
is being_a_model_of_ZF;
theorem :: ZFREFLE1:41
omega in W & X in W implies ex M st X in M & M in W & M is
being_a_model_of_ZF;