The Mizar article:

The Reflection Theorem

by
Grzegorz Bancerek

Received August 10, 1990

Copyright (c) 1990 Association of Mizar Users

MML identifier: ZF_REFLE
[ MML identifier index ]


environ

 vocabulary CLASSES2, ZF_LANG, FUNCT_1, ZF_MODEL, ORDINAL1, TARSKI, ORDINAL2,
      BOOLE, ZFMODEL1, RELAT_1, CARD_1, ORDINAL4, PROB_1, CLASSES1, ZFMISC_1,
      QC_LANG1, FUNCT_2, ARYTM_3, ZF_REFLE;
 notation TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, NUMBERS, XREAL_0, NAT_1,
      RELAT_1, FUNCT_1, FUNCT_2, FRAENKEL, ZF_MODEL, ZFMODEL1, ORDINAL1,
      ORDINAL2, CARD_1, PROB_1, CLASSES1, CLASSES2, ZF_LANG, ORDINAL4,
      ZF_LANG1;
 constructors ENUMSET1, NAT_1, FRAENKEL, ZF_MODEL, ZFMODEL1, WELLORD2, PROB_1,
      CLASSES1, ORDINAL4, ZF_LANG1, MEMBERED, XBOOLE_0;
 clusters SUBSET_1, FUNCT_1, ZF_LANG, ORDINAL1, ORDINAL2, CLASSES2, ZF_LANG1,
      RELSET_1, CARD_1, ZFMISC_1, XBOOLE_0;
 requirements NUMERALS, BOOLE, SUBSET;
 definitions TARSKI, FUNCT_1, ZF_LANG, ZF_MODEL, WELLORD2, ORDINAL2, RELAT_1,
      XBOOLE_0;
 theorems TARSKI, ZFMISC_1, NAT_1, FUNCT_1, FUNCT_2, ORDINAL1, ORDINAL2,
      ORDINAL3, ORDINAL4, CARD_1, CARD_2, CLASSES1, CLASSES2, ZF_LANG,
      ZF_MODEL, PROB_1, ZFMODEL1, FUNCT_5, ZF_LANG1, RELAT_1, RELSET_1,
      XBOOLE_0, XBOOLE_1, XCMPLX_1;
 schemes FUNCT_1, PARTFUN1, RECDEF_1, ORDINAL1, ORDINAL2, ZF_LANG, CARD_3;

begin

 reserve W for Universe,
         H for ZF-formula,
         x,y,z,X,Y for set,
         k for Variable,
         f for Function of VAR,W,
         u,v for Element of W;

canceled;

theorem
 Th2: W |= the_axiom_of_pairs
  proof
      W is epsilon-transitive & for u,v holds {u,v} in W;
   hence thesis by ZFMODEL1:2;
  end;

theorem
 Th3: W |= the_axiom_of_unions
  proof
      W is epsilon-transitive & for u holds union u in W;
   hence thesis by ZFMODEL1:4;
  end;

theorem
 Th4: omega in W implies W |= the_axiom_of_infinity
  proof assume omega in W;
   then reconsider u = omega as Element of W;
      now take u;
     thus u <> {};
     let v; assume
A1:   v in u;
     then reconsider A = v as Ordinal by ORDINAL1:23;
     succ A in omega by A1,ORDINAL1:41,ORDINAL2:19;
      then succ A c= u & u in W by ORDINAL1:def 2;
     then reconsider w = succ A as Element of W by CLASSES1:def 1;
     take w;
        A in succ A by ORDINAL1:10;
     then v c= w & v <> w & w in u by A1,ORDINAL1:41,def 2,ORDINAL2:19;
     hence v c< w & w in u by XBOOLE_0:def 8;
    end;
   hence thesis by ZFMODEL1:6;
  end;

theorem
 Th5: W |= the_axiom_of_power_sets
  proof
      now let u; bool u in W & W /\ bool u c= bool u by XBOOLE_1:17;
     hence W /\ bool u in W by CLASSES1:def 1;
    end;
   hence thesis by ZFMODEL1:8;
  end;

theorem
 Th6: for H st { x.0,x.1,x.2 } misses Free H holds
   W |= the_axiom_of_substitution_for H
  proof
      for H,f st { x.0,x.1,x.2 } misses Free H &
     W,f |= All(x.3,Ex(x.0,All(x.4,H <=> x.4 '=' x.0)))
      for u holds def_func'(H,f).:u in W
     proof let H,f such that { x.0,x.1,x.2 } misses Free H &
       W,f |= All(x.3,Ex(x.0,All(x.4,H <=> x.4 '=' x.0)));
      let u;
       Card u <` Card W & def_func'(H,f).:u c= W &
        Card (def_func'(H,f).:u) <=` Card u
         by CARD_2:3,CLASSES2:1;
       then Card (def_func'(H,f).:u) <` Card W by ORDINAL1:22;
      hence thesis by CLASSES1:2;
     end;
   hence thesis by ZFMODEL1:19;
  end;

theorem
   omega in W implies W is_a_model_of_ZF
  proof assume omega in W;
   hence
      W is epsilon-transitive &
    W |= the_axiom_of_pairs &
    W |= the_axiom_of_unions &
    W |= the_axiom_of_infinity &
    W |= the_axiom_of_power_sets &
    for H st { x.0,x.1,x.2 } misses Free H holds
     W |= the_axiom_of_substitution_for H
      by Th2,Th3,Th4,Th5,Th6;
  end;

 reserve
         F for Function,

         A,A1,A2,B,C for Ordinal,
         a,b,b1,b2,c for Ordinal of W,
         fi for Ordinal-Sequence,
         phi for Ordinal-Sequence of W,
         H for ZF-formula;

 definition let A,B;
  redefine pred A c= B means for C st C in A holds C in B;
   compatibility
    proof
     thus A c= B implies for C st C in A holds C in B;
     assume
A1:    for C st C in A holds C in B;
     let x; assume
A2:    x in A;
     then reconsider C = x as Ordinal by ORDINAL1:23;
        C in B by A1,A2;
     hence thesis;
    end;
 end;

scheme ALFA { D() -> non empty set, P[set,set] }:
 ex F st dom F = D() &
  for d being Element of D() ex A st A = F.d & P[d,A] &
   for B st P[d,B] holds A c= B
  provided
A1: for d being Element of D() ex A st P[d,A]
  proof
   defpred Q[set,set] means
    ex A st A = $2 & P[$1,A] & for B st P[$1,B] holds A c= B;
A2:  for x,y,z st x in D() & Q[x,y] & Q[x,z] holds y = z
     proof let x,y,z such that x in D();
      given A1 such that
A3:    A1 = y & P[x,A1] & for B st P[x,B] holds A1 c= B;
      given A2 such that
A4:    A2 = z & P[x,A2] & for B st P[x,B] holds A2 c= B;
         A1 c= A2 & A2 c= A1 by A3,A4;
      hence thesis by A3,A4,XBOOLE_0:def 10;
     end;
A5:  for x st x in D() ex y st Q[x,y]
     proof let x; assume x in D(); then
       reconsider d = x as Element of D();
       defpred Q[Ordinal] means P[d,$1];
A6:    ex A st Q[A] by A1;
      consider A such that
A7:    Q[A] & for B st Q[B] holds A c= B from Ordinal_Min(A6);
      reconsider y = A as set;
      take y,A; thus thesis by A7;
     end;
   consider F such that
A8:  dom F = D() & for x st x in D() holds Q[x,F.x] from FuncEx(A2,A5);
   take F; thus dom F = D() by A8;
   let d be Element of D();
   thus Q[d,F.d] by A8;
  end;

scheme ALFA'Universe { W()->Universe, D() -> non empty set, P[set,set] }:
 ex F st dom F = D() &
  for d being Element of D() ex a being Ordinal of W() st a = F.d & P[d,a] &
   for b being Ordinal of W() st P[d,b] holds a c= b
  provided
A1: for d being Element of D() ex a being Ordinal of W() st P[d,a]
  proof defpred p[set,set] means P[$1,$2];
A2:  for d being Element of D() ex A st p[d,A]
     proof let d be Element of D();
      consider a being Ordinal of W() such that
A3:    P[d,a] by A1;
      reconsider a as Ordinal;
      take a; thus thesis by A3;
     end;
   consider F such that
A4:  dom F = D() and
A5:  for d being Element of D() ex A st A = F.d & p[d,A] &
     for B st p[d,B] holds A c= B from ALFA(A2);
   take F; thus dom F = D() by A4;
   let d be Element of D();
   consider A such that
A6:  A = F.d & P[d,A] & for B st P[d,B] holds A c= B by A5;
   consider a being Ordinal of W() such that
A7:  P[d,a] by A1;
      A c= a & a in W() by A6,A7,ORDINAL4:def 2;
    then A in W() by CLASSES1:def 1;
   then reconsider a = A as Ordinal of W() by ORDINAL4:def 2;
   take a; thus thesis by A6;
  end;

theorem
 Th8: x is Ordinal of W iff x in On W
  proof
      (x is Ordinal of W iff x is Ordinal & x in W) &
    (x in On W iff x is Ordinal & x in W) by ORDINAL2:def 2,ORDINAL4:def 2;
   hence thesis;
  end;

 reserve psi for Ordinal-Sequence;

scheme OrdSeqOfUnivEx { W()->Universe, P[set,set] }:
 ex phi being Ordinal-Sequence of W() st
   for a being Ordinal of W() holds P[a,phi.a]
  provided
A1: for a,b1,b2 being Ordinal of W() st P[a,b1] & P[a,b2] holds b1 = b2 and
A2: for a being Ordinal of W() ex b being Ordinal of W() st P[a,b]
  proof defpred Q[set,set] means P[$1,$2] & $2 is Ordinal of W();
A3:  for x,y,z st x in On W() & Q[x,y] & Q[x,z] holds y = z
     proof let x,y,z; assume x in On W();
      then reconsider a = x as Ordinal of W() by Th8;
      assume
A4:    (P[x,y] & y is Ordinal of W()) & (P[x,z] & z is Ordinal of W());
      then reconsider b1 = y, b2 = z as Ordinal of W();
         P[a,b1] & P[a,b2] by A4;
      hence thesis by A1;
     end;
A5:  for x st x in On W() ex y st Q[x,y]
     proof let x; assume x in On W();
      then reconsider a = x as Ordinal of W() by Th8;
      consider b being Ordinal of W() such that
A6:    P[a,b] by A2;
      reconsider y = b as set;
      take y; thus thesis by A6;
     end;
   consider f being Function such that
A7:  dom f = On W() &
     for x st x in On W() holds Q[x,f.x] from FuncEx(A3,A5);
   reconsider phi = f as T-Sequence by A7,ORDINAL1:def 7;
A8:  rng phi c= On W()
     proof let x; assume x in rng phi;
       then ex y st y in dom phi & x = phi.y by FUNCT_1:def 5;
      then reconsider x as Ordinal of W() by A7;
         x in W() by ORDINAL4:def 2;
      hence thesis by ORDINAL2:def 2;
     end;
   then reconsider phi as Ordinal-Sequence by ORDINAL2:def 8;
   reconsider phi as Ordinal-Sequence of W() by A7,A8,ORDINAL4:def 3;
   take phi; let a be Ordinal of W();
      a in W() by ORDINAL4:def 2;
    then a in On W() by ORDINAL2:def 2;
   hence P[a,phi.a] by A7;
  end;

scheme UOS_Exist { W()->Universe, a()->Ordinal of W(),
                   C(Ordinal,Ordinal)->Ordinal of W(),
                   D(Ordinal,T-Sequence)->Ordinal of W() } :
  ex phi being Ordinal-Sequence of W() st
   phi.0-element_of W() = a() &
   (for a being Ordinal of W() holds phi.(succ a) = C(a,phi.a)) &
   (for a being Ordinal of W() st a <> 0-element_of W() & a is_limit_ordinal
     holds phi.a = D(a,phi|a))
 proof
   deffunc c(Ordinal,Ordinal) = C($1,$2);
   deffunc d(Ordinal,T-Sequence) = D($1,$2);
   consider phi being Ordinal-Sequence such that
A1: dom phi = On W() and
A2: {} in On W() implies phi.{} = a() and
A3: for A st succ A in On W() holds phi.(succ A) = c(A,phi.A) and
A4: for A st A in On W() & A <> {} & A is_limit_ordinal
          holds phi.A = d(A,phi|A) from OS_Exist;
     rng phi c= On W()
    proof let x; assume x in rng phi;
     then consider y such that
A5:   y in dom phi & x = phi.y by FUNCT_1:def 5;
     reconsider y as Ordinal of W() by A1,A5,Th8;
A6:   now given A such that
A7:     y = succ A;
       reconsider B = phi.A as Ordinal;
          x = C(A,B) by A1,A3,A5,A7;
       hence thesis by Th8;
      end;
        now assume not ex A st y = succ A;
then A8:     y is_limit_ordinal by ORDINAL1:42;
       assume y <> {};
        then x = D(y,phi|y) by A1,A4,A5,A8;
       hence thesis by Th8;
      end;
     hence thesis by A2,A5,A6,Th8;
    end;
  then reconsider phi as Ordinal-Sequence of W() by A1,ORDINAL4:def 3;
  take phi; 0-element_of W() in dom phi by ORDINAL4:36;
  hence phi.0-element_of W() = a() by A1,A2,ORDINAL4:35;
  thus for a being Ordinal of W() holds phi.(succ a) = C(a,phi.a)
    proof let a be Ordinal of W();
        succ a in dom phi by ORDINAL4:36;
     hence thesis by A1,A3;
    end;
  let a be Ordinal of W();
     a in dom phi & {} = 0-element_of W() by ORDINAL4:35,36;
  hence thesis by A1,A4;
 end;

scheme Universe_Ind { W()->Universe, P[Ordinal] }:
 for a being Ordinal of W() holds P[a]
  provided
A1:  P[0-element_of W()] and
A2:  for a being Ordinal of W() st P[a] holds P[succ a] and
A3:  for a being Ordinal of W() st a <> 0-element_of W() & a is_limit_ordinal &
     for b being Ordinal of W() st b in a holds P[b] holds P[a]
  proof defpred Q[Ordinal] means $1 is Ordinal of W() implies P[$1];
A4: Q[{}] by A1,ORDINAL4:35;
A5: for A st Q[A] holds Q[succ A]
     proof let A such that
A6:    A is Ordinal of W() implies P[A] and
A7:    succ A is Ordinal of W();
         A in succ A & succ A in On W() by A7,Th8,ORDINAL1:10;
       then A in On W() by ORDINAL1:19;
      then reconsider a = A as Ordinal of W() by Th8;
         P[succ a] by A2,A6;
      hence thesis;
     end;
A8: for A st A <> {} & A is_limit_ordinal & for B st B in A holds Q[B]
      holds Q[A]
     proof let A such that
A9:    A <> {} & A is_limit_ordinal and
A10:    for B st B in A holds B is Ordinal of W() implies P[B];
      assume A is Ordinal of W();
      then reconsider a = A as Ordinal of W();
         {} = 0-element_of W() & for b be Ordinal of W() st b in a holds P[b]
        by A10,ORDINAL4:35;
      hence P[A] by A3,A9;
     end;
      Q[A] from Ordinal_Ind(A4,A5,A8);
   hence thesis;
  end;

 definition let f be Function, W be Universe, a be Ordinal of W;
  func union(f,a) -> set equals:
Def2:    Union (W|(f|Rank a));
   correctness;
 end;

canceled;

theorem
 Th10: for L being T-Sequence,A holds L|Rank A is T-Sequence
  proof let L be T-Sequence, A;
A1:  dom(L|Rank A) = dom L /\ Rank A by RELAT_1:90;
      now let X; assume X in dom(L|Rank A);
then A2:    X in dom L & X in Rank A by A1,XBOOLE_0:def 3;
     hence X is Ordinal by ORDINAL1:23;
        X c= dom L & X c= Rank A by A2,ORDINAL1:def 2;
     hence X c= dom(L|Rank A) by A1,XBOOLE_1:19;
    end;
    then dom(L|Rank A) is Ordinal by ORDINAL1:31;
   hence thesis by ORDINAL1:46;
  end;

theorem
 Th11: for L being Ordinal-Sequence,A holds L|Rank A is Ordinal-Sequence
  proof let L be Ordinal-Sequence, A;
   reconsider K = L|Rank A as T-Sequence by Th10;
   consider B such that
A1:  rng L c= B by ORDINAL2:def 8;
      rng K c= rng L by FUNCT_1:76;
    then rng K c= B by A1,XBOOLE_1:1;
   hence thesis by ORDINAL2:def 8;
  end;

theorem
    Union psi is Ordinal
  proof consider A such that
A1:  rng psi c= A by ORDINAL2:def 8;
A2:  Union psi = union rng psi by PROB_1:def 3;
      for x st x in rng psi holds x is Ordinal by A1,ORDINAL1:23;
   hence thesis by A2,ORDINAL1:35;
  end;

theorem
 Th13: Union (X|psi) is Ordinal
  proof consider A such that
A1:  rng psi c= A by ORDINAL2:def 8;
A2:  Union (X|psi) = union rng (X|psi) & rng (X|psi) c= rng psi
     by FUNCT_1:89,PROB_1:def 3;
      now let x; assume x in rng (X|psi);
      then x in A by A1,A2,TARSKI:def 3;
     hence x is Ordinal by ORDINAL1:23;
    end;
   hence thesis by A2,ORDINAL1:35;
  end;

theorem
 Th14: On Rank A = A
  proof
   thus On Rank A c= A
     proof let x; assume A1: x in On Rank A;
then A2:     x is Ordinal & x in Rank A by ORDINAL2:def 2;
      reconsider B = x as Ordinal by A1,ORDINAL2:def 2;
         the_rank_of B in A by A2,CLASSES1:74;
      hence x in A by CLASSES1:81;
     end;
      A c= Rank A by CLASSES1:44;
    then On A c= On Rank A by ORDINAL2:11;
   hence thesis by ORDINAL2:10;
  end;

theorem
 Th15: psi|Rank A = psi|A
  proof
      A c= Rank A by CLASSES1:44;
then A1:  (psi|Rank A)|A = psi|A & dom (psi|Rank A) c= Rank A &
     dom (psi|Rank A) c= dom psi by FUNCT_1:76,82,RELAT_1:87;
    then On dom (psi|Rank A) c= On Rank A & On dom (psi|Rank A) = dom (psi|
Rank A)
     by ORDINAL2:11,ORDINAL3:8;
    then dom (psi|Rank A) c= A by Th14;
   hence psi|Rank A = psi|A by A1,RELAT_1:97;
  end;

 definition let phi be Ordinal-Sequence, W be Universe, a be Ordinal of W;
  redefine func union(phi,a) -> Ordinal of W;
   coherence
    proof
     reconsider K = phi|Rank a as Ordinal-Sequence by Th11;
     reconsider A = Union (W|K) as Ordinal by Th13;
A1:    a in On W & W is_Tarski-Class & rng (W|K) c= W & dom (W|K) c= dom K
        by Th8,FUNCT_1:89,RELAT_1:116;
      then dom K c= Rank a & Rank a in W by CLASSES2:26,RELAT_1:87;
      then dom K in W by CLASSES1:def 1;
      then dom (W|K) in W by A1,CLASSES1:def 1;
      then Card dom (W|K) <` Card W & Card ((W|K).:dom(W|K)) <=` Card dom(W|K)
&
       (W|K).:dom(W|K) = rng(W|K) by CARD_2:3,CLASSES2:1,RELAT_1:146;
      then Card rng (W|K) <` Card W by ORDINAL1:22;
      then rng (W|K) in W & union rng (W|K) = Union (W|K)
       by A1,CLASSES1:2,PROB_1:def 3;
      then A in W & A = union (phi,a) by Def2,CLASSES2:65;
     hence thesis by ORDINAL4:def 2;
    end;
 end;

canceled;

theorem
 Th17: for phi being Ordinal-Sequence of W holds
   union(phi,a) = Union (phi|a) & union(phi|a,a) = Union (phi|a)
  proof let phi be Ordinal-Sequence of W;
      rng phi c= On W & On W c= W by ORDINAL2:9,ORDINAL4:def 3;
    then rng (phi|Rank a) c= rng phi & rng (phi|a) c= rng phi &
     rng phi c= W by FUNCT_1:76,XBOOLE_1:1;
    then rng (phi|Rank a) c= W & rng (phi|a) c= W & a c= Rank a
     by CLASSES1:44,XBOOLE_1:1;
    then (phi|a)|Rank a = phi|a & W|(phi|Rank a) = phi|Rank a &
     phi|a = W|(phi|a) by FUNCT_1:82,RELAT_1:125;
    then union(phi,a) = Union (phi|Rank a) &
     union(phi|a,a) = Union (phi|a) by Def2;
   hence thesis by Th15;
  end;

 definition let W be Universe, a,b be Ordinal of W;
  redefine func a \/ b -> Ordinal of W;
    coherence
     proof
        a,b are_c=-comparable by ORDINAL1:25;
      then a c= b or b c= a by XBOOLE_0:def 9;
      hence thesis by XBOOLE_1:12;
     end;
 end;

 definition let W;
  cluster non empty Element of W;
   existence
    proof consider u;
        {u} is non empty Element of W;
     hence thesis;
    end;
 end;

 definition let W;
  mode Subclass of W is non empty Subset of W;
 end;

 definition let W;
   let IT be T-Sequence of W;
 canceled 2;

  attr IT is DOMAIN-yielding means:
Def5:   dom IT = On W;
 end;

 definition let W;
  cluster DOMAIN-yielding non-empty T-Sequence of W;
   existence
    proof consider D being non empty Element of W;
      deffunc F(set) = D;
     consider L being T-Sequence such that
A1:    dom L = On W &
       for A for L1 being T-Sequence st A in On W & L1 = L|A holds L.A = F(L1)
        from TS_Exist;
        rng L c= W
       proof let x; assume x in rng L;
        then consider y such that
A2:       y in dom L & x = L.y by FUNCT_1:def 5;
        reconsider y as Ordinal by A2,ORDINAL1:23;
           L|y = L|y;
         then x = D by A1,A2;
        hence thesis;
       end;
     then reconsider L as T-Sequence of W by ORDINAL1:def 8;
     take L; thus dom L = On W by A1;
     assume {} in rng L;
     then consider x such that
A3:    x in dom L & {} = L.x by FUNCT_1:def 5;
     reconsider x as Ordinal by A3,ORDINAL1:23;
        L|x = L|x;
     hence contradiction by A1,A3;
    end;
 end;

definition let W;
  mode DOMAIN-Sequence of W is non-empty DOMAIN-yielding T-Sequence of W;
end;

 Lm1: X <> {} & X c= Y implies Y <> {}
  proof assume A1: X <> {};
   consider x being Element of X;
A2: x in X by A1;
   assume y in X implies y in Y;
   hence thesis by A2;
  end;

 definition let W; let L be DOMAIN-Sequence of W;
 redefine func Union L -> Subclass of W;
   coherence
    proof rng L c= W & Union L = union rng L by ORDINAL1:def 8,PROB_1:def 3;
     then A1:    Union L c= union W by ZFMISC_1:95;
     consider a; a in W by ORDINAL4:def 2;
     then a in On W by ORDINAL2:def 2;
      then a in dom L by Def5;
      then L.a in rng L & L.a = L.a by FUNCT_1:def 5;
      then L.a c= union rng L & L.a <> {} by RELAT_1:def 9,ZFMISC_1:92;
      then union rng L <> {} & union rng L = Union L by Lm1,PROB_1:def 3;
     then reconsider S = Union L as non empty set;

        S c= W
       proof let x; assume x in S;
        then consider X such that
A2:       x in X & X in W by A1,TARSKI:def 4;
           X c= W by A2,ORDINAL1:def 2;
        hence thesis by A2;
       end;
     hence thesis;
    end;
  let a;
  func L.a -> non empty Element of W;
   coherence
    proof a in W by ORDINAL4:def 2; then a in On W by ORDINAL2:def 2;
      then a in dom L by Def5;
      then L.a in rng L & rng L c= W by FUNCT_1:def 5,ORDINAL1:def 8;
     hence thesis by RELAT_1:def 9;
    end;
 end;

 reserve L for DOMAIN-Sequence of W,
         n,j for Nat,
         f for Function of VAR,L.a;

canceled 5;

theorem
 Th23: a in dom L
  proof a in W by ORDINAL4:def 2; then a in On W by ORDINAL2:def 2;
   hence thesis by Def5;
  end;

theorem
 Th24: L.a c= Union L
  proof a in dom L by Th23;
    then L.a in rng L & union rng L = Union L by FUNCT_1:def 5,PROB_1:def 3;
   hence thesis by ZFMISC_1:92;
  end;

theorem
 Th25: NAT,VAR are_equipotent
  proof deffunc F(Nat,set) = 5+($1+1);
    consider f being Function of NAT,NAT such that
A1:  f.0 = 5+0 & for n holds f.(n+1) = F(n,f.n) from LambdaRecExD;
A2:  dom f = NAT by FUNCT_2:def 1;
A3:  now let n;
        now given j such that A4: n = j+1;
       thus f.n = 5+n by A1,A4;
      end;
      then n = 0 or f.n = 5+n by NAT_1:22;
     hence f.n = 5+n by A1;
    end;
   thus NAT,VAR are_equipotent
     proof reconsider g = f as Function; take g;
      thus g is one-to-one
        proof let x,y; assume x in dom g & y in dom g;
         then reconsider n1 = x, n2 = y as Nat by FUNCT_2:def 1;
            f.n1 = 5+n1 & f.n2 = 5+n2 by A3;
         hence thesis by XCMPLX_1:2;
        end;
      thus dom g = NAT by FUNCT_2:def 1;
      thus rng g c= VAR
        proof let x; assume x in rng g;
         then consider y such that
A5:        y in dom f & x = f.y by FUNCT_1:def 5;
         reconsider y as Nat by A5,FUNCT_2:def 1;
            x = 5+y & 5+y >= 5 by A3,A5,NAT_1:29;
         hence thesis by ZF_LANG:def 1;
        end;
      let x; assume x in VAR;
       then ex n st x = n & 5 <= n by ZF_LANG:def 1;
      then consider n such that
A6:     x = 5+n by NAT_1:28;
         f.n = x & n in NAT by A3,A6;
      hence thesis by A2,FUNCT_1:def 5;
     end;
  end;

canceled;

theorem
 Th27: sup X c= succ union On X
  proof reconsider A = union On X as Ordinal by ORDINAL3:7;
      On X c= succ A
     proof let x; assume
A1:     x in On X;
      then reconsider a = x as Ordinal by ORDINAL2:def 2;
         a c= A by A1,ZFMISC_1:92;
      hence x in succ A by ORDINAL1:34;
     end;
   hence thesis by ORDINAL2:def 7;
  end;

theorem
 Th28: X in W implies sup X in W
  proof assume
A1:  X in W;
   reconsider a = union On X as Ordinal by ORDINAL3:7;
      On X c= X by ORDINAL2:9;
    then On X in W by A1,CLASSES1:def 1;
    then a in W by CLASSES2:65;
   then reconsider a as Ordinal of W by ORDINAL4:def 2;
      sup X c= succ a & succ a in W by Th27,ORDINAL4:def 2;
   hence thesis by CLASSES1:def 1;
  end;

 reserve x1 for Variable;

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
     for H ex phi st phi is increasing & phi is continuous &
      for a st phi.a = a & {} <> a
       for f holds Union L,(Union L)!f |= H iff L.a,f |= H
  proof assume
A1: 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);
   set M = Union L;
A2: dom L = On W by Def5;
A3: union rng L = M by PROB_1:def 3;
   defpred RT[ZF-formula] means
    ex phi st phi is increasing & phi is continuous &
      for a st phi.a = a & {} <> a for f holds M,M!f |= $1 iff L.a,f |= $1;
A4: for H st H is atomic holds RT[H]
     proof let H such that
A5:     H is_equality or H is_membership;
A6:     dom id On W = On W & rng id On W = On W by RELAT_1:71;
      then reconsider phi = id On W as T-Sequence by ORDINAL1:def 7;
      reconsider phi as Ordinal-Sequence by A6,ORDINAL2:def 8;
      reconsider phi as Ordinal-Sequence of W by A6,ORDINAL4:def 3;
      take phi;
      thus
A7:     phi is increasing
        proof let A,B; assume
A8:       A in B & B in dom phi;
          then A in dom phi by ORDINAL1:19;
          then phi.A = A & phi.B = B by A6,A8,FUNCT_1:35;
         hence thesis by A8;
        end;
      thus phi is continuous
        proof let A,B; assume
A9:       A in dom phi & A <> {} & A is_limit_ordinal & B = phi.A;
then A10:       phi.A = A & A c= dom phi by A6,FUNCT_1:35,ORDINAL1:def 2;
            phi|A = phi*(id A) by RELAT_1:94
             .= id((dom phi) /\ A) by A6,FUNCT_1:43
             .= id A by A10,XBOOLE_1:28;
          then rng(phi|A) = A by RELAT_1:71;
then A11:       sup(phi|A) = sup A by ORDINAL2:35 .= B by A9,A10,ORDINAL2:26;
            dom (phi|A) = A & phi|A is increasing
           by A7,A10,ORDINAL4:15,RELAT_1:91;
         hence thesis by A9,A11,ORDINAL4:8;
        end;
      let a such that phi.a = a & {} <> a;
A12:    L.a c= M by Th24;
      let f;
      thus M,M!f |= H implies L.a,f |= H
        proof assume
A13:       M,M!f |= H;
A14:       M!f = f by A12,ZF_LANG1:def 2;
A15:       now assume H is_equality;
then A16:         H = (Var1 H) '=' (Var2 H) by ZF_LANG:53;
            then (M!f).Var1 H = (M!f).Var2 H by A13,ZF_MODEL:12;
           hence thesis by A14,A16,ZF_MODEL:12;
          end;
            now assume H is_membership;
then A17:         H = (Var1 H) 'in' (Var2 H) by ZF_LANG:54;
            then (M!f).Var1 H in (M!f).Var2 H by A13,ZF_MODEL:13;
           hence thesis by A14,A17,ZF_MODEL:13;
          end;
         hence thesis by A5,A15;
        end;
      assume
A18:     L.a,f |= H;
A19:     M!f = f by A12,ZF_LANG1:def 2;
A20:     now assume H is_equality;
then A21:      H = (Var1 H) '=' (Var2 H) by ZF_LANG:53;
         then f.Var1 H = f.Var2 H by A18,ZF_MODEL:12;
        hence thesis by A19,A21,ZF_MODEL:12;
       end;
         now assume H is_membership;
then A22:      H = (Var1 H) 'in' (Var2 H) by ZF_LANG:54;
         then f.Var1 H in f.Var2 H by A18,ZF_MODEL:13;
        hence thesis by A19,A22,ZF_MODEL:13;
       end;
      hence M,M!f |= H by A5,A20;
     end;
A23: for H st H is negative & RT[the_argument_of H] holds RT[H]
     proof let H; assume H is negative;
then A24:     H = 'not' the_argument_of H by ZF_LANG:def 30;
      given phi such that
A25:     phi is increasing & phi is continuous and
A26:     for a st phi.a = a & {} <> a
        for f holds M,M!f |= the_argument_of H iff L.a,f |= the_argument_of H;
      take phi;
      thus phi is increasing & phi is continuous by A25;
      let a such that
A27:     phi.a = a & {} <> a;
A28:    L.a c= M by Th24;
      let f;
      thus M,M!f |= H implies L.a,f |= H
        proof assume
            M,M!f |= H;
          then not M,M!f |= the_argument_of H & f = M!f
           by A24,A28,ZF_LANG1:def 2,ZF_MODEL:14;
          then not L.a,f |= the_argument_of H by A26,A27;
         hence thesis by A24,ZF_MODEL:14;
        end;
      assume L.a,f |= H;
       then not L.a,f |= the_argument_of H by A24,ZF_MODEL:14;
       then not M,M!f |= the_argument_of H by A26,A27;
      hence thesis by A24,ZF_MODEL:14;
     end;
A29: for H st H is conjunctive &
      RT[the_left_argument_of H] & RT[the_right_argument_of H] holds RT[H]
     proof let H; assume H is conjunctive;
then A30:     H = (the_left_argument_of H) '&' (the_right_argument_of H)
         by ZF_LANG:58;
      given fi1 being Ordinal-Sequence of W such that
A31:     fi1 is increasing & fi1 is continuous and
A32:     for a st fi1.a = a & {} <> a for f holds
        M,M!f |= the_left_argument_of H iff L.a,f |= the_left_argument_of H;
      given fi2 being Ordinal-Sequence of W such that
A33:     fi2 is increasing & fi2 is continuous and
A34:     for a st fi2.a = a & {} <> a for f holds
        M,M!f |= the_right_argument_of H iff L.a,f |= the_right_argument_of H;
      take phi = fi2*fi1;
         ex fi st fi = fi2*fi1 & fi is increasing by A31,A33,ORDINAL4:13;
      hence phi is increasing & phi is continuous
       by A31,A33,ORDINAL4:17;
      let a such that
A35:     phi.a = a & {} <> a;
A36:     a in dom fi1 & a in dom fi2 & a in dom phi by ORDINAL4:36;
then A37:     a c= fi1.a & a c= fi2.a by A31,A33,ORDINAL4:10;
A38:     now assume fi1.a <> a;
         then a c< fi1.a by A37,XBOOLE_0:def 8;
then A39:      a in fi1.a by ORDINAL1:21;
           fi1.a in dom fi2 by ORDINAL4:36;
then A40:      fi2.a in fi2.(fi1.a) by A33,A39,ORDINAL2:def 16;
           phi.a = fi2.(fi1.a) by A36,FUNCT_1:22;
        hence contradiction by A35,A37,A40,ORDINAL1:7;
       end;
then A41:       fi2.a = a by A35,A36,FUNCT_1:22;
A42:    L.a c= M by Th24;
      let f;
      thus M,M!f |= H implies L.a,f |= H
        proof assume
            M,M!f |= H;
          then M,M!f |= the_left_argument_of H & M,M!f |=
the_right_argument_of H &
           f = M!f by A30,A42,ZF_LANG1:def 2,ZF_MODEL:15;
          then L.a,f |= the_left_argument_of H & L.a,f |=
the_right_argument_of H
            by A32,A34,A35,A38,A41;
         hence thesis by A30,ZF_MODEL:15;
        end;
      assume L.a,f |= H;
     then L.a,f |= the_left_argument_of H & L.a,f |= the_right_argument_of H
         by A30,ZF_MODEL:15;
       then M,M!f |= the_left_argument_of H & M,M!f |= the_right_argument_of H
         by A32,A34,A35,A38,A41;
      hence thesis by A30,ZF_MODEL:15;
     end;
A43: for H st H is universal & RT[the_scope_of H] holds RT[H]
     proof let H; assume H is universal;
then A44:     H = All(bound_in H,the_scope_of H) by ZF_LANG:62;
      given phi such that
A45:     phi is increasing & phi is continuous and
A46:     for a st phi.a = a & {} <> a for f holds
        M,M!f |= the_scope_of H iff L.a,f |= the_scope_of H;
      set x0 = bound_in H;
      set H' = the_scope_of H;
A47:     now assume
A48:      not x0 in Free H';
        thus thesis
          proof take phi;
           thus phi is increasing & phi is continuous by A45;
           let a such that
A49:         phi.a = a & {} <> a;
           let f;
           thus M,M!f |= H implies L.a,f |= H
             proof assume
A50:            M,M!f |= H;
                 for k st (M!f).k <> (M!f).k holds x0 = k;
               then M,M!f |= H' by A44,A50,ZF_MODEL:16;
               then L.a,f |= H' by A46,A49;
              hence L.a,f |= H by A44,A48,ZFMODEL1:10;
             end;
           assume
A51:         L.a,f |= H;
              for k st f.k <> f.k holds x0 = k;
         then L.a,f |= H' by A44,A51,ZF_MODEL:16;
            then M,M!f |= H' by A46,A49;
           hence M,M!f |= H by A44,A48,ZFMODEL1:10;
          end;
       end;
      defpred P[set,set] means
       ex f being Function of VAR,M st $1 = f &
         ((ex m being Element of M st m in L.$2 & M,f/(x0,m) |= 'not' H') or
           $2 = 0-element_of W & not ex m being Element of M st
           M,f/(x0,m) |= 'not' H');
A52:     for h being Element of Funcs(VAR,M) qua non empty set
        ex a st P[h,a]
        proof let h be Element of Funcs(VAR,M) qua non empty set;
         reconsider f = h as Element of Funcs(VAR,M);
         reconsider f as Function of VAR,M;
            now per cases;
           suppose
            for m being Element of M holds not M,f/(x0,m) |= 'not' H';
            hence thesis;
           suppose
A53:          not for m being Element of M holds not M,f/(x0,m) |= 'not' H';
            thus thesis
              proof consider m being Element of M such that
A54:             M,f/(x0,m) |= 'not' H' by A53;
               consider X be set such that
A55:             m in X & X in rng L by A3,TARSKI:def 4;
               consider x such that
A56:             x in dom L & X = L.x by A55,FUNCT_1:def 5;
               reconsider x as Ordinal by A56,ORDINAL1:23;
                  x in W by A2,A56,ORDINAL2:def 2;
               then reconsider b = x as Ordinal of W by ORDINAL4:def 2;
               take b, f; thus thesis by A54,A55,A56;
              end;
          end;
         hence thesis;
        end;
      consider rho being Function such that
A57:    dom rho = Funcs(VAR,M) qua non empty set and
A58:    for h being Element of Funcs(VAR,M) qua non empty set
        ex a st a = rho.h & P[h,a] &
         for b st P[h,b] holds a c= b from ALFA'Universe(A52);
        defpred SI[Ordinal of W,Ordinal of W] means
          $2 = sup (rho.:Funcs(VAR,L.$1));
A59:    for a,b1,b2 st SI[a, b1] & SI[a, b2] holds b1 = b2;
A60:    for a ex b st SI[a, b]
        proof let a; set X = rho.:Funcs(VAR,L.a);
A61:        X c= W
           proof let x; assume x in X;
            then consider h being set such that
A62:          h in dom rho & h in Funcs(VAR,L.a) & x = rho.h by FUNCT_1:def 12;
               L.a c= M by Th24;
             then Funcs(VAR,L.a) c= Funcs(VAR,M) by FUNCT_5:63;
            then reconsider h as Element of Funcs(VAR,M) qua non empty set by
A62;
               ex a st a = rho.h &
             (ex f being Function of VAR,M st h = f & ((ex m being Element of
             M st m in L.a & M,f/(x0,m) |= 'not'
 H') or a = 0-element_of W & not ex m being
             Element of M st M,f/(x0,m) |= 'not' H')) & for b st ex f being
             Function of VAR,M st h = f & ((ex m being Element of M st m in L.b
             & M,f/(x0,m) |= 'not'
 H') or b = 0-element_of W & not ex m being Element of M
             st M,f/(x0,m) |= 'not' H') holds a c= b by A58;
            hence x in W by A62,ORDINAL4:def 2;
           end;
            L.a in W & Card VAR = Card omega & Card(L.a) = Card(L.a)
           by Th25,CARD_1:21;
          then Card Funcs(VAR,L.a) = Card Funcs(omega,L.a) & Funcs(omega,L.a)
in W
           by A1,CLASSES2:67,FUNCT_5:68;
          then Card X <=` Card Funcs(omega,L.a) & Card Funcs(omega,L.a) <`
Card W
           by CARD_2:3,CLASSES2:1;
          then Card X <` Card W & W is_Tarski-Class by ORDINAL1:22;
          then X in W by A61,CLASSES1:2;
          then sup X in W by Th28;
         then reconsider b = sup X as Ordinal of W by ORDINAL4:def 2;
         take b; thus thesis;
        end;
      consider si being Ordinal-Sequence of W such that
A63:     for a holds SI[a, si.a] from OrdSeqOfUnivEx(A59,A60);
      deffunc C(Ordinal of W, Ordinal of W) = succ((si.succ $1) \/ $2);
      deffunc D(Ordinal of W, Ordinal-Sequence) = union($2,$1);
      consider ksi being Ordinal-Sequence of W such that
A64:    ksi.0-element_of W = si.0-element_of W and
A65:    for a holds ksi.(succ a) = C(a,ksi.a) and
A66:    for a st a <> 0-element_of W & a is_limit_ordinal
               holds ksi.a = D(a,ksi|a) from UOS_Exist;
A67:    dom ksi = On W by ORDINAL4:def 3;
A68:    0-element_of W = {} by ORDINAL4:35;
A69:     ksi is increasing
        proof let A,B; assume
A70:       A in B & B in dom ksi;
          then A in dom ksi by ORDINAL1:19;
         then reconsider a = A, b = B as Ordinal of W by A67,A70,Th8;
         defpred Theta[Ordinal of W] means a in $1 implies ksi.a in ksi.$1;
A71:       Theta[0-element_of W] by ORDINAL4:35;
A72:       Theta[c] implies Theta[succ c]
           proof assume that
A73:          a in c implies ksi.a in ksi.c and
A74:          a in succ c;
A75:          a c= c & ksi.succ c = succ((si.succ c) \/ ksi.c) &
              (si.succ c) \/ ksi.c in succ((si.succ c) \/ ksi.c) &
               ksi.c c= (si.succ c) \/ ksi.c
                by A65,A74,ORDINAL1:34,XBOOLE_1:7;
            ksi.a in ksi.c or ksi.a = ksi.c
             proof
               per cases;
               suppose a <> c;
               then a c< c by A75,XBOOLE_0:def 8;
               hence thesis by A73,ORDINAL1:21;
               suppose a = c;
               hence thesis;
             end;
            hence thesis by A75,ORDINAL1:19,22;
           end;
A76:       for b st b <> 0-element_of W & b is_limit_ordinal &
            for c st c in b holds Theta[c] holds Theta[b]
           proof let b such that
A77:          b <> 0-element_of W & b is_limit_ordinal and
               for c st c in b holds Theta[c] and
A78:          a in b;
A79:          ksi.b = union(ksi|b,b) by A66,A77 .= Union (ksi|b) by Th17
                  .= union rng (ksi|b) by PROB_1:def 3;
               succ a in dom ksi & succ a in b
              by A77,A78,ORDINAL1:41,ORDINAL4:36;
then A80:          ksi.succ a in rng(ksi|b) by FUNCT_1:73;
               ksi.succ a = succ((si.succ a) \/ ksi.a) by A65;
             then (si.succ a) \/ ksi.a in ksi.succ a &
              ksi.a c= (si.succ a) \/ ksi.a by ORDINAL1:10,XBOOLE_1:7;
             then ksi.a in ksi.succ a by ORDINAL1:22;
            hence thesis by A79,A80,TARSKI:def 4;
           end;
            Theta[c] from Universe_Ind(A71,A72,A76);
          then ksi.a in ksi.b by A70;
         hence thesis;
        end;
      defpred P[Ordinal] means si.$1 c= ksi.$1;
A81:    P[0-element_of W] by A64;
A82:    P[a] implies P[succ a]
        proof assume si.a c= ksi.a;
            ksi.succ a = succ((si.succ a) \/ (ksi.a)) &
           (si.succ a) \/ (ksi.a) in succ((si.succ a) \/ (ksi.a)) &
            si.succ a c= (si.succ a) \/ (ksi.a)
             by A65,ORDINAL1:10,XBOOLE_1:7;
          then si.succ a in ksi.succ a by ORDINAL1:22;
         hence si.succ a c= ksi.succ a by ORDINAL1:def 2;
        end;
A83:    a <> 0-element_of W & a is_limit_ordinal implies si.a c= sup (si|a)
        proof assume
A84:       a <> 0-element_of W & a is_limit_ordinal;
         let A such that
A85:       A in si.a;
            si.a = sup (rho.:Funcs(VAR,L.a)) by A63;
         then consider B such that
A86:       B in rho.:Funcs(VAR,L.a) & A c= B by A85,ORDINAL2:29;
         consider x such that
A87:    x in dom rho & x in Funcs(VAR,L.a) & B = rho.x by A86,FUNCT_1:def 12;
         reconsider h = x as Element of Funcs(VAR,M) qua non empty set
           by A57,A87;
         consider a1 being Ordinal of W such that
A88:       a1 = rho.h &
          (ex f being Function of VAR,M st h = f &
           ((ex m being Element of M st m in L.a1 & M,f/(x0,m) |= 'not' H') or
            a1 = 0-element_of W & not ex m being Element of M st
            M,f/(x0,m) |= 'not' H'))&
          for b st
           ex f being Function of VAR,M st h = f &
            ((ex m being Element of M st m in L.b & M,f/(x0,m) |= 'not' H') or
             b = 0-element_of W & not ex m being Element of M st
             M,f/(x0,m) |= 'not' H')
           holds a1 c= b by A58;
         consider f being Function of VAR,M such that
A89:       h = f &
          ((ex m being Element of M st m in L.a1 & M,f/(x0,m) |= 'not' H') or
         a1 = 0-element_of W & not ex m being Element of M st
         M,f/(x0,m) |= 'not' H') by A88;
         defpred P[set,set] means  for a st f.$1 in L.a holds f.$2 in L.a;
A90:      now assume Free 'not' H' <> {}; then
A91:         Free 'not' H' <> {};
A92:         for x,y holds P[x,y] or P[y,x]
             proof let x,y; given a such that
A93:            f.x in L.a & not f.y in L.a;
              let b such that
A94:            f.y in L.b; a in b or a = b or b in a by ORDINAL1:24;
               then L.a c= L.b or L.b c= L.a by A1;
              hence thesis by A93,A94;
             end;
A95:         for x,y,z st P[x,y] & P[y,z] holds P[x,z]
             proof let x,y,z such that
A96:            (for a st f.x in L.a holds f.y in L.a) &
               (for a st f.y in L.a holds f.z in L.a);
              let a; assume f.x in L.a; then f.y in L.a by A96;
              hence f.z in L.a by A96;
             end;
           consider z such that
A97:          z in Free 'not' H' & for y st y in Free 'not' H' holds P[z,y]
             from MaxFinSetElem(A91,A92,A95);
           reconsider z as Variable by A97;
A98:            ex s being Function st f = s & dom s = VAR & rng s c= L.a
             by A87,A89,FUNCT_2:def 2;
            then f.z in rng f by FUNCT_1:def 5;
            then f.z in L.a & L.a = Union (L|a) & Union (L|a) = union rng (L|a
)
             by A1,A68,A84,A98,PROB_1:def 3;
           then consider X such that
A99:         f.z in X & X in rng (L|a) by TARSKI:def 4;
           consider x such that
A100:         x in dom (L|a) & X = (L|a).x by A99,FUNCT_1:def 5;
A101:         dom (L|a) c= a & (L|a).x = L.x by A100,FUNCT_1:70,RELAT_1:87;then
A102:         x in a & a in On W by A100,Th8;
           reconsider x as Ordinal by A100,ORDINAL1:23;
              x in On W by A102,ORDINAL1:19;
           then reconsider x as Ordinal of W by Th8;
           take x; thus x in a by A100,A101;
           let y be Variable; assume y in Free 'not' H';
           hence f.y in L.x by A97,A99,A100,A101;
          end;
            now assume
A103:         Free 'not' H' = {};
           take b = 0-element_of W; thus b in a by A68,A84,ORDINAL3:10;
           thus for x1 st x1 in Free 'not' H' holds f.x1 in L.b by A103;
          end;
         then consider c such that
A104:       c in a & for x1 st x1 in Free 'not' H' holds f.x1 in L.c by A90;
         consider e being Element of L.c;
         defpred C[set] means $1 in Free 'not' H';
         deffunc F(set) = f.$1;
         deffunc G(set) = e;
         consider v being Function such that
A105:       dom v = VAR & for x st x in VAR holds
           (C[x] implies v.x = F(x)) &
           (not C[x] implies v.x = G(x)) from LambdaC;
A106:       rng v c= L.c
           proof let x; assume x in rng v;
            then consider y such that
A107:          y in dom v & x = v.y by FUNCT_1:def 5;
            reconsider y as Variable by A105,A107;
               y in Free 'not' H' or not y in Free 'not' H';
             then x = f.y & f.y in L.c or x = e by A104,A105,A107;
            hence x in L.c;
           end; then
         reconsider v as Function of VAR,L.c by A105,FUNCT_2:def 1,RELSET_1:11;
A108:          L.c c= M by Th24; then
A109:       v in Funcs(VAR,L.c) & v = M!v & Funcs(VAR,L.c) c= Funcs(VAR,M)
           by A105,A106,FUNCT_2:def 2,FUNCT_5:63,ZF_LANG1:def 2;
         then reconsider v' = v as Element of Funcs(VAR,M) qua non empty set;
         consider a2 being Ordinal of W such that
A110:       a2 = rho.v' &
          (ex f being Function of VAR,M st v' = f &
           ((ex m being Element of M st m in L.a2 & M,f/(x0,m) |= 'not' H') or
            a2 = 0-element_of W & not ex m being Element of M st
            M,f/(x0,m) |= 'not' H'))&
          for b st
           ex f being Function of VAR,M st v' = f &
            ((ex m being Element of M st m in L.b & M,f/(x0,m) |= 'not' H') or
             b = 0-element_of W & not ex m being Element of M st
             M,f/(x0,m) |= 'not' H')
           holds a2 c= b by A58;
         consider f' being Function of VAR,M such that
A111:       v' = f' &
           ((ex m being Element of M st m in L.a2 & M,f'/(x0,m) |= 'not' H') or
            a2 = 0-element_of W & not ex m being Element of M st
            M,f'/(x0,m) |= 'not' H') by A110;
A112:       now assume
A113:         not ex m being Element of M st M,f/(x0,m) |= 'not' H';
              now let m be Element of M;
A114:           not M,f/(x0,m) |= 'not' H' by A113;
                now let x1; assume
               x1 in Free 'not' H';
                then f.x1 = (M!v).x1 & f/(x0,m).x0 = m & (M!v)/(x0,m).x0 = m &
                (x1 <> x0 implies f/(x0,m).x1 = f.x1 &
                                  (M!v)/(x0,m).x1 = (M!v).x1)
                 by A105,A109,ZF_LANG1:def 1;
               hence f/(x0,m).x1 = (M!v)/(x0,m).x1;
              end;
             hence not M,(M!v)/(x0,m) |= 'not' H' by A114,ZF_LANG1:84;
            end;
           hence a1 = a2 by A89,A109,A111,A113;
          end;
            now given m being Element of M such that
A115:         m in L.a1 & M,f/(x0,m) |= 'not' H';
              now let x1; assume
             x1 in Free 'not' H';
              then f.x1 = (M!v).x1 & f/(x0,m).x0 = m & (M!v)/(x0,m).x0 = m &
              (x1 <> x0 implies f/(x0,m).x1 = f.x1 &
                                (M!v)/(x0,m).x1 = (M!v).x1)
               by A105,A109,ZF_LANG1:def 1;
             hence f/(x0,m).x1 = (M!v)/(x0,m).x1;
            end;
then A116:         M,(M!v)/(x0,m) |= 'not' H' by A115,ZF_LANG1:84;
           then consider m' being Element of M such that
A117:         m' in L.a2 & M,f'/(x0,m') |= 'not' H' by A109,A111;
              now let x1; assume
             x1 in Free 'not' H';
              then f.x1 = (M!v).x1 & f/(x0,m').x0 = m' & (M!v)/(x0,m').x0 = m'
&
              (x1 <> x0 implies f/(x0,m').x1 = f.x1 &
                                (M!v)/(x0,m').x1 = (M!v).x1)
               by A105,A109,ZF_LANG1:def 1;
             hence f/(x0,m').x1 = f'/(x0,m').x1 by A108,A111,ZF_LANG1:def 2;
            end;
         then M,f/(x0,m') |= 'not' H' by A117,ZF_LANG1:84;
            then a1 c= a2 & a2 c= a1 by A88,A89,A109,A110,A115,A116,A117;
           hence a1 = a2 by XBOOLE_0:def 10;
          end;
          then B in rho.:Funcs(VAR,L.c) & si.c = sup (rho.:Funcs(VAR,L.c)) &
           c in dom si & dom (si|a) = dom si /\ a
            by A57,A63,A87,A88,A89,A109,A110,A112,FUNCT_1:def 12,ORDINAL4:36,
RELAT_1:90;
then A118:       B in si.c & si.c = (si|a).c & c in dom (si|a)
           by A104,FUNCT_1:72,ORDINAL2:27,XBOOLE_0:def 3;
          then si.c in rng (si|a) & sup (si|a) = sup rng (si|a)
           by FUNCT_1:def 5,ORDINAL2:35;
          then si.c in sup (si|a) by ORDINAL2:27;
          then B in sup (si|a) by A118,ORDINAL1:19;
         hence thesis by A86,ORDINAL1:22;
        end;
A119:    a <> 0-element_of W & a is_limit_ordinal &
         (for b st b in a holds P[b]) implies P[a]
        proof assume that
A120:       a <> 0-element_of W & a is_limit_ordinal and
A121:       for b st b in a holds si.b c= ksi.b;
         thus si.a c= ksi.a
         proof let A such that
A122:       A in si.a;
            si.a c= sup (si|a) by A83,A120;
          then A in sup (si|a) & sup (si|a) = sup rng (si|a)
           by A122,ORDINAL2:35;
         then consider B such that
A123:       B in rng (si|a) & A c= B by ORDINAL2:29;
         consider x such that
A124:       x in dom (si|a) & B = (si|a).x by A123,FUNCT_1:def 5;
         reconsider x as Ordinal by A124,ORDINAL1:23;
          A125: dom (si|a) c= a by RELAT_1:87; then
A126:       x in a & a in On W by A124,Th8;
          then x in On W by ORDINAL1:19;
         then reconsider x as Ordinal of W by Th8;
            si.x = B & si.x c= ksi.x & dom ksi = On W
           by A121,A124,A125,FUNCT_1:70,ORDINAL4:def 3;
          then A c= ksi.x & ksi.x in ksi.a
          by A69,A123,A126,ORDINAL2:def 16,XBOOLE_1:1;
         hence thesis by ORDINAL1:22;
         end;
        end;
A127:     P[a] from Universe_Ind(A81,A82,A119);
A128:     ksi is continuous
        proof let A,B; assume
A129:       A in dom ksi & A <> {} & A is_limit_ordinal & B = ksi.A;
         then reconsider a = A as Ordinal of W by A67,Th8;
            A c= dom ksi by A129,ORDINAL1:def 2;
then A130:       dom (ksi|A) = A & ksi|A is increasing
           by A69,ORDINAL4:15,RELAT_1:91;
then A131:       sup (ksi|A) is_limes_of ksi|A & sup (ksi|A) = sup rng (ksi|A)
           by A129,ORDINAL2:35,ORDINAL4:8;
A132:       B = union(ksi|a,a) by A66,A68,A129 .= Union (ksi|a) by Th17
           .= union rng (ksi|a) by PROB_1:def 3;
A133:       B c= sup (ksi|A)
           proof let C; assume C in B;
            then consider X such that
A134:          C in X & X in rng (ksi|A) by A132,TARSKI:def 4;
            consider A1 being Ordinal such that
A135:          rng (ksi|A) c= A1 by ORDINAL2:def 8;
             reconsider X as Ordinal by A134,A135,ORDINAL1:23;
               X in sup (ksi|A) by A131,A134,ORDINAL2:27;
            hence C in sup (ksi|A) by A134,ORDINAL1:19;
           end;
            sup (ksi|A) c= B
           proof let C; assume C in sup (ksi|A);
            then consider D being Ordinal such that
A136:          D in rng (ksi|A) & C c= D by A131,ORDINAL2:29;
            consider x such that
A137:          x in dom (ksi|A) & D = (ksi|A).x by A136,FUNCT_1:def 5;
            reconsider x as Ordinal by A137,ORDINAL1:23;
               x in succ x & succ x in A by A129,A130,A137,ORDINAL1:10,41;
             then D in (ksi|A).succ x & (ksi|A).succ x in rng (ksi|A)
              by A130,A137,FUNCT_1:def 5,ORDINAL2:def 16;
             then D in B by A132,TARSKI:def 4;
            hence thesis by A136,ORDINAL1:22;
           end;
         hence thesis by A131,A133,XBOOLE_0:def 10;
        end;
         now assume x0 in Free H';
        thus thesis
         proof take gamma = phi*ksi;
             ex f being Ordinal-Sequence st f = phi*ksi & f is increasing
            by A45,A69,ORDINAL4:13;
          hence gamma is increasing & gamma is continuous
            by A45,A69,A128,ORDINAL4:17;
          let a such that
A138:         gamma.a = a & {} <> a;
             a in dom gamma & ksi.a in dom phi & a in
 dom ksi by ORDINAL4:36;
           then ksi.a c= phi.(ksi.a) & a c= ksi.a & phi.(ksi.a) = gamma.a
            by A45,A69,FUNCT_1:22,ORDINAL4:10;
then A139:        ksi.a = a & phi.a = a by A138,XBOOLE_0:def 10;
A140:        L.a c= M by Th24;
          let f;
          thus M,M!f |= H implies L.a,f |= H
            proof assume A141: M,M!f |= H;
                now let g be Function of VAR,L.a such that
A142:             for k st g.k <> f.k holds x0 = k;
                  now let k; L.a c= M by Th24;
                  then M!f = f & M!g = g by ZF_LANG1:def 2;
                 hence (M!g).k <> (M!f).k implies x0 = k by A142;
                end;
                then M,(M!g) |= H' by A44,A141,ZF_MODEL:16;
               hence L.a,g |= H' by A46,A138,A139;
              end;
             hence thesis by A44,ZF_MODEL:16;
            end;
          assume that
A143:        L.a,f |= H and
A144:        not M,M!f |= H;
          consider m being Element of M such that
A145:       not M,(M!f)/(x0,m) |= H' by A44,A144,ZF_LANG1:80;
A146:        M,(M!f)/(x0,m) |= 'not' H' by A145,ZF_MODEL:14;
A147:        M!f in Funcs(VAR,M) & f in Funcs(VAR,L.a) by FUNCT_2:11;
          reconsider h = M!f as Element of Funcs(VAR,M) qua non empty set by
FUNCT_2:11;
          consider a1 being Ordinal of W such that
A148:        a1 = rho.h &
           (ex f being Function of VAR,M st h = f &
            ((ex m being Element of M st m in L.a1 & M,f/(x0,m) |= 'not' H') or
             a1 = 0-element_of W & not ex m being Element of M st
             M,f/(x0,m) |= 'not' H'))&
           for b st
            ex f being Function of VAR,M st h = f &
             ((ex m being Element of M st m in L.b & M,f/(x0,m) |= 'not' H') or
              b = 0-element_of W & not ex m being Element of M st
              M,f/(x0,m) |= 'not' H')
            holds a1 c= b by A58;
          consider m being Element of M such that
A149:        m in L.a1 & M,(M!f)/(x0,m) |= 'not' H' by A146,A148;
A150:        M!f = f by A140,ZF_LANG1:def 2;
           then a1 in rho.:Funcs(VAR,L.a) & si.a = sup (rho.:Funcs(VAR,L.a))
            by A57,A63,A147,A148,FUNCT_1:def 12;
           then a1 in si.a & si.a c= ksi.a by A127,ORDINAL2:27;
           then L.a1 c= L.a by A1,A139;
          then reconsider m' = m as Element of L.a by A149;
             dom ((M!f)/(x0,m)) = VAR & rng ((M!f)/(x0,m)) c= L.a
            proof thus
            dom ((M!f)/(x0,m)) = VAR by FUNCT_2:def 1;
             let x; assume x in rng ((M!f)/(x0,m));
             then consider y such that
A151:           y in
 dom ((M!f)/(x0,m)) & x = ((M!f)/(x0,m)).y by FUNCT_1:def 5;
             reconsider y as Variable by A151,FUNCT_2:def 1;
                y = x0 or y <> x0;
              then x = m' or x = f.y by A150,A151,ZF_LANG1:def 1;
             hence thesis;
            end;
          then reconsider g = (M!f)/(x0,m) as Function of VAR,L.a by FUNCT_2:
def 1,RELSET_1:11;
              g.x0 = m' & for y be Variable holds g.y <> f.y implies x0 = y
 by A150,ZF_LANG1:def 1;
           then (M!f)/(x0,m) = f/(x0,m') by ZF_LANG1:def 1;
           then (M!f)/(x0,m) = M!(f/(x0,m')) by A140,ZF_LANG1:def 2;
           then not M,M!(f/(x0,m')) |= H' by A149,ZF_MODEL:14;
           then not L.a,f/(x0,m') |= H' by A46,A138,A139;
          hence contradiction by A44,A143,ZF_LANG1:80;
         end;
       end;
      hence thesis by A47;
     end;
   thus RT[H] from ZF_Ind(A4,A23,A29,A43);
  end;

Back to top