Volume 2, 1990

University of Bialystok

Copyright (c) 1990 Association of Mizar Users

### The abstract of the Mizar article:

### Consequences of the Reflection Theorem

**by****Grzegorz Bancerek**- Received August 13, 1990
- 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;

Back to top