ZFREFLE1

:: Consequences of the Reflection Theorem
::  by Grzegorz Bancerek
::
:: Received August 13, 1990
:: Copyright (c) 1990-2026 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;
 definitions TARSKI, ORDINAL2, ZF_MODEL, ORDINAL1, XBOOLE_0;
 equalities ORDINAL2, BINOP_1, ORDINAL4;
 expansions TARSKI, ORDINAL2, XBOOLE_0;
 theorems TARSKI, ZFMISC_1, FUNCT_1, FUNCT_2, FUNCT_5, ORDINAL1, ORDINAL2,
      ORDINAL3, ORDINAL4, CARD_1, CARD_2, CLASSES1, CLASSES2, ZF_LANG, CARD_3,
      ZF_MODEL, ZFMODEL1, ZF_LANG1, ZF_REFLE, RELAT_1, RELSET_1, XBOOLE_0,
      XBOOLE_1, XCMPLX_1;
 schemes NAT_1, ORDINAL2, ORDINAL4, ZF_REFLE, FUNCT_1, XBOOLE_0;

begin

Lm1: {} in omega by ORDINAL1:def 11;

Lm2: omega is limit_ordinal by ORDINAL1:def 11;

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

  for H st H in F holds M |= H;
end;

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

defpred ZFAx[object] means $1 = the_axiom_of_extensionality or $1 =
the_axiom_of_pairs or $1 = the_axiom_of_unions or $1 = the_axiom_of_infinity or
$1 = the_axiom_of_power_sets or ex H st {x.0,x.1,x.2} misses Free H & $1 =
the_axiom_of_substitution_for H;

definition
  func ZF-axioms -> set means
  : Def4:
  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);
  existence
  proof
    thus ex X st for e being object holds e in X iff e in WFF & ZFAx[e] from
    XBOOLE_0:sch 1;
  end;
  uniqueness
  proof
    defpred P[object] means $1 in WFF & ZFAx[$1];
    let X1,X2 be set such that
A1: for e being object holds e in X1 iff P[e] and
A2: for e being object holds e in X2 iff P[e];
    thus thesis from XBOOLE_0:sch 2(A1,A2);
  end;
end;

definition
  redefine func ZF-axioms -> Subset of WFF;  :: redefines ZF-axioms (ZFREFLE1, definition)
  coherence
  proof
    ZF-axioms c= WFF
    by Def4;
    hence thesis;
  end;
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
  M |= {} WFF;

theorem
  F1 c= F2 & M |= F2 implies M |= F1;

theorem
  M |= F1 & M |= F2 implies M |= F1 \/ F2
proof
  assume
A1: M |= F1 & M |= F2;
  let H;
  assume H in F1 \/ F2;
  then H in F1 or H in F2 by XBOOLE_0:def 3;
  hence thesis by A1;
end;

theorem Th4:
  M is being_a_model_of_ZF implies M |= ZF-axioms
proof
  assume
A1: M is epsilon-transitive & M |= the_axiom_of_pairs & M |=
  the_axiom_of_unions & M |= the_axiom_of_infinity &( M |=
  the_axiom_of_power_sets & for H st {x.0,x.1,x.2} misses Free H holds M |=
  the_axiom_of_substitution_for H);
  let H;
  assume H in ZF-axioms;
  then H = the_axiom_of_extensionality or H = the_axiom_of_pairs or H =
the_axiom_of_unions or H = the_axiom_of_infinity or H = the_axiom_of_power_sets
  or ex H1 being ZF-formula st {x.0,x.1,x.2} misses Free H1 & H =
  the_axiom_of_substitution_for H1 by Def4;
  hence thesis by A1,ZFMODEL1:1;
end;

theorem Th5:
  M |= ZF-axioms & M is epsilon-transitive implies M is being_a_model_of_ZF
proof
  the_axiom_of_power_sets in WFF by ZF_LANG:4;
  then
A1: the_axiom_of_power_sets in ZF-axioms by Def4;
  the_axiom_of_infinity in WFF by ZF_LANG:4;
  then
A2: the_axiom_of_infinity in ZF-axioms by Def4;
  the_axiom_of_unions in WFF by ZF_LANG:4;
  then
A3: the_axiom_of_unions in ZF-axioms by Def4;
  assume that
A4: for H st H in ZF-axioms holds M |= H and
A5: M is epsilon-transitive;
  the_axiom_of_pairs in WFF by ZF_LANG:4;
  then the_axiom_of_pairs in ZF-axioms by Def4;
  hence M is epsilon-transitive & M |= the_axiom_of_pairs & M |=
the_axiom_of_unions & M |= the_axiom_of_infinity & M |= the_axiom_of_power_sets
  by A4,A5,A3,A2,A1;
  let H;
  assume
A6: {x.0,x.1,x.2} misses Free H;
  the_axiom_of_substitution_for H in WFF by ZF_LANG:4;
  then the_axiom_of_substitution_for H in ZF-axioms by A6,Def4;
  hence thesis by A4;
end;

theorem Th6:
  ex S st Free S = {} & for M holds M |= S iff M |= H
proof
  defpred P[Nat] means for H st card Free H = $1 ex S st Free S =
  {} & for M holds M |= S iff M |= H;
A1: for i being Nat holds P[i] implies P[i+1]
  proof let i be Nat;
    assume
A2: P[i];
    let H;
    set e = the Element of Free H;
    assume
A3: card Free H = i+1;
    then
A4: Free H <> {};
    then reconsider x = e as Variable by TARSKI:def 3;
A5: {x} c= Free H by A4,ZFMISC_1:31;
A6: Free All(x,H) = Free H \ {x} by ZF_LANG1:62;
    x in {x} by ZFMISC_1:31;
    then
A7: not x in Free All(x,H) by A6,XBOOLE_0:def 5;
    Free All(x,H) \/ {x} = Free H \/ {x} by A6,XBOOLE_1:39;
    then Free All(x,H) \/ {x} = Free H by A5,XBOOLE_1:12;
    then card Free All(x,H) + 1 = card Free H by A7,CARD_2:41;
    then consider S such that
A8: Free S = {} and
A9: for M holds M |= S iff M |= All(x,H) by A2,A3,XCMPLX_1:2;
    take S;
    thus Free S = {} by A8;
    let M;
    M |= H iff M |= All(x,H) by ZF_MODEL:23;
    hence thesis by A9;
  end;
A10: card Free H = card Free H;
A11: P[0]
  proof
    let H;
    assume
A12: card Free H = 0;
    take H;
    thus thesis by A12;
  end;
  for i being Nat holds P[i] from NAT_1:sch 2(A11,A1);
  hence thesis by A10;
end;

theorem
  M1 <==> M2 iff for H holds M1 |= H iff M2 |= H
proof
  thus M1 <==> M2 implies for H holds M1 |= H iff M2 |= H
  proof
    assume
A1: for H st Free H = {} holds M1 |= H iff M2 |= H;
    let H;
    consider S such that
A2: Free S = {} and
A3: for M holds M |= S iff M |= H by Th6;
    M1 |= S iff M2 |= S by A1,A2;
    hence thesis by A3;
  end;
  assume
A4: for H holds M1 |= H iff M2 |= H;
  let H;
  thus thesis by A4;
end;

theorem Th8:
  M1 <==> M2 iff for F holds M1 |= F iff M2 |= F
proof
  thus M1 <==> M2 implies for F holds M1 |= F iff M2 |= F
  proof
    assume
A1: for H st Free H = {} holds M1 |= H iff M2 |= H;
    let F;
    thus M1 |= F implies M2 |= F
    proof
      assume
A2:   H in F implies M1 |= H;
      let H;
      consider S such that
A3:   Free S = {} and
A4:   for M holds M |= S iff M |= H by Th6;
      assume H in F;
      then M1 |= H by A2;
      then M1 |= S by A4;
      then M2 |= S by A1,A3;
      hence thesis by A4;
    end;
    assume
A5: H in F implies M2 |= H;
    let H;
    consider S such that
A6: Free S = {} and
A7: for M holds M |= S iff M |= H by Th6;
    assume H in F;
    then M2 |= H by A5;
    then M2 |= S by A7;
    then M1 |= S by A1,A6;
    hence thesis by A7;
  end;
  assume
A8: M1 |= F iff M2 |= F;
  let H such that
  Free H = {};
  H in WFF by ZF_LANG:4;
  then reconsider F = {H} as Subset of WFF by ZFMISC_1:31;
  thus M1 |= H implies M2 |= H
  proof
    assume M1 |= H;
    then S in F implies M1 |= S by TARSKI:def 1;
    then M1 |= F;
    then
A9: M2 |= F by A8;
    H in F by TARSKI:def 1;
    hence thesis by A9;
  end;
  assume M2 |= H;
  then S in F implies M2 |= S by TARSKI:def 1;
  then M2 |= F;
  then
A10: M1 |= F by A8;
  H in F by TARSKI:def 1;
  hence thesis by A10;
end;

theorem Th9:
  M1 is_elementary_subsystem_of M2 implies M1 <==> M2
proof
  assume that
  M1 c= M2 and
A1: for H for v being Function of VAR,M1 holds M1,v |= H iff M2,M2!v |= H;
  let H such that
A2: Free H = {};
  thus M1 |= H implies M2 |= H
  proof
    assume
A3: M1,v1 |= H;
    set v1 = the Function of VAR,M1;
    M1,v1 |= H by A3;
    then
A4: M2,M2!v1 |= H by A1;
    let v2;
    for x st x in Free H holds v2.x = (M2!v1).x by A2;
    hence thesis by A4,ZF_LANG1:75;
  end;
  assume
A5: M2,v2 |= H;
  let v1;
  M2,M2!v1 |= H by A5;
  hence thesis by A1;
end;

theorem Th10:
  M1 is being_a_model_of_ZF & M1 <==> M2 & M2 is
  epsilon-transitive implies M2 is being_a_model_of_ZF
proof
  assume that
A1: M1 is being_a_model_of_ZF and
A2: M1 <==> M2;
  M1 |= ZF-axioms by A1,Th4;
  then M2 |= ZF-axioms by A2,Th8;
  hence thesis by Th5;
end;

theorem Th11:
  dom f in W & rng f c= W implies rng f in W
proof
  assume dom f in W;
  then rng f = f.:(dom f) & card dom f in card W by CLASSES2:1,RELAT_1:113;
  then card rng f in card W by CARD_1:67,ORDINAL1:12;
  hence thesis by CLASSES1:1;
end;

theorem
  X,Y are_equipotent or card X = card Y implies bool X,bool Y
  are_equipotent & card bool X = card bool Y
proof
  assume X,Y are_equipotent or card X = card Y;
  then X,Y are_equipotent by CARD_1:5;
  then
A1: card Funcs(X,{0,1}) = card Funcs(Y,{0,1}) by FUNCT_5:60;
  card Funcs(X,{0,1}) = card bool X & card Funcs(Y,{0,1}) = card bool Y by
FUNCT_5:65;
  hence thesis by A1,CARD_1:5;
end;

theorem Th13:
  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)
proof
  deffunc D(set,Sequence) = sup $2;
  let D be non empty set, Phi be Function of D, Funcs(On W, On W) such that
A1: card D in card W;
  deffunc C(Ordinal,Ordinal) = sup ({$2} \/ (uncurry Phi).:[:D,{succ $1}:]);
  consider L be Ordinal-Sequence such that
A2: dom L = On W & (0 in On W implies L.0 = 0) and
A3: for A st succ A in On W holds L.succ A = C(A,L.A) and
A4: for A st A in On W & A <> 0 & A is limit_ordinal holds L.A = D(A,L|
  A) from ORDINAL2:sch 11;
  defpred P[Ordinal] means L.$1 in On W;
A5: for a st P[a] holds P[succ a]
  proof
    let a;
A6: On W c= W by ORDINAL2:7;
    assume L.a in On W;
    then reconsider b = L.a as Ordinal of W by ZF_REFLE:7;
    card [:D,{succ a}:] = card D by CARD_1:69;
    then card ((uncurry Phi).:[:D,{succ a}:]) c= card D by CARD_1:66;
    then
A7: card ((uncurry Phi).:[:D,{succ a}:]) in card W by A1,ORDINAL1:12;
    rng Phi c= Funcs(On W, On W) by RELAT_1:def 19;
    then
A8: rng uncurry Phi c= On W by FUNCT_5:41;
    (uncurry Phi).:[:D,{succ a}:] c= rng uncurry Phi by RELAT_1:111;
    then (uncurry Phi).:[:D,{succ a}:] c= On W by A8;
    then (uncurry Phi).:[:D,{succ a}:] c= W by A6;
    then (uncurry Phi).:[:D,{succ a}:] in W by A7,CLASSES1:1;
    then
A9: {b} \/ (uncurry Phi).:[:D,{succ a}:] in W by CLASSES2:60;
    succ a in On W by ZF_REFLE:7;
    then L.succ a = sup ({b} \/ (uncurry Phi).:[:D,{succ a}:]) by A3;
    then L.succ a in W by A9,ZF_REFLE:19;
    hence thesis by ORDINAL1:def 9;
  end;
A10: for a st a <> 0-element_of W & a is limit_ordinal & for b st b in a
  holds P[b] holds P[a]
  proof
    let a such that
A11: a <> 0-element_of W & a is limit_ordinal and
A12: for b st b in a holds L.b in On W;
A13: dom (L|a) c= a by RELAT_1:58;
    then
A14: dom (L|a) in W by CLASSES1:def 1;
A15: a in On W by ZF_REFLE:7;
A16: rng (L|a) c= W
    proof
      let e be object;
      assume e in rng (L|a);
      then consider u being object such that
A17:  u in dom (L|a) and
A18:  e = (L|a).u by FUNCT_1:def 3;
      reconsider u as Ordinal by A17;
      u in On W by A15,A13,A17,ORDINAL1:10;
      then reconsider u as Ordinal of W by ZF_REFLE:7;
      e = L.u by A17,A18,FUNCT_1:47;
      then e in On W by A12,A13,A17;
      hence thesis by ORDINAL1:def 9;
    end;
    L.a = sup (L|a) by A4,A11,A15;
    then L.a in W by A14,A16,Th11,ZF_REFLE:19;
    hence thesis by ORDINAL1:def 9;
  end;
A19: P[0-element_of W] by A2,ORDINAL1:def 9;
  rng L c= On W
  proof
    let e be object;
    assume e in rng L;
    then consider u being object such that
A20: u in dom L and
A21: e = L.u by FUNCT_1:def 3;
    reconsider u as Ordinal of W by A2,A20,ZF_REFLE:7;
    P[a] from ZF_REFLE:sch 4(A19,A5,A10);
    then L.u in On W;
    hence thesis by A21;
  end;
  then reconsider phi = L as Ordinal-Sequence of W by A2,FUNCT_2:def 1
,RELSET_1:4;
  take phi;
  thus
A22: phi is increasing
  proof
    let A,B;
    assume that
A23: A in B and
A24: B in dom phi;
    A in dom phi by A23,A24,ORDINAL1:10;
    then reconsider a = A, b = B as Ordinal of W by A2,A24,ZF_REFLE:7;
    defpred Q[Ordinal] means a in $1 implies phi.a in phi.$1;
A25: for b st Q[b] holds Q[succ b]
    proof
      let b such that
A26:  ( a in b implies phi.a in phi.b)& a in succ b;
      phi.b in {phi.b} by TARSKI:def 1;
      then
A27:  phi.b in {phi.b} \/ (uncurry Phi).:[:D,{succ b}:] by XBOOLE_0:def 3;
      succ b in On W by ZF_REFLE:7;
      then phi.succ b = sup({phi.b} \/ (uncurry Phi).:[:D,{succ b}:]) by A3;
      then phi.b in phi.succ b by A27,ORDINAL2:19;
      hence thesis by A26,ORDINAL1:8,10;
    end;
A28: for b st b <> 0-element_of W & b is limit_ordinal & for c st c in b
    holds Q[c] holds Q[b]
    proof
      let b such that
A29:  b <> 0-element_of W & b is limit_ordinal and
      for c st c in b holds a in c implies phi.a in phi.c and
A30:  a in b;
      b in On W by ZF_REFLE:7;
      then
A31:  phi.b = sup (phi|b) by A4,A29;
      a in On W by ZF_REFLE:7;
      then phi.a in rng (phi|b) by A2,A30,FUNCT_1:50;
      hence phi.a in phi.b by A31,ORDINAL2:19;
    end;
A32: Q[0-element_of W];
    for b holds Q[b] from ZF_REFLE:sch 4(A32,A25,A28);
    then phi.a in phi.b by A23;
    hence thesis;
  end;
  thus phi is continuous
  proof
    let A,B;
    assume that
A33: A in dom phi and
A34: A <> 0 & A is limit_ordinal and
A35: B = phi.A;
    A c= dom phi by A33,ORDINAL1:def 2;
    then
A36: dom (phi|A) = A by RELAT_1:62;
A37: phi|A is increasing by A22,ORDINAL4:15;
    B = sup (phi|A) by A2,A4,A33,A34,A35;
    hence thesis by A34,A36,A37,ORDINAL4:8;
  end;
  thus phi.0-element_of W = 0-element_of W by A2,ORDINAL1:def 9;
  thus for a holds phi.succ a = sup ({phi.a} \/ (uncurry Phi).:[:D,{succ a}:] )
  by A3,ZF_REFLE:7;
  let a;
  a in On W by ZF_REFLE:7;
  hence thesis by A4;
end;

theorem Th14:
  for phi being Ordinal-Sequence st phi is increasing holds C+^phi
  is increasing
proof
  let phi be Ordinal-Sequence such that
A1: phi is increasing;
  let A,B;
  set xi = C+^phi;
  assume that
A2: A in B and
A3: B in dom xi;
  reconsider A9 = phi.A, B9 = phi.B as Ordinal;
A4: dom xi = dom phi by ORDINAL3:def 1;
  then
A5: xi.B = C+^B9 by A3,ORDINAL3:def 1;
  A in dom xi by A2,A3,ORDINAL1:10;
  then
A6: xi.A = C+^A9 by A4,ORDINAL3:def 1;
  A9 in B9 by A1,A2,A3,A4;
  hence thesis by A6,A5,ORDINAL2:32;
end;

theorem Th15:
  for xi being Ordinal-Sequence holds (C+^xi)|A = C+^(xi|A)
proof
  let xi be Ordinal-Sequence;
A1: dom (xi|A) = dom xi /\ A by RELAT_1:61;
A2: dom (C+^xi) = dom xi by ORDINAL3:def 1;
A3: dom ((C+^xi)|A) = dom (C+^xi) /\ A by RELAT_1:61;
A4: now
    let e be object;
    assume
A5: e in dom ((C+^xi)|A);
    then reconsider a = e as Ordinal;
A6: e in dom xi by A3,A2,A5,XBOOLE_0:def 4;
    thus ((C+^xi)|A).e = (C+^xi).a by A5,FUNCT_1:47
      .= C+^(xi.a) by A6,ORDINAL3:def 1
      .= C+^((xi|A).a) by A3,A1,A2,A5,FUNCT_1:47
      .= (C+^(xi|A)).e by A3,A1,A2,A5,ORDINAL3:def 1;
  end;
  dom (C+^(xi|A)) = dom (xi|A) by ORDINAL3:def 1;
  hence thesis by A1,A2,A4,FUNCT_1:2,RELAT_1:61;
end;

theorem Th16:
  for phi being Ordinal-Sequence st phi is increasing & phi is
  continuous holds C+^phi is continuous
proof
  let phi be Ordinal-Sequence such that
A1: phi is increasing;
  assume
A2: for A,B st A in dom phi & A <> 0 & A is limit_ordinal & B = phi.A
  holds B is_limes_of phi|A;
  let A,B;
  set xi = phi|A;
  reconsider A9 = phi.A as Ordinal;
  assume that
A3: A in dom (C+^phi) and
A4: A <> 0 and
A5: A is limit_ordinal and
A6: B = (C+^phi).A;
A7: dom phi = dom (C+^phi) by ORDINAL3:def 1;
  then
A8: B = C+^A9 by A3,A6,ORDINAL3:def 1;
  A9 is_limes_of xi by A2,A3,A4,A5,A7;
  then
A9: lim xi = A9 by ORDINAL2:def 10;
A10: dom xi = dom (C+^xi) & (C+^phi)|A = C+^xi by Th15,ORDINAL3:def 1;
A11: xi is increasing by A1,ORDINAL4:15;
  then
A12: C+^xi is increasing by Th14;
  A c= dom (C+^phi) by A3,ORDINAL1:def 2;
  then
A13: dom xi = A by A7,RELAT_1:62;
  then
A14: sup (C+^xi) = C+^sup xi by A4,ORDINAL3:43;
  sup xi = lim xi by A4,A5,A13,A11,ORDINAL4:8;
  hence thesis by A4,A5,A13,A10,A8,A14,A9,A12,ORDINAL4:8;
end;

reserve psi for Ordinal-Sequence;

theorem
  e in rng psi implies e is Ordinal by ORDINAL2:48;

theorem
  rng psi c= sup psi by ORDINAL2:49;

theorem
  A is_cofinal_with B & B is_cofinal_with C implies A is_cofinal_with C
  by ORDINAL4:37;

theorem Th20:
  A is_cofinal_with B implies B c= A
proof
  given psi such that
A1: dom psi = B and
A2: rng psi c= A and
A3: psi is increasing and
  A = sup psi;
  let C;
  assume C in B;
  then C c= psi.C & psi.C in rng psi by A1,A3,FUNCT_1:def 3,ORDINAL4:10;
  hence thesis by A2,ORDINAL1:12;
end;

theorem
  A is_cofinal_with B & B is_cofinal_with A implies A = B
by Th20;

theorem
  dom psi <> {} & dom psi is limit_ordinal & psi is increasing & A
  is_limes_of psi implies A is_cofinal_with dom psi
proof
  assume that
A1: dom psi <> {} & dom psi is limit_ordinal and
A2: psi is increasing and
A3: A is_limes_of psi;
  take psi;
  thus dom psi = dom psi;
  sup psi = lim psi & A = lim psi by A1,A2,A3,ORDINAL2:def 10,ORDINAL4:8;
  hence thesis by A2,ORDINAL2:49;
end;

theorem
  succ A is_cofinal_with 1 by ORDINAL3:73;

theorem
  A is_cofinal_with succ B implies ex C st A = succ C
proof
  given psi such that
A1: dom psi = succ B and
A2: rng psi c= A and
A3: psi is increasing and
A4: A = sup psi;
  reconsider C = psi.B as Ordinal;
  take C;
  thus A c= succ C
  proof
    let a be Ordinal;
    assume a in A;
    then consider b being Ordinal such that
A5: b in rng psi and
A6: a c= b by A4,ORDINAL2:21;
    consider e being object such that
A7: e in succ B and
A8: b = psi.e by A1,A5,FUNCT_1:def 3;
    reconsider e as Ordinal by A7;
    e c= B by A7,ORDINAL1:22;
    then b c= C by A1,A3,A8,ORDINAL1:6,ORDINAL4:9;
    then b in succ C by ORDINAL1:22;
    hence thesis by A6,ORDINAL1:12;
  end;
  B in succ B by ORDINAL1:6;
  then C in rng psi by A1,FUNCT_1:def 3;
  hence thesis by A2,ORDINAL1:21;
end;

theorem
  A is_cofinal_with B implies (A is limit_ordinal iff B is limit_ordinal
  ) by ORDINAL4:38;

theorem
  A is_cofinal_with {} implies A = {} by ORDINAL2:50;

theorem
  not On W is_cofinal_with a
proof
  given psi such that
A1: dom psi = a and
A2: rng psi c= On W and
  psi is increasing and
A3: On W = sup psi;
  On W c= W by ORDINAL2:7;
  then rng psi c= W by A2;
  then sup rng psi in W by A1,Th11,ZF_REFLE:19;
  then sup psi in On W by ORDINAL1:def 9;
  hence contradiction by A3;
end;

theorem Th28:
  omega in W & phi is increasing & phi is continuous implies ex b
  st a in b & phi.b = b
proof
  assume that
A1: omega in W and
A2: phi is increasing and
A3: phi is continuous;
  deffunc F(Ordinal of W) = (succ a)+^phi.$1;
  consider xi such that
A4: xi.b = F(b) from ORDINAL4:sch 2;
A5: dom xi = On W by FUNCT_2:def 1;
A6: dom phi = On W by FUNCT_2:def 1;
  for A st A in dom phi holds xi.A = (succ a)+^(phi.A)
  proof
    let A;
    assume A in dom phi;
    then reconsider b = A as Ordinal of W by A6,ZF_REFLE:7;
    xi.b = (succ a)+^phi.b by A4;
    hence thesis;
  end;
  then xi = (succ a)+^phi by A6,A5,ORDINAL3:def 1;
  then xi is increasing & xi is continuous by A2,A3,Th14,Th16;
  then consider A such that
A7: A in dom xi and
A8: xi.A = A by A1,ORDINAL4:36;
  reconsider b = A as Ordinal of W by A5,A7,ZF_REFLE:7;
A9: b = (succ a)+^phi.b by A4,A8;
  take b;
A10: succ a c= (succ a)+^phi.b & a in succ a by ORDINAL1:6,ORDINAL3:24;
A11: phi.b c= (succ a)+^phi.b by ORDINAL3:24;
  b c= phi.b by A2,A6,A5,A7,ORDINAL4:10;
  hence thesis by A10,A9,A11;
end;

theorem Th29:
  omega in W & phi is increasing & phi is continuous implies ex a
  st b in a & phi.a = a & a is_cofinal_with omega
proof
  assume that
A1: omega in W and
A2: phi is increasing and
A3: phi is continuous;
A4: omega in On W by A1,ORDINAL1:def 9;
  deffunc D(Ordinal,set) = 0-element_of W;
  deffunc C(Ordinal,Ordinal of W) = succ(phi.$2);
  consider nu be Ordinal-Sequence of W such that
A5: nu.0-element_of W = b and
A6: for a holds nu.succ a = C(a,nu.a) and
  for a st a <> 0-element_of W & a is limit_ordinal holds nu.a = D(a,nu|a)
  from ZF_REFLE:sch 3;
  set xi = nu|omega;
  set a = sup xi;
A7: On W c= W by ORDINAL2:7;
  dom nu = On W by FUNCT_2:def 1;
  then
A8: omega c= dom nu by A4;
  then
A9: dom xi = omega by RELAT_1:62;
  rng xi c= rng nu & rng nu c= On W by RELAT_1:def 19;
  then rng xi c= On W;
  then rng xi c= W by A7;
  then reconsider a as Ordinal of W by A1,A9,Th11,ZF_REFLE:19;
A10: a in dom phi by ORDINAL4:34;
  then
A11: a c= dom phi by ORDINAL1:def 2;
  then
A12: dom (phi|a) = a by RELAT_1:62;
A13: xi is increasing
  proof
    let A,B;
    assume that
A14: A in B and
A15: B in dom xi;
    defpred P[Ordinal] means A+^$1 in dom xi & $1 <> {} implies xi.A in xi.(A
    +^$1);
A16: for B st B <> 0 & B is limit_ordinal & for C st C in B holds P[C]
    holds P[B]
    proof
      let B;
      assume that
A17:  B <> 0 and
A18:  B is limit_ordinal;
      {} in B by A17,ORDINAL3:8;
      then
A19:  omega c= B by A18,ORDINAL1:def 11;
      B c= A+^B by ORDINAL3:24;
      hence thesis by A9,A19,ORDINAL1:5;
    end;
A20: for C st P[C] holds P[succ C]
    proof
      let C such that
A21:  A+^C in dom xi & C <> {} implies xi.A in xi.(A+^C) and
A22:  A+^succ C in dom xi and
      succ C <> {};
A23:  A+^succ C in On W by A4,A9,A22,ORDINAL1:10;
      then reconsider asc = A+^succ C as Ordinal of W by ZF_REFLE:7;
A24:  A+^C in asc by ORDINAL1:6,ORDINAL2:32;
      then A+^C in On W by A23,ORDINAL1:10;
      then reconsider ac = A+^C as Ordinal of W by ZF_REFLE:7;
A25:  now
        nu.ac in dom phi by ORDINAL4:34;
        then
A26:    nu.ac c= phi.(nu.ac) by A2,ORDINAL4:10;
        asc = succ ac by ORDINAL2:28;
        then
A27:    nu.asc = succ (phi.(nu.ac)) by A6;
        assume C = {};
        then
A28:    ac = A by ORDINAL2:27;
        xi.ac = nu.ac & xi.asc = nu.asc by A22,A24,FUNCT_1:47,ORDINAL1:10;
        hence thesis by A28,A27,A26,ORDINAL1:6,12;
      end;
A29:  succ ac = asc & nu.ac in dom phi by ORDINAL2:28,ORDINAL4:34;
      A+^C in dom xi by A22,A24,ORDINAL1:10;
      then
      xi.A in xi.ac & nu.asc = succ (phi.(nu.ac)) & nu.ac = xi.ac & phi.(
nu.ac) in succ(phi.(nu.ac)) & nu.ac c= phi.(nu.ac) or C = {} by A2,A6,A21,A29,
FUNCT_1:47,ORDINAL1:6,ORDINAL4:10;
      then
      xi.A in nu.ac & nu.ac in nu.asc & nu.asc = xi.asc or C = {} by A22,
FUNCT_1:47,ORDINAL1:12;
      then xi.A in nu.ac & nu.ac c= xi.asc or C = {} by ORDINAL1:def 2;
      hence thesis by A25;
    end;
A30: P[0];
A31: P[C] from ORDINAL2:sch 1(A30,A20,A16);
    ex C st B = A+^C & C <> {} by A14,ORDINAL3:28;
    hence thesis by A15,A31;
  end;
  then
A32: a is limit_ordinal by A9,Lm2,ORDINAL4:16;
  take a;
  0-element_of W in dom nu by ORDINAL4:34;
  then
A33: b in rng xi by A5,Lm1,FUNCT_1:50;
  hence b in a by ORDINAL2:19;
A34: a <> {} by A33,ORDINAL2:19;
  a in dom phi by ORDINAL4:34;
  then
A35: phi.a is_limes_of phi|a by A3,A32,A34;
  phi|a is increasing by A2,ORDINAL4:15;
  then sup (phi|a) = lim (phi|a) by A32,A34,A12,ORDINAL4:8;
  then
A36: phi.a = sup rng (phi|a) by A35,ORDINAL2:def 10;
  thus phi.a c= a
  proof
    let A;
    assume A in phi.a;
    then consider B such that
A37: B in rng (phi|a) and
A38: A c= B by A36,ORDINAL2:21;
    consider e being object such that
A39: e in a and
A40: B = (phi|a).e by A12,A37,FUNCT_1:def 3;
    reconsider e as Ordinal by A39;
    consider C such that
A41: C in rng xi and
A42: e c= C by A39,ORDINAL2:21;
A43: e c< C iff e c= C & e <> C;
    consider u being object such that
A44: u in omega and
A45: C = xi.u by A9,A41,FUNCT_1:def 3;
    reconsider u as Ordinal by A44;
    u c= omega by A44,ORDINAL1:def 2;
    then reconsider u as Ordinal of W by A1,CLASSES1:def 1;
A46: succ u in dom nu by ORDINAL4:34;
    C in a by A41,ORDINAL2:19;
    then e = C or e in C & C in dom phi by A11,A42,A43,ORDINAL1:11;
    then
A47: phi.e = phi.C or phi.e in phi.C by A2;
A48: nu.succ u = succ (phi.(nu.u)) by A6;
    succ u in omega by A44,Lm2,ORDINAL1:28;
    then nu.succ u in rng xi by A46,FUNCT_1:50;
    then
A49: nu.succ u in a by ORDINAL2:19;
    C = nu.u by A9,A44,A45,FUNCT_1:47;
    then
A50: phi.e c= phi.(nu.u) by A47,ORDINAL1:def 2;
    phi.e = B by A12,A39,A40,FUNCT_1:47;
    then B in nu.succ u by A48,A50,ORDINAL1:6,12;
    then B in a by A49,ORDINAL1:10;
    hence thesis by A38,ORDINAL1:12;
  end;
  thus a c= phi.a by A2,A10,ORDINAL4:10;
  take xi;
  rng xi c= a
  proof
    let e be object;
    assume
A51: e in rng xi;
    then consider u being object such that
 u in dom xi and
A52: e = xi.u by FUNCT_1:def 3;
    thus thesis by A51,A52,ORDINAL2:19;
  end;
  hence thesis by A8,A13,RELAT_1:62;
end;

theorem Th30:
  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
proof
  assume that
A1: omega in W and
A2: ( 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);
  set M = Union L;
  defpred P[object,object] means
ex H,phi st $1 = H & $2 = phi & phi is increasing &
phi is continuous & for a st phi.a = a & {} <> a for va holds Union L,(Union L)
  !va |= H iff L.a,va |= H;
A3: for e being object st e in WFF
ex u being object st u in Funcs(On W, On W) & P[e, u]
  proof
    let e be object;
    assume e in WFF;
    then reconsider H = e as ZF-formula by ZF_LANG:4;
    consider phi such that
A4: phi is increasing & phi is continuous & for a st phi.a = a & {} <>
a for va holds Union L,(Union L)!va |= H iff L.a,va |= H by A1,A2,ZF_REFLE:20;
    reconsider u = phi as set;
    take u;
    dom phi = On W & rng phi c= On W by FUNCT_2:def 1,RELAT_1:def 19;
    hence u in Funcs(On W, On W) by FUNCT_2:def 2;
    take H,phi;
    thus thesis by A4;
  end;
  consider Phi being Function such that
A5: dom Phi = WFF & rng Phi c= Funcs(On W, On W) and
A6: for e being object st e in WFF holds P[e, Phi.e]
from FUNCT_1:sch 6(A3);
  reconsider Phi as Function of WFF, Funcs(On W, On W) by A5,FUNCT_2:def 1
,RELSET_1:4;
  [:omega,omega:] in W by A1,CLASSES2:61;
  then bool [:omega,omega:] in W by CLASSES2:59;
  then card WFF c= card bool [:omega,omega:] & card bool [:omega,omega:] in
  card W by CARD_1:11,CLASSES2:1,ZF_LANG1:134;
  then consider phi such that
A7: phi is increasing & phi is continuous and
  phi.0-element_of W = 0-element_of W and
A8: for a holds phi.(succ a) = sup ({phi.a} \/ (uncurry Phi).:[:WFF,{
  succ a}:]) and
A9: for a st a <> 0-element_of W & a is limit_ordinal holds phi.a = sup
  (phi|a) by Th13,ORDINAL1:12;
  take phi;
  thus phi is increasing & phi is continuous by A7;
  let a such that
A10: phi.a = a and
A11: {} <> a;
  thus L.a c= Union L by ZF_REFLE:16;
  let H,va;
A12: H in WFF by ZF_LANG:4;
  then consider H1 being ZF-formula, xi such that
A13: H = H1 and
A14: Phi.H = xi and
A15: xi is increasing and
A16: xi is continuous and
A17: for a st xi.a = a & {} <> a for va holds M,M!va |= H1 iff L.a,va |=
  H1 by A6;
  defpred P[Ordinal] means $1 <> {} implies xi.$1 c= phi.$1;
  a in dom xi by ORDINAL4:34;
  then
A18: a c= xi.a by A15,ORDINAL4:10;
A19: for a st a <> 0-element_of W & a is limit_ordinal & for b st b in a
  holds P[b] holds P[a]
  proof
    let a such that
A20: a <> 0-element_of W and
A21: a is limit_ordinal and
A22: for b st b in a holds b <> {} implies xi.b c= phi.b and
    a <> {};
A23: a in dom xi by ORDINAL4:34;
    then xi.a is_limes_of xi|a by A16,A20,A21;
    then
A24: xi.a = lim (xi|a) by ORDINAL2:def 10;
    let A such that
A25: A in xi.a;
    a c= dom xi by A23,ORDINAL1:def 2;
    then
A26: dom (xi|a) = a by RELAT_1:62;
    xi|a is increasing by A15,ORDINAL4:15;
    then xi.a = sup (xi|a) by A20,A21,A26,A24,ORDINAL4:8
      .= sup rng (xi|a);
    then consider B such that
A27: B in rng (xi|a) and
A28: A c= B by A25,ORDINAL2:21;
    consider e being object such that
A29: e in dom (xi|a) and
A30: B = (xi|a).e by A27,FUNCT_1:def 3;
    reconsider e as Ordinal by A29;
    a in On W by ZF_REFLE:7;
    then e in On W by A26,A29,ORDINAL1:10;
    then reconsider e as Ordinal of W by ZF_REFLE:7;
A31: succ e in a by A21,A26,A29,ORDINAL1:28;
    e in succ e & succ e in dom xi by ORDINAL1:6,ORDINAL4:34;
    then
A32: xi.e in xi.succ e by A15;
    B = xi.e by A29,A30,FUNCT_1:47;
    then
A33: A in xi.succ e by A28,A32,ORDINAL1:12;
    succ e in dom phi by ORDINAL4:34;
    then
A34: phi.succ e in rng (phi| a) by A31,FUNCT_1:50;
    phi.a = sup (phi|a) by A9,A20,A21
      .= sup rng (phi|a);
    then
A35: phi.succ e in phi.a by A34,ORDINAL2:19;
    xi.succ e c= phi.succ e by A22,A31;
    hence A in phi.a by A35,A33,ORDINAL1:10;
  end;
A36: for a st P[a] holds P[succ a]
  proof
    let a;
    succ a in {succ a} by TARSKI:def 1;
    then
A37: [H,succ a] in [:WFF,{succ a}:] by A12,ZFMISC_1:87;
    succ a in dom xi by ORDINAL4:34;
    then [H,succ a] in dom uncurry Phi & (uncurry Phi).(H,succ a) = xi.succ a
    by A5,A12,A14,FUNCT_5:38;
    then xi.succ a in (uncurry Phi).:[:WFF,{succ a}:] by A37,FUNCT_1:def 6;
    then xi.succ a in {phi.a} \/ (uncurry Phi).:[:WFF,{succ a}:] by
XBOOLE_0:def 3;
    then
A38: xi.succ a in sup ({phi.a} \/ (uncurry Phi).:[:WFF,{succ a}:]) by
ORDINAL2:19;
    phi.(succ a) = sup ({phi.a} \/ (uncurry Phi).:[:WFF,{succ a}:]) by A8;
    hence thesis by A38,ORDINAL1:def 2;
  end;
A39: P[0-element_of W];
  for a holds P[a] from ZF_REFLE:sch 4(A39,A36,A19);
  then xi.a c= a by A10,A11;
  then xi.a = a by A18;
  hence thesis by A11,A13,A17;
end;

theorem Th31:
  Rank a in W
proof
  W = Rank On W & a in On W by CLASSES2:50,ZF_REFLE:7;
  hence thesis by CLASSES1:36;
end;

theorem Th32:
  a <> {} implies Rank a is non empty Element of W
by Th31,CLASSES1:36,ORDINAL3:8;

theorem Th33:
  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
proof
  deffunc D(Ordinal, set) = Rank $1;
  deffunc C(Ordinal,set) = Rank succ $1;
  consider L being Sequence such that
A1: dom L = On W & (0 in On W implies L.0 = Rank 1-element_of W) and
A2: for A st succ A in On W holds L.(succ A) = C(A,L.A) and
A3: for A st A in On W & A <> 0 & A is limit_ordinal holds L.A = D(A,L|
  A) from ORDINAL2:sch 5;
A4: a <> {} & a is limit_ordinal implies L.a = Rank a
  by A3,ZF_REFLE:7;
A5: L.succ a = Rank succ a
  by A2,ZF_REFLE:7;
A6: a <> {} implies L.a = Rank a
  proof
A7: now
A8:   a in On W by ZF_REFLE:7;
      given A such that
A9:   a = succ A;
      A in a by A9,ORDINAL1:6;
      then A in On W by A8,ORDINAL1:10;
      then reconsider A as Ordinal of W by ZF_REFLE:7;
      L.succ A = Rank succ A by A5;
      hence thesis by A9;
    end;
    a is limit_ordinal or ex A st a = succ A by ORDINAL1:29;
    hence thesis by A4,A7;
  end;
  rng L c= W
  proof
    let e be object;
    assume e in rng L;
    then consider u being object such that
A10: u in On W and
A11: e = L.u by A1,FUNCT_1:def 3;
    reconsider u as Ordinal of W by A10,ZF_REFLE:7;
    Rank 1-element_of W in W & Rank u in W by Th31;
    hence thesis by A1,A6,A10,A11;
  end;
  then reconsider L as Sequence of W by RELAT_1:def 19;
  now
    assume {} in rng L;
    then consider e being object such that
A12: e in On W and
A13: {} = L.e by A1,FUNCT_1:def 3;
    reconsider e as Ordinal of W by A12,ZF_REFLE:7;
    e = {} & 1-element_of W = {{}} or e <> {} by ORDINAL3:15;
    then L.e = Rank 1-element_of W & 1-element_of W <> {} or e <> {} & L.e =
    Rank e by A1,A6,ZF_REFLE:7;
    hence contradiction by A13,Th32;
  end;
  then reconsider L as DOMAIN-Sequence of W by A1,RELAT_1:def 9,ZF_REFLE:def 2;
A14: Union L = W
  proof
    thus Union L c= W;
    let e be object;
A15: Union L = union rng L by CARD_3:def 4;
    assume e in W;
    then
A16: e in Rank On W by CLASSES2:50;
    On W is limit_ordinal by CLASSES2:51;
    then consider A such that
A17: A in On W and
A18: e in Rank A by A16,CLASSES1:31;
    reconsider A as Ordinal of W by A17,ZF_REFLE:7;
    L.A = Rank A & L.A in rng L by A1,A6,A17,A18,CLASSES1:29,FUNCT_1:def 3;
    then Rank A c= Union L by A15,ZFMISC_1:74;
    hence thesis by A18;
  end;
A19: 0-element_of W in On W by ZF_REFLE:7;
A20: for a,b st a in b holds L.a c= L.b
  proof
    let a,b;
    assume
A21: a in b;
    then
A22: Rank a in Rank b & succ a c= b by CLASSES1:36,ORDINAL1:21;
A23: L.b = Rank b by A6,A21;
    L.a = Rank a or a = 0-element_of W & L.a = Rank 1-element_of W &
    1-element_of W = succ 0-element_of W by A1,A19,A6;
    hence thesis by A22,A23,CLASSES1:37,ORDINAL1:def 2;
  end;
A24: for a st a <> {} & a is limit_ordinal holds L.a = Union (L|a)
  proof
    let a;
    assume that
A25: a <> {} and
A26: a is limit_ordinal;
A27: a in On W by ZF_REFLE:7;
A28: L.a = Rank a by A4,A25,A26;
    thus L.a c= Union (L|a)
    proof
      let e be object;
      assume e in L.a;
      then consider B such that
A29:  B in a and
A30:  e in Rank B by A26,A28,CLASSES1:31;
      B in On W by A27,A29,ORDINAL1:10;
      then reconsider B as Ordinal of W by ZF_REFLE:7;
A31:  succ B in On W & Union (L|a) = union rng (L|a) by CARD_3:def 4,ZF_REFLE:7
;
      L.succ B = Rank succ B by A5;
      then
A32:  Rank B c= L.succ B by CLASSES1:33;
      succ B in a by A26,A29,ORDINAL1:28;
      then L.succ B c= Union (L|a) by A1,A31,FUNCT_1:50,ZFMISC_1:74;
      then Rank B c= Union (L|a) by A32;
      hence thesis by A30;
    end;
    let e be object;
    assume e in Union (L|a);
    then e in union rng (L|a) by CARD_3:def 4;
    then consider X such that
A33: e in X and
A34: X in rng (L|a) by TARSKI:def 4;
    consider u being object such that
A35: u in dom (L|a) and
A36: X = (L|a).u by A34,FUNCT_1:def 3;
    reconsider u as Ordinal by A35;
A37: X = L.u by A35,A36,FUNCT_1:47;
A38: dom (L|a) c= a by RELAT_1:58;
    then u in On W by A27,A35,ORDINAL1:10;
    then reconsider u as Ordinal of W by ZF_REFLE:7;
    L.u c= L.a by A20,A35,A38;
    hence thesis by A33,A37;
  end;
  assume omega in W;
  then consider phi such that
A39: phi is increasing & phi is continuous and
A40: for a st phi.a = a & {} <> a holds L.a is_elementary_subsystem_of
  Union L by A20,A24,Th30;
  take phi;
  thus phi is increasing & phi is continuous by A39;
  let a,M;
  assume that
A41: phi.a = a and
A42: {} <> a and
A43: M = Rank a;
  M = L.a by A6,A42,A43;
  hence thesis by A40,A14,A41,A42;
end;

theorem Th34:
  omega in W implies ex b,M st a in b & M = Rank b & M
  is_elementary_subsystem_of W
proof
  assume
A1: omega in W;
  then consider phi such that
A2: phi is increasing & phi is continuous and
A3: for a,M st phi.a = a & {} <> a & M = Rank a holds M
  is_elementary_subsystem_of W by Th33;
  consider b such that
A4: a in b and
A5: phi.b = b by A1,A2,Th28;
  reconsider M = Rank b as non empty set by A4,CLASSES1:36;
  take b,M;
  thus thesis by A3,A4,A5;
end;

theorem Th35:
  omega in W implies ex a,M st a is_cofinal_with omega & M = Rank
  a & M is_elementary_subsystem_of W
proof
  set a = the Ordinal of W;
  assume
A1: omega in W;
  then consider phi such that
A2: phi is increasing & phi is continuous and
A3: for a,M st phi.a = a & {} <> a & M = Rank a holds M
  is_elementary_subsystem_of W by Th33;
  consider b such that
A4: a in b and
A5: phi.b = b & b is_cofinal_with omega by A1,A2,Th29;
  reconsider M = Rank b as non empty set by A4,CLASSES1:36;
  take b,M;
  thus thesis by A3,A4,A5;
end;

theorem
  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
proof
  assume ( 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);
  then consider phi such that
A1: phi is increasing & phi is continuous and
A2: for a st phi.a = a & {} <> a holds L.a is_elementary_subsystem_of
  Union L by Th30;
  take phi;
  thus phi is increasing & phi is continuous by A1;
  let a;
  assume phi.a = a & {} <> a;
  hence thesis by A2,Th9;
end;

theorem
  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
proof
  assume omega in W;
  then consider phi such that
A1: phi is increasing & phi is continuous and
A2: for a,M st phi.a = a & {} <> a & M = Rank a holds M
  is_elementary_subsystem_of W by Th33;
  take phi;
  thus phi is increasing & phi is continuous by A1;
  let a,M;
  assume phi.a = a & {} <> a & M = Rank a;
  hence thesis by A2,Th9;
end;

theorem Th38:
  omega in W implies ex b,M st a in b & M = Rank b & M <==> W
proof
  assume omega in W;
  then consider b,M such that
A1: a in b & M = Rank b & M is_elementary_subsystem_of W by Th34;
  take b,M;
  thus thesis by A1,Th9;
end;

theorem Th39:
  omega in W implies ex a,M st a is_cofinal_with omega & M = Rank a & M <==> W
proof
  assume omega in W;
  then consider b,M such that
A1: b is_cofinal_with omega & M = Rank b & M is_elementary_subsystem_of
  W by Th35;
  take b,M;
  thus thesis by A1,Th9;
end;

theorem
  omega in W implies ex a,M st a is_cofinal_with omega & M = Rank a & M
  is being_a_model_of_ZF
proof
  assume
A1: omega in W;
  then consider a,M such that
A2: a is_cofinal_with omega & M = Rank a & M <==> W by Th39;
  take a,M;
  W is being_a_model_of_ZF by A1,ZF_REFLE:6;
  hence thesis by A2,Th10;
end;

theorem
  omega in W & X in W implies ex M st X in M & M in W & M is
  being_a_model_of_ZF
proof
  assume
A1: omega in W;
A2: W = Rank On W by CLASSES2:50;
  assume X in W;
  then the_rank_of X in the_rank_of W by CLASSES1:68;
  then the_rank_of X in On W by A2,CLASSES1:64;
  then reconsider a = the_rank_of X as Ordinal of W by ZF_REFLE:7;
  consider b,M such that
A3: a in b and
A4: M = Rank b and
A5: M <==> W by A1,Th38;
  take M;
  X c= Rank a by CLASSES1:def 9;
  then
A6: X in Rank succ a by CLASSES1:32;
  succ a c= b by A3,ORDINAL1:21;
  then Rank succ a c= M by A4,CLASSES1:37;
  hence X in M by A6;
  b in On W by ZF_REFLE:7;
  hence M in W by A2,A4,CLASSES1:36;
  W is being_a_model_of_ZF by A1,ZF_REFLE:6;
  then W |= ZF-axioms by Th4;
  then M |= ZF-axioms by A5,Th8;
  hence thesis by A4,Th5;
end;