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;