:: Consequences of the Reflection Theorem :: by Grzegorz Bancerek :: :: Received August 13, 1990 :: Copyright (c) 1990-2021 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;