The Mizar article:

Increasing and Continuous Ordinal Sequences

by
Grzegorz Bancerek

Received May 31, 1990

Copyright (c) 1990 Association of Mizar Users

MML identifier: ORDINAL4
[ MML identifier index ]


environ

 vocabulary ORDINAL2, ORDINAL1, FUNCT_1, TARSKI, RELAT_1, BOOLE, FINSEQ_1,
      ORDINAL3, CLASSES2, CLASSES1, CARD_1, ORDINAL4;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1,
      ORDINAL2, ORDINAL3, CARD_1, CLASSES1, CLASSES2;
 constructors WELLORD2, ORDINAL3, CARD_1, CLASSES1, CLASSES2, XBOOLE_0;
 clusters FUNCT_1, ORDINAL1, ORDINAL2, ORDINAL3, CLASSES2, ARYTM_3, CARD_1,
      ZFMISC_1, XBOOLE_0;
 requirements SUBSET, BOOLE;
 definitions TARSKI, ORDINAL2, XBOOLE_0;
 theorems ZFMISC_1, FUNCT_1, GRFUNC_1, ORDINAL1, ORDINAL2, ORDINAL3, CARD_2,
      CLASSES2, RELAT_1, CLASSES1, XBOOLE_0, XBOOLE_1;
 schemes ORDINAL1, ORDINAL2, PARTFUN1;

begin

 reserve phi,fi,psi for Ordinal-Sequence,
         A,A1,B,C,D for Ordinal,
         f,g for Function,
         X for set,
         x,y,z for set;

definition let L be Ordinal-Sequence;
  cluster last L -> ordinal;
  coherence
  proof
      last L = L.(union dom L) by ORDINAL2:def 1;
    hence thesis;
  end;
end;

theorem
   dom fi = succ A implies last fi is_limes_of fi & lim fi = last fi
  proof assume
A1:  dom fi = succ A;
then A2:  fi.A is Ordinal & last fi = fi.A by ORDINAL2:7;
   thus last fi is_limes_of fi
     proof per cases;
      case
A3:      last fi = {};
       take A; thus A in dom fi by A1,ORDINAL1:10;
       let B; assume
A4:      A c= B & B in dom fi;
        then B c= A by A1,ORDINAL1:34;
       hence fi.B = {} by A2,A3,A4,XBOOLE_0:def 10;
      case last fi <> {};
       let B,C such that
A5:      B in last fi & last fi in C;
       take A; thus A in dom fi by A1,ORDINAL1:10;
       let D; assume
A6:      A c= D & D in dom fi;
        then D c= A by A1,ORDINAL1:34;
       hence thesis by A2,A5,A6,XBOOLE_0:def 10;
     end;
   hence lim fi = last fi by ORDINAL2:def 14;
  end;

definition let fi,psi be T-Sequence;
 func fi^psi -> T-Sequence means:
Def1:    dom it = (dom fi)+^(dom psi) &
   (for A st A in dom fi holds it.A = fi.A) &
   (for A st A in dom psi holds it.((dom fi)+^A) = psi.A);
  existence
   proof
    deffunc F(Ordinal) = fi.$1;
    deffunc G(Ordinal) = psi.(($1)-^dom fi);
    defpred P[set] means $1 in dom fi;
    consider f such that
A1:   dom f = (dom fi)+^(dom psi) and
A2:   for x being set st x in (dom fi)+^(dom psi) holds
      (P[x] implies f.x = F(x)) &
       (not P[x] implies f.x = G(x))
        from LambdaC;
    reconsider f as T-Sequence by A1,ORDINAL1:def 7;
    take f; thus dom f = (dom fi)+^(dom psi) by A1;
    thus for A st A in dom fi holds f.A = fi.A
      proof let A such that
A3:      A in dom fi;
          dom fi c= dom f by A1,ORDINAL3:27; hence thesis by A1,A2,A3;
      end;
    let A; assume A in dom psi;
then A4:   (dom fi)+^A in dom f by A1,ORDINAL2:49;
       dom fi c= (dom fi)+^A by ORDINAL3:27;
     then not (dom fi)+^A in dom fi by ORDINAL1:7;
     then f.((dom fi)+^A) = psi.((((dom fi)+^A))-^dom fi) &
      ((dom fi)+^A)-^dom fi = A by A1,A2,A4,ORDINAL3:65;
    hence thesis;
   end;
  uniqueness
   proof let f1,f2 be T-Sequence such that
A5:  dom f1 = (dom fi)+^(dom psi) &
      (for A st A in dom fi holds f1.A = fi.A) &
      (for A st A in dom psi holds f1.((dom fi)+^A) = psi.A) and
A6:  dom f2 = (dom fi)+^(dom psi) &
      (for A st A in dom fi holds f2.A = fi.A) &
      (for A st A in dom psi holds f2.((dom fi)+^A) = psi.A);
       now let x; assume
A7:     x in (dom fi)+^(dom psi);
      then reconsider A = x as Ordinal by ORDINAL1:23;
         now per cases;
        suppose x in dom fi; then f1.A = fi.A & f2.A = fi.A by A5,A6;
         hence f1.x = f2.x;
        suppose not x in dom fi;
          then dom fi c= A by ORDINAL1:26;
then A8:        (dom fi)+^(A-^dom fi) = A by ORDINAL3:def 6;
          then A-^dom fi in dom psi by A7,ORDINAL3:25;
          then f1.A = psi.(A-^dom fi) & f2.A = psi.(A-^dom fi) by A5,A6,A8;
         hence f1.x = f2.x;
       end;
      hence f1.x = f2.x;
     end;
    hence thesis by A5,A6,FUNCT_1:9;
   end;
end;

definition let fi,psi;
 cluster fi^psi -> Ordinal-yielding;
 coherence
  proof set f = fi^psi;
A1:  dom f = dom fi +^ dom psi by Def1;
    consider A1 being Ordinal such that
A2:  rng fi c= A1 by ORDINAL2:def 8;
    consider A2 being Ordinal such that
A3:  rng psi c= A2 by ORDINAL2:def 8;
       rng f c= A1+^A2
      proof let y; assume y in rng f;
       then consider x such that
A4:     x in dom f & y = f.x by FUNCT_1:def 5;
       reconsider x as Ordinal by A4,ORDINAL1:23;
A5:     A1 c= A1+^A2 & A2 c= A1+^A2 by ORDINAL3:27;
          now per cases;
         suppose x in dom fi;
           then y = fi.x & fi.x in rng fi by A4,Def1,FUNCT_1:def 5;
           then y in A1 by A2;
          hence thesis by A5;
         suppose not x in dom fi;
           then dom fi c= x by ORDINAL1:26;
then A6:        (dom fi)+^(x-^dom fi) = x
             by ORDINAL3:def 6;
then A7:        x-^dom fi in dom psi by A1,A4,ORDINAL3:25;
           then y = psi.(x-^dom fi) by A4,A6,Def1;
           then y in rng psi by A7,FUNCT_1:def 5;
           then y in A2 by A3;
          hence thesis by A5;
        end;
       hence thesis;
      end;
   hence f is Ordinal-yielding by ORDINAL2:def 8;
  end;
end;

canceled;

theorem
 Th3: A is_limes_of psi implies A is_limes_of fi^psi
  proof assume
A1:  A = {} &
    (ex B st B in dom psi & for C st B c= C & C in dom psi holds psi.C = {}) or
    A <> {} &
     for B,C st B in A & A in C ex D st D in dom psi &
      for E being Ordinal st D c= E & E in dom psi holds B in psi.E & psi.E in
 C;
A2:  dom(fi^psi) = (dom fi)+^(dom psi) by Def1;
   per cases;
    case A = {};
     then consider B such that
A3:    B in dom psi & for C st B c= C & C in dom psi holds psi.C = {} by A1;
     take B1 = (dom fi)+^B;
     thus B1 in dom(fi^psi) by A2,A3,ORDINAL2:49;
     let C; assume
A4:    B1 c= C & C in dom(fi^psi);
then A5:    C = B1+^(C-^B1) by ORDINAL3:def 6
 .= (dom fi)+^(B+^(C-^B1)) by ORDINAL3:33;
      then B c= B+^(C-^B1) & B+^(C-^B1) in dom psi by A2,A4,ORDINAL3:25,27;
      then (fi^psi).C = psi.(B+^(C-^B1)) & psi.(B+^(C-^B1)) = {} by A3,A5,Def1
;
     hence thesis;
    case
      A <> {};
     let B,C; assume
      B in A & A in C;
     then consider D such that
A6:     D in dom psi and
A7:     for E being Ordinal st D c= E & E in dom psi holds B in psi.E & psi.E
in C
         by A1;
     take D1 = (dom fi)+^D;
     thus D1 in dom(fi^psi) by A2,A6,ORDINAL2:49;
     let E be Ordinal; assume
A8:    D1 c= E & E in dom(fi^psi);
then A9:    E = D1+^(E-^D1) by ORDINAL3:def 6
 .= (dom fi)+^(D+^(E-^D1)) by ORDINAL3:33;
      then D c= D+^(E-^D1) & D+^(E-^D1) in dom psi by A2,A8,ORDINAL3:25,27;
      then (fi^psi).E = psi.(D+^(E-^D1)) & B in psi.(D+^(E-^D1)) &
      psi.(D+^(E-^D1)) in C
        by A7,A9,Def1;
     hence thesis;
  end;

theorem
    A is_limes_of fi implies B+^A is_limes_of B+^fi
  proof assume
A1:  A = {} &
    (ex B st B in dom fi & for C st B c= C & C in dom fi holds fi.C = {}) or
    A <> {} &
     for B,C st B in A & A in C ex D st D in dom fi &
      for E being Ordinal st D c= E & E in dom fi holds B in fi.E & fi.E in C;
A2:  dom fi = dom(B+^fi) by ORDINAL3:def 2;
   per cases;
    case A3: B+^A = {};
     then consider A1 such that
A4:    A1 in dom fi & for C st A1 c= C & C in dom fi holds fi.C = {}
       by A1,ORDINAL3:29;
     take A1; thus A1 in dom(B+^fi) by A4,ORDINAL3:def 2;
     let C; assume A1 c= C & C in dom(B+^fi);
      then (B+^fi).C = B+^(fi.C) & fi.C = {} & {} = {}
        by A2,A4,ORDINAL3:def 2;
     hence (B+^fi).C = {} by A3,ORDINAL3:29;
    case
      B+^A <> {};
        now per cases;
       suppose
A5:       A = {};
        then consider A1 such that
A6:       A1 in dom fi & for C st A1 c= C & C in dom fi holds fi.C = {} by A1;
        let B1,B2 be Ordinal such that
A7:       B1 in B+^A & B+^A in B2;
        take A1; thus A1 in dom(B+^fi) by A6,ORDINAL3:def 2;
        let C; assume A1 c= C & C in dom(B+^fi);
         then (B+^fi).C = B+^(fi.C) & fi.C = {} & {} = {}
           by A2,A6,ORDINAL3:def 2;
        hence B1 in (B+^fi).C & (B+^fi).C in B2 by A5,A7;
       suppose
A8:       A <> {};
        let B1,B2 be Ordinal; assume
           B1 in B+^A & B+^A in B2;
then A9:       B1-^B in A & A in B2-^B & B+^A c= B2
          by A8,ORDINAL1:def 2,ORDINAL3:73,74;
        then consider A1 such that
A10:       A1 in dom fi &
          for C st A1 c= C & C in dom fi holds B1-^B in fi.C & fi.C in
 B2-^B by A1;
        take A1; thus A1 in dom(B+^fi) by A10,ORDINAL3:def 2;
           B c= B+^A by ORDINAL3:27;
then A11:       B c= B2 & B1 c= B+^(B1-^B) by A9,ORDINAL3:75,XBOOLE_1:1;
        let C; assume
A12:       A1 c= C & C in dom(B+^fi);
        reconsider E = fi.C as Ordinal;
A13:       (B+^fi).C = B+^(fi.C) & B1-^B in E & E in B2-^B & E = E &
           B+^(B2-^B) = B2
            by A2,A10,A11,A12,ORDINAL3:def 2,def 6;
         then B+^(B1-^B) in B+^E by ORDINAL2:49;
        hence B1 in (B+^fi).C & (B+^fi).C in B2 by A11,A13,ORDINAL1:22,ORDINAL2
:49;
      end;
     hence for A1,C st A1 in B+^A & B+^A in C ex D st D in dom(B+^fi) &
       for E being Ordinal st D c= E & E in dom(B+^fi) holds
        A1 in (B+^fi).E & (B+^fi).E in C;
  end;

 Lm1: A is_limes_of fi implies dom fi <> {}
  proof assume
A1:  A = {} &
    (ex B st B in dom fi & for C st B c= C & C in dom fi holds fi.C = {}) or
    A <> {} &
     for B,C st B in A & A in C ex D st D in dom fi &
      for E being Ordinal st D c= E & E in dom fi holds B in fi.E & fi.E in C;
      now per cases;
     suppose A = {};
      hence thesis by A1;
     suppose
       A <> {};
       then {} in A & A in succ A by ORDINAL1:10,ORDINAL3:10;
       then ex B st B in dom fi &
        for C st B c= C & C in dom fi holds {} in fi.C & fi.C in succ A by A1;
      hence thesis;
    end;
   hence thesis;
  end;

theorem
 Th5: A is_limes_of fi implies A*^B is_limes_of fi*^B
  proof assume
A1:  A is_limes_of fi;
then A2:  dom fi = dom(fi*^B) & dom fi <> {} by Lm1,ORDINAL3:def 5;
   per cases;
    case A*^B = {};
then A3:    B = {} or A = {} by ORDINAL3:34;
        now per cases;
       suppose
A4:      B = {};
        consider x being Element of dom fi;
        reconsider x as Ordinal;
        take A1 = x; thus A1 in dom(fi*^B) by A2;
        let C; assume A1 c= C & C in dom(fi*^B);
        hence (fi*^B).C = (fi.C)*^B by A2,ORDINAL3:def 5
                      .= {} by A4,ORDINAL2:55;
       suppose B <> {};
        then consider A1 such that
A5:      A1 in dom fi & for C st A1 c= C & C in dom fi holds fi.C = {}
          by A1,A3,ORDINAL2:def 13;
        take A1; thus A1 in dom(fi*^B) by A5,ORDINAL3:def 5;
        let C; assume A1 c= C & C in dom(fi*^B);
         then (fi*^B).C = (fi.C)*^B & fi.C = {} & {} = {}
          by A2,A5,ORDINAL3:def 5;
        hence (fi*^B).C = {} by ORDINAL2:52;
      end;
     hence ex A1 st A1 in dom(fi*^B) &
       for C st A1 c= C & C in dom(fi*^B) holds (fi*^B).C = {};
    case A*^B <> {};
then A6:    A <> {} & B <> {} by ORDINAL2:52,55;
     let B1,B2 be Ordinal such that
A7:    B1 in A*^B & A*^B in B2;
A8:    now given A1 such that
A9:     A = succ A1;
          A1 in A & A in succ A by A9,ORDINAL1:10;
       then consider D such that
A10:     D in dom fi &
         for C st D c= C & C in dom fi holds A1 in fi.C & fi.C in succ A by A1,
ORDINAL2:def 13;
       take D; thus D in dom(fi*^B) by A10,ORDINAL3:def 5;
       let C; assume
A11:     D c= C & C in dom(fi*^B);
       reconsider E = fi.C as Ordinal;
A12:     A1 in E & E in succ A & (fi*^B).C = E*^B by A2,A10,A11,ORDINAL3:def 5;
        then A c= E & E c= A by A9,ORDINAL1:33,34;
       hence B1 in (fi*^B).C & (fi*^B).C in B2 by A7,A12,XBOOLE_0:def 10;
      end;
        now assume not ex A1 st A = succ A1;
        then A is_limit_ordinal by ORDINAL1:42;
       then consider C such that
A13:      C in A & B1 in C*^B by A7,ORDINAL3:49;
          A in succ A by ORDINAL1:10;
       then consider D such that
A14:      D in dom fi &
         for A1 st D c= A1 & A1 in dom fi holds C in fi.A1 & fi.A1 in succ A
          by A1,A13,ORDINAL2:def 13;
       take D; thus D in dom(fi*^B) by A14,ORDINAL3:def 5;
       let A1; assume
A15:      D c= A1 & A1 in dom(fi*^B);
       reconsider E = fi.A1 as Ordinal;
          C in fi.A1 & fi.A1 in succ A by A2,A14,A15;
        then C*^B in E*^B & E c= A by A6,ORDINAL1:34,ORDINAL2:57;
        then B1 in E*^B & E*^B c= A*^B & E = E &
        (fi*^B).A1 = (fi.A1)*^B
         by A2,A13,A15,ORDINAL1:19,ORDINAL2:58,ORDINAL3:def 5;
       hence B1 in (fi*^B).A1 & (fi*^B).A1 in B2 by A7,ORDINAL1:22;
      end;
     hence thesis by A8;
  end;

theorem
 Th6: dom fi = dom psi & B is_limes_of fi & C is_limes_of psi &
  ((for A st A in dom fi holds fi.A c= psi.A) or
    (for A st A in dom fi holds fi.A in psi.A)) implies B c= C
  proof assume that
A1: dom fi = dom psi and
A2: B = {} &
    (ex A1 st A1 in dom fi & for C st A1 c= C & C in dom fi holds fi.C = {}) or
    B <> {} &
     for A1,C st A1 in B & B in C ex D st D in dom fi &
      for E being Ordinal st D c= E & E in dom fi holds A1 in fi.E & fi.E in
 C and
A3: C = {} & (ex B st B in dom psi &
      for A1 st B c= A1 & A1 in dom psi holds psi.A1 = {}) or
    C <> {} &
     for B,A1 st B in C & C in A1 ex D st D in dom psi &
      for E being Ordinal st D c= E & E in dom psi holds B in psi.E & psi.E in
 A1
   and
A4:  (for A st A in dom fi holds fi.A c= psi.A) or
     (for A st A in dom fi holds fi.A in psi.A);
A5:  now let A; assume
A6:   A in dom fi;
     reconsider A1 = fi.A, A2 = psi.A as Ordinal;
        A1 c= A2 or A1 in A2 by A4,A6;
     hence fi.A c= psi.A by ORDINAL1:def 2;
    end;
      now per cases;
     suppose B = {} & C = {}; hence thesis;
     suppose B = {} & C <> {}; then B in C by ORDINAL3:10;
      hence thesis by ORDINAL1:def 2;
     suppose
A7:     B <> {} & C = {};
      then consider A1 such that
A8:    A1 in dom psi & for A st A1 c= A & A in dom psi holds psi.A = {} by A3;
         {} in B & B in succ B by A7,ORDINAL1:10,ORDINAL3:10;
      then consider A2 being Ordinal such that
A9:    A2 in dom fi & for A st A2 c= A & A in dom fi holds
        {} in fi.A & fi.A in succ B by A2;
         A1 c= A1 \/ A2 & A2 c= A1 \/ A2 & (A1 \/ A2 = A1 or A1 \/ A2 = A2)
        by ORDINAL3:15,XBOOLE_1:7;
       then psi.(A1 \/ A2) = {} & {} in fi.(A1 \/ A2) &
        fi.(A1 \/ A2) c= psi.(A1 \/ A2) by A1,A5,A8,A9;
      hence thesis;
     suppose
A10:     B <> {} & C <> {};
      assume not B c= C;
     then C in B & B in succ B by ORDINAL1:10,26;
      then consider A1 such that
A11:    A1 in dom fi & for A st A1 c= A & A in dom fi holds
        C in fi.A & fi.A in succ B by A2;
         {} in C & C in succ C by A10,ORDINAL1:10,ORDINAL3:10;
      then consider A2 being Ordinal such that
A12:    A2 in dom psi & for A st A2 c= A & A in dom psi holds
        {} in psi.A & psi.A in succ C by A3;
         A1 c= A1 \/ A2 & A2 c= A1 \/ A2 & (A1 \/ A2 = A1 or A1 \/ A2 = A2)
        by ORDINAL3:15,XBOOLE_1:7;
then A13:     psi.(A1 \/ A2) in succ C & C in fi.(A1 \/ A2) & A1 \/ A2 in dom
psi &
        fi.(A1 \/ A2) c= psi.(A1 \/ A2) by A1,A5,A11,A12;
      reconsider A3 = psi.(A1 \/ A2) as Ordinal;
         A3 c= C & C in A3 by A13,ORDINAL1:34;
      hence contradiction by ORDINAL1:7;
    end;
   hence thesis;
  end;

 reserve f1,f2 for Ordinal-Sequence;

theorem
   dom f1 = dom fi & dom fi = dom f2 & A is_limes_of f1 & A is_limes_of f2 &
  (for A st A in dom fi holds f1.A c= fi.A & fi.A c= f2.A) implies
    A is_limes_of fi
  proof assume that
A1: dom f1 = dom fi & dom fi = dom f2 and
A2: A = {} &
    (ex B st B in dom f1 & for C st B c= C & C in dom f1 holds f1.C = {}) or
    A <> {} &
     for B,C st B in A & A in C ex D st D in dom f1 &
      for E being Ordinal st D c= E & E in dom f1 holds B in f1.E & f1.E in
 C and
A3: A = {} &
    (ex B st B in dom f2 & for C st B c= C & C in dom f2 holds f2.C = {}) or
    A <> {} &
     for B,C st B in A & A in C ex D st D in dom f2 &
      for E being Ordinal st D c= E & E in dom f2 holds B in f2.E & f2.E in
 C and
A4: for A st A in dom fi holds f1.A c= fi.A & fi.A c= f2.A;
   per cases;
    case
      A = {};
     then consider B being Ordinal such that
A5:    B in dom f2 & for C st B c= C & C in dom f2 holds f2.C = {} by A3;
     take B; thus B in dom fi by A1,A5;
     let C; assume B c= C & C in dom fi;
      then f2.C = {} & fi.C c= f2.C by A1,A4,A5;
     hence fi.C = {} by XBOOLE_1:3;
    case
      A <> {};
     let B,C; assume
A6:    B in A & A in C;
     then consider D1 being Ordinal such that
A7:    D1 in dom f1 &
       for A1 st D1 c= A1 & A1 in dom f1 holds B in f1.A1 & f1.A1 in C by A2;
     consider D2 being Ordinal such that
A8:    D2 in dom f2 &
       for A1 st D2 c= A1 & A1 in dom f2 holds B in f2.A1 & f2.A1 in
 C by A3,A6;
     take D = D1 \/ D2;
     thus D in dom fi by A1,A7,A8,ORDINAL3:15;
     let A1; assume
A9:    D c= A1 & A1 in dom fi;
     reconsider B1 = fi.A1, B2 = f2.A1 as Ordinal;
        D1 c= D & D2 c= D by XBOOLE_1:7;
      then D1 c= A1 & D2 c= A1 by A9,XBOOLE_1:1;
      then B in f1.A1 & f1.A1 c= fi.A1 & B1 c= B2 & B2 in C by A1,A4,A7,A8,A9;
     hence thesis by ORDINAL1:22;
  end;

theorem
 Th8: dom fi <> {} & dom fi is_limit_ordinal & fi is increasing implies
   sup fi is_limes_of fi & lim fi = sup fi
  proof assume that
A1: dom fi <> {} & dom fi is_limit_ordinal and
A2: A in B & B in dom fi implies fi.A in fi.B;
A3: sup fi = sup rng fi by ORDINAL2:35;
A4: {} in dom fi by A1,ORDINAL3:10;
   reconsider x = fi.{} as Ordinal;
A5:    x in rng fi by A4,FUNCT_1:def 5;
   thus sup fi is_limes_of fi
     proof per cases;
      case sup fi = {}; hence thesis by A3,A5,ORDINAL2:27;
      case sup fi <> {};
       let A,B; assume
A6:      A in sup fi & sup fi in B;
       then consider C such that
A7:      C in rng fi & A c= C by A3,ORDINAL2:29;
       consider x such that
A8:      x in dom fi & C = fi.x by A7,FUNCT_1:def 5;
       reconsider x as Ordinal by A8,ORDINAL1:23;
       take M = succ x; thus M in dom fi by A1,A8,ORDINAL1:41;
       let D; assume
A9:      M c= D & D in dom fi;
       reconsider E = fi.D as Ordinal;
          x in M by ORDINAL1:10;
        then C in E by A2,A8,A9;
       hence A in fi.D by A7,ORDINAL1:22;
          fi.D in rng fi by A9,FUNCT_1:def 5;
        then E in sup fi by A3,ORDINAL2:27;
       hence thesis by A6,ORDINAL1:19;
     end;
   hence lim fi = sup fi by ORDINAL2:def 14;
  end;

theorem
 Th9: fi is increasing & A c= B & B in dom fi implies fi.A c= fi.B
  proof assume that
A1:  for A,B st A in B & B in dom fi holds fi.A in fi.B and
A2:  A c= B & B in dom fi;
   reconsider C = fi.B as Ordinal;
      now per cases;
     suppose A = B; hence thesis;
     suppose A <> B;
       then A c< B by A2,XBOOLE_0:def 8;
       then A in B by ORDINAL1:21;
       then fi.A in C by A1,A2;
      hence thesis by ORDINAL1:def 2;
    end;
   hence thesis;
  end;

theorem
 Th10: fi is increasing & A in dom fi implies A c= fi.A
  proof assume that
A1:  for A,B st A in B & B in dom fi holds fi.A in fi.B and
A2:  A in dom fi & not A c= fi.A;
    defpred P[set] means
     $1 in dom fi & not $1 c= fi.$1;
A3:  ex A st P[A] by A2;
   consider A such that
A4:  P[A] and
A5:  for B st P[B] holds A c= B from Ordinal_Min(A3);
   reconsider B = fi.A as Ordinal;
A6:  B in A by A4,ORDINAL1:26;
    then fi.B in B by A1,A4;
    then B in dom fi & not B c= fi.B by A4,A6,ORDINAL1:7,19;
   hence contradiction by A4,A5;
  end;

theorem
 Th11: phi is increasing implies phi"A is Ordinal
  proof assume
A1:  for A,B st A in B & B in dom phi holds phi.A in phi.B;
      now let X; assume X in phi"A;
then A2:    X in dom phi & phi.X in A by FUNCT_1:def 13;
     hence X is Ordinal by ORDINAL1:23;
     reconsider B = X as Ordinal by A2,ORDINAL1:23;
     thus X c= phi"A
       proof let x; assume A3: x in X;
then A4:       x in B;
        then reconsider C = x, D = phi.B as Ordinal by ORDINAL1:23;
A5:       C in dom phi by A2,A4,ORDINAL1:19;
        reconsider E = phi.C as Ordinal;
           E in D by A1,A2,A3;
         then phi.x in A by A2,ORDINAL1:19;
        hence thesis by A5,FUNCT_1:def 13;
       end;
    end;
   hence thesis by ORDINAL1:31;
  end;

theorem
 Th12: f1 is increasing implies f2*f1 is Ordinal-Sequence
  proof assume
A1:  f1 is increasing;
      dom(f2*f1) = f1"dom f2 by RELAT_1:182;
    then dom(f2*f1) is Ordinal by A1,Th11;
   then reconsider f = f2*f1 as T-Sequence by ORDINAL1:def 7;
   consider A such that
A2:  rng f2 c= A by ORDINAL2:def 8;
      rng f c= rng f2 by RELAT_1:45;
    then rng f c= A by A2,XBOOLE_1:1;
   hence thesis by ORDINAL2:def 8;
  end;

theorem
   f1 is increasing & f2 is increasing implies
   ex phi st phi = f1*f2 & phi is increasing
  proof assume
A1:  f1 is increasing & f2 is increasing;
   then reconsider f = f1*f2 as Ordinal-Sequence by Th12;
   take f; thus f = f1*f2;
   let A,B; assume
A2:  A in B & B in dom f;
then A3:  A in dom f by ORDINAL1:19;
    A4: dom f c= dom f2 by RELAT_1:44;
   reconsider A1 = f2.A, B1 = f2.B as Ordinal;
      A1 in B1 & B1 in dom f1 by A1,A2,A4,FUNCT_1:21,ORDINAL2:def 16;
    then f.A = f1.A1 & f.B = f1.B1 & f1.A1 in f1.B1 by A1,A2,A3,FUNCT_1:22,
ORDINAL2:def 16;
   hence thesis;
  end;

theorem Th14:
 f1 is increasing & A is_limes_of f2 & sup rng f1 = dom f2 &
   fi = f2*f1 implies A is_limes_of fi
  proof assume that
A1:  f1 is increasing and
A2:  A = {} & (ex B st B in dom f2 &
      for C st B c= C & C in dom f2 holds f2.C = {}) or
    A <> {} &
      for B,C st B in A & A in C ex D st D in dom f2 &
       for E being Ordinal st D c= E & E in dom f2 holds B in f2.E & f2.E in
 C and
A3:  sup rng f1 = dom f2 & fi = f2*f1;
   per cases;
    case A = {};
     then consider B such that
A4:    B in dom f2 & for C st B c= C & C in dom f2 holds f2.C = {} by A2;
     consider B1 being Ordinal such that
A5:    B1 in rng f1 & B c= B1 by A3,A4,ORDINAL2:29;
     consider x such that
A6:    x in dom f1 & B1 = f1.x by A5,FUNCT_1:def 5;
     reconsider x as Ordinal by A6,ORDINAL1:23;
     take x; B1 in dom f2 by A3,A5,ORDINAL2:27;
     hence x in dom fi by A3,A6,FUNCT_1:21;
     let C such that
A7:    x c= C & C in dom fi;
      A8: dom fi c= dom f1 by A3,RELAT_1:44;
     reconsider C1 = f1.C as Ordinal;
        B1 c= C1 by A1,A6,A7,A8,Th9;
then A9:    B c= C1 by A5,XBOOLE_1:1;
        C1 in rng f1 by A7,A8,FUNCT_1:def 5;
      then C1 in dom f2 by A3,ORDINAL2:27;
      then f2.C1 = {} by A4,A9;
     hence thesis by A3,A7,FUNCT_1:22;
    case
      A <> {};
     let B,C; assume
      B in A & A in C;
     then consider D such that
A10:    D in dom f2 & for A1 st D c= A1 & A1 in dom f2 holds B in f2.A1 & f2.A1
in
 C
        by A2;
     consider B1 being Ordinal such that
A11:    B1 in rng f1 & D c= B1 by A3,A10,ORDINAL2:29;
     consider x such that
A12:    x in dom f1 & B1 = f1.x by A11,FUNCT_1:def 5;
     reconsider x as Ordinal by A12,ORDINAL1:23;
     take x; B1 in dom f2 by A3,A11,ORDINAL2:27;
     hence x in dom fi by A3,A12,FUNCT_1:21;
     let E be Ordinal such that
A13:    x c= E & E in dom fi;
      A14: dom fi c= dom f1 by A3,RELAT_1:44;
     reconsider E1 = f1.E as Ordinal;
        B1 c= E1 by A1,A12,A13,A14,Th9;
then A15:    D c= E1 by A11,XBOOLE_1:1;
        E1 in rng f1 by A13,A14,FUNCT_1:def 5;
      then E1 in dom f2 by A3,ORDINAL2:27;
      then B in f2.E1 & f2.E1 in C by A10,A15;
     hence thesis by A3,A13,FUNCT_1:22;
  end;

theorem
 Th15: phi is increasing implies phi|A is increasing
  proof assume
A1:  for A,B st A in B & B in dom phi holds phi.A in phi.B;
   let B,C such that
A2:  B in C & C in dom (phi|A);
      dom (phi|A) c= dom phi by FUNCT_1:76;
    then B in dom (phi|A) & C in dom phi by A2,ORDINAL1:19;
    then phi.B in phi.C & phi.B = (phi|A).B & phi.C = (phi|A).C by A1,A2,
FUNCT_1:70;
   hence thesis;
  end;

theorem
 Th16: phi is increasing & dom phi is_limit_ordinal implies
   sup phi is_limit_ordinal
  proof assume
A1:  phi is increasing & dom phi is_limit_ordinal;
A2:  sup phi = sup rng phi by ORDINAL2:35;
      now let A; assume A in sup phi;
     then consider B such that
A3:    B in rng phi & A c= B by A2,ORDINAL2:29;
     consider x such that
A4:    x in dom phi & B = phi.x by A3,FUNCT_1:def 5;
     reconsider x as Ordinal by A4,ORDINAL1:23;
A5:    x in succ x & succ x in dom phi by A1,A4,ORDINAL1:10,41;
     reconsider C = phi.succ x as Ordinal;
        B in C & C in rng phi by A1,A4,A5,FUNCT_1:def 5,ORDINAL2:def 16;
      then succ B c= C & C in sup phi by A2,ORDINAL1:33,ORDINAL2:27;
      then succ A c= succ B & succ B in sup phi by A3,ORDINAL1:22,ORDINAL2:1;
     hence succ A in sup phi by ORDINAL1:22;
    end;
   hence thesis by ORDINAL1:41;
  end;

 Lm2: rng f c= X implies (g|X)*f = g*f
  proof assume rng f c= X;
    then f"rng f c= f"X & f"X c= dom f & f"rng f = dom f
     by RELAT_1:167,169,178;
then A1:  f"X = dom f & f"dom g c= dom f by RELAT_1:167,XBOOLE_0:def 10;
A2:  dom ((g|X)*f) = f"(dom (g|X)) by RELAT_1:182
                 .= f"(dom g /\ X) by RELAT_1:90
                 .= f"(dom g) /\ f"X by FUNCT_1:137
                 .= f"(dom g) by A1,XBOOLE_1:28
                 .= dom (g*f) by RELAT_1:182;
      (g|X)*f c= g*f by GRFUNC_1:54;
   hence thesis by A2,GRFUNC_1:9;
  end;

theorem
   fi is increasing & fi is continuous & psi is continuous &
   phi = psi*fi implies phi is continuous
  proof assume that
A1: fi is increasing and
A2: for A,B st A in dom fi & A <> {} & A is_limit_ordinal & B = fi.A
         holds B is_limes_of fi|A and
A3: for A,B st A in dom psi & A <> {} & A is_limit_ordinal & B = psi.A
         holds B is_limes_of psi|A and
A4: phi = psi*fi;
   let A,B such that
A5:  A in dom phi & A <> {} & A is_limit_ordinal & B = phi.A;
  A6: dom phi c= dom fi & rng phi c= rng psi by A4,RELAT_1:44,45;
   reconsider A1 = fi.A as Ordinal;
A7:    rng (fi|A) c= sup rng (fi|A)
     proof let x; assume
A8:     x in rng (fi|A);
      then consider y such that
A9:     y in dom (fi|A) & x = (fi|A).y by FUNCT_1:def 5;
      reconsider y as Ordinal by A9,ORDINAL1:23;
      reconsider B = (fi|A).y as Ordinal;
         B in sup rng (fi|A) by A8,A9,ORDINAL2:27;
      hence thesis by A9;
     end;
      A c= dom fi by A5,A6,ORDINAL1:def 2;
then A10:  A1 is_limes_of fi|A & B = psi.A1 & A1 in dom psi & phi|A = psi*(fi|A
) &
     dom (fi|A) = A & A c= A1 & {} in A
      by A1,A2,A4,A5,A6,Th10,FUNCT_1:21,22,ORDINAL3:10,RELAT_1:91,112;
then A11:  fi|A is increasing & A1 c= dom psi & lim (fi|A) = A1 & {} in A1
     by A1,Th15,ORDINAL1:def 2,ORDINAL2:def 14;
then A12:  dom (psi|A1) = A1 & sup (fi|A) = A1 & sup rng (fi|A) = sup (fi|A) &
     sup (fi|A) is_limit_ordinal & A1 <> {}
       by A5,A10,Th8,Th16,ORDINAL2:35,RELAT_1:91;
    then B is_limes_of psi|A1 & phi|A = (psi|A1)*(fi|A) by A3,A7,A10,Lm2;
   hence B is_limes_of phi|A by A11,A12,Th14;
  end;

theorem
   (for A st A in dom fi holds fi.A = C+^A) implies fi is increasing
  proof assume
A1:  for A st A in dom fi holds fi.A = C+^A;
   let A,B; assume
A2:  A in B & B in dom fi;
    then A in dom fi by ORDINAL1:19;
    then fi.A = C+^A & fi.B = C+^B by A1,A2;
   hence thesis by A2,ORDINAL2:49;
  end;

theorem Th19:
 C <> {} & (for A st A in dom fi holds fi.A = A*^C) implies fi is increasing
  proof assume that
A1:  C <> {} and
A2:  for A st A in dom fi holds fi.A = A*^C;
   let A,B; assume
A3:  A in B & B in dom fi;
    then A in dom fi by ORDINAL1:19;
    then fi.A = A*^C & fi.B = B*^C by A2,A3;
   hence thesis by A1,A3,ORDINAL2:57;
  end;

theorem
 Th20: A <> {} implies exp({},A) = {}
  proof
   defpred FF[Ordinal] means $1 <> {} implies exp({},$1) = {};
A1:  FF[{}];
A2:  FF[B] implies FF[succ B]
     proof assume FF[B] & succ B <> {};
      thus exp({},succ B) = {}*^exp({},B) by ORDINAL2:61
             .= {} by ORDINAL2:52;
     end;
A3:  for B st B <> {} & B is_limit_ordinal & for C st C in B holds FF[C]
       holds FF[B]
     proof let A such that
A4:    A <> {} & A is_limit_ordinal and
A5:    for C st C in A holds FF[C] and A <> {};
      deffunc F(Ordinal) = exp({},$1);
      consider fi such that
A6:    dom fi = A & for B st B in A holds fi.B = F(B) from OS_Lambda;
         {} is_limes_of fi
        proof per cases;
         case {} = {};
          take B = one;
             {} in A by A4,ORDINAL3:10;
          hence B in dom fi by A4,A6,ORDINAL1:41,ORDINAL2:def 4;
          let D; assume A7: B c= D;
          assume D in dom fi;
           then FF[D] & fi.D = exp({},D) by A5,A6;
          hence fi.D = {} by A7,ORDINAL1:33,ORDINAL2:def 4;
         case {} <> {}; thus thesis;
        end;
       then lim fi = {} & exp({},A) = lim fi by A4,A6,ORDINAL2:62,def 14;
      hence thesis;
     end;
      FF[B] from Ordinal_Ind(A1,A2,A3);
   hence thesis;
  end;

 Lm3: A <> {} & A is_limit_ordinal implies
  for fi st dom fi = A & for B st B in A holds fi.B = exp({},B) holds
   {} is_limes_of fi
  proof assume
A1:  A <> {} & A is_limit_ordinal;
   let fi; assume
A2:  dom fi = A & for B st B in A holds fi.B = exp({},B);
   per cases;
    case {} = {};
     take B = one;
        {} in A by A1,ORDINAL3:10;
     hence B in dom fi by A1,A2,ORDINAL1:41,ORDINAL2:def 4;
     let D; assume
      B c= D & D in dom fi;
      then D <> {} & exp({},D) = fi.D by A2,ORDINAL1:33,ORDINAL2:def 4
;
     hence fi.D = {} by Th20;
    case {} <> {}; thus thesis;
  end;

 Lm4: A <> {} & A is_limit_ordinal implies
  for fi st dom fi = A & for B st B in A holds fi.B = exp(one,B) holds
   one is_limes_of fi
  proof assume
A1:  A <> {} & A is_limit_ordinal;
   let fi; assume
A2:  dom fi = A & for B st B in A holds fi.B = exp(one,B);
   per cases;
    case one = {};
     hence thesis;
    case one <> {};
     let A1,A2 be Ordinal such that
A3:    A1 in one & one in A2;
     take B = {};
     thus B in dom fi by A1,A2,ORDINAL3:10;
     let D; assume B c= D & D in dom fi;
      then exp(one,D) = fi.D & exp(one,D) = one by A2,ORDINAL2:63;
     hence thesis by A3;
  end;

Lm5: for A st
     A <> {} & A is_limit_ordinal holds
     ex fi st dom fi = A & (for B st B in A holds fi.B = exp(C,B)) &
        ex D st D is_limes_of fi
 proof
  defpred P[Ordinal] means
    $1 <> {} & $1 is_limit_ordinal &
    for fi st dom fi = $1 & for B st B in $1 holds fi.B = exp(C,B)
     for D holds not D is_limes_of fi;
 let A such that
A1: A <> {} & A is_limit_ordinal &
    for fi st dom fi = A & for B st B in A holds fi.B = exp(C,B)
     for D holds not D is_limes_of fi;
A2: ex A st P[A] by A1;
  consider A such that
A3:P[A] and
A4:for A1 st P[A1] holds A c= A1 from Ordinal_Min(A2);
  deffunc F(Ordinal) = exp(C,$1);
  consider fi such that
A5: dom fi = A & for B st B in A holds fi.B = F(B) from OS_Lambda;
A6: now assume C = {} or C = one;
     then {} is_limes_of fi or one is_limes_of fi by A3,A5,Lm3,Lm4;
    hence contradiction by A3,A5;
   end;
   then {} in C by ORDINAL3:10;
   then one c= C by ORDINAL1:33,ORDINAL2:def 4;
   then one c< C by A6,XBOOLE_0:def 8;
then A7: one in C by ORDINAL1:21;
A8: for B2,B1 being Ordinal st B1 in B2 & B2 in A holds exp(C,B1) in exp(C,B2)
    proof defpred V[Ordinal] means
      for B1 being Ordinal st B1 in $1 & $1 in A holds exp(C,B1) in exp(C,$1);
A9:   V[{}];
A10:   V[B] implies V[succ B]
       proof assume
A11:      for B1 being Ordinal st B1 in B & B in A holds exp(C,B1) in exp(C,B);
        let B1 be Ordinal such that
A12:      B1 in succ B & succ B in A;
A13:      exp(C,B) <> {}
          proof
              now per cases;
             suppose B = {};
              hence thesis by ORDINAL2:60;
             suppose B <> {};
then A14:            {} in B by ORDINAL3:10;
                 B in succ B by ORDINAL1:10;
               then B in A by A12,ORDINAL1:19;
              hence thesis by A11,A14;
            end;
           hence thesis;
          end;
A15:     exp(C,succ B) = C*^exp(C,B) & one*^exp(C,B) = exp(C,B) & B in succ B
           by ORDINAL1:10,ORDINAL2:56,61;
then A16:      exp(C,B) in exp(C,succ B) & B in A & B1 c= B
           by A7,A12,A13,ORDINAL1:19,34,ORDINAL2:57;
           now assume B1 <> B;
           then B1 c< B by A16,XBOOLE_0:def 8;
           then B1 in B by ORDINAL1:21;
           then exp(C,B1) in exp(C,B) by A11,A16;
          hence thesis by A16,ORDINAL1:19;
         end;
        hence thesis by A7,A13,A15,ORDINAL2:57;
       end;
A17:   for B st B <> {} & B is_limit_ordinal & for D st D in B holds V[D]
         holds V[B]
       proof let B such that
A18:      B <> {} & B is_limit_ordinal and
A19:      for D st D in B holds V[D];
        let B1 be Ordinal; assume
A20:      B1 in B & B in A;
         then not A c= B by ORDINAL1:7;
        then consider psi such that
A21:      dom psi = B & (for D st D in B holds psi.D = exp(C,D)) &
          ex D st D is_limes_of psi by A4,A18;
A22:      exp(C,B) = lim psi by A18,A21,ORDINAL2:62;
           psi is increasing
          proof let B1,B2 be Ordinal; assume
A23:         B1 in B2 & B2 in dom psi;
            then V[B2] & B2 in A & B1 in B by A19,A20,A21,ORDINAL1:19;
            then exp(C,B1) in exp(C,B2) & psi.B1 = exp(C,B1) & psi.B2 = exp(C,
B2)
              by A21,A23;
           hence thesis;
          end;
then A24:      lim psi = sup psi by A18,A21,Th8;
           psi.B1 = exp(C,B1) by A20,A21;
         then exp(C,B1) in rng psi & sup psi = sup rng psi
           by A20,A21,FUNCT_1:def 5,ORDINAL2:35;
        hence thesis by A22,A24,ORDINAL2:27;
       end;
     thus for B holds V[B] from Ordinal_Ind(A9,A10,A17);
    end;
     fi is increasing
    proof let B1,B2 be Ordinal; assume
A25:   B1 in B2 & B2 in dom fi;
      then B1 in dom fi by ORDINAL1:19;
      then exp(C,B1) in exp(C,B2) & fi.B1 = exp(C,B1) & fi.B2 = exp(C,B2) by A5
,A8,A25;
     hence thesis;
    end;
   then sup fi is_limes_of fi by A3,A5,Th8;
  hence contradiction by A3,A5;
 end;

theorem
 Th21: A <> {} & A is_limit_ordinal implies
  for fi st dom fi = A & for B st B in A holds fi.B = exp(C,B) holds
   exp(C,A) is_limes_of fi
  proof assume
A1:  A <> {} & A is_limit_ordinal;
   let fi such that
A2:  dom fi = A & for B st B in A holds fi.B = exp(C,B);
   consider psi such that
A3:  dom psi = A & for B st B in A holds psi.B = exp(C,B) and
A4:  ex D st D is_limes_of psi by A1,Lm5;
      now let x; assume
A5:    x in A;
     then reconsider B = x as Ordinal by ORDINAL1:23;
     thus fi.x = exp(C,B) by A2,A5 .= psi.x by A3,A5;
    end;
    then fi = psi by A2,A3,FUNCT_1:9;
   then consider D such that
A6:  D is_limes_of fi by A4;
      D = lim fi by A6,ORDINAL2:def 14 .= exp(C,A) by A1,A2,ORDINAL2:62;
   hence thesis by A6;
  end;

theorem
 Th22: C <> {} implies exp(C,A) <> {}
  proof
    defpred P[Ordinal] means exp(C,$1) <> {};
    assume
A1:  C <> {};
A2:  P[{}] by ORDINAL2:60;
A3:  for A st P[A] holds P[succ A]
     proof let A such that
A4:    exp(C,A) <> {};
      exp(C,succ A) = C*^exp(C,A) by ORDINAL2:61;
      hence thesis by A1,A4,ORDINAL3:34;
     end;
A5:  for A st A <> {} & A is_limit_ordinal &
      for B st B in A holds P[B] holds P[A]
     proof let A such that
A6:    A <> {} & A is_limit_ordinal and
A7:    for B st B in A holds exp(C,B) <> {};
      consider fi such that
A8:    dom fi = A & (for B st B in A holds fi.B = exp(C,B)) &
        ex D st D is_limes_of fi by A6,Lm5;
A9:    exp(C,A) = lim fi by A6,A8,ORDINAL2:62;
      consider D such that
A10:    D is_limes_of fi by A8;
A11:    lim fi = D by A10,ORDINAL2:def 14;
      assume exp(C,A) = {};
      then consider B such that
A12:    B in dom fi & for D st B c= D & D in dom fi holds fi.D = {}
        by A9,A10,A11,ORDINAL2:def 13;
         fi.B = exp(C,B) & exp(C,B) <> {} & fi.B = {} by A7,A8,A12;
      hence contradiction;
     end;
     for A holds P[A] from Ordinal_Ind(A2,A3,A5);
   hence thesis;
  end;

theorem
 Th23: one in C implies exp(C,A) in exp(C,succ A)
  proof assume
A1:  one in C;
    then exp(C,A) <> {} & one*^exp(C,A) = exp(C,A) by Th22,ORDINAL2:56;
    then exp(C,succ A) = C*^exp(C,A) & exp(C,A) in C*^exp(C,A)
     by A1,ORDINAL2:57,61;
   hence thesis;
  end;

theorem
 Th24: one in C & A in B implies exp(C,A) in exp(C,B)
  proof assume
A1:  one in C;
   defpred OO[Ordinal] means for A st A in $1 holds exp(C,A) in exp(C,$1);
A2:  OO[{}];
A3:  for B st OO[B] holds OO[succ B]
     proof let B such that
A4:    for A st A in B holds exp(C,A) in exp(C,B);
      let A; assume A in succ B;
then A5:    A c= B by ORDINAL1:34;
A6:    exp(C,B) in exp(C,succ B) by A1,Th23;
         now assume A <> B;
         then A c< B by A5,XBOOLE_0:def 8;
         then A in B by ORDINAL1:21;
        hence exp(C,A) in exp(C,B) by A4;
       end;
      hence thesis by A6,ORDINAL1:19;
     end;
A7:  for B st B <> {} & B is_limit_ordinal & for D st D in B holds OO[D]
       holds OO[B]
     proof let B such that
A8:    B <> {} & B is_limit_ordinal and
A9:    for D st D in B holds OO[D];
      let A such that
A10:    A in B;
      deffunc F(Ordinal) = exp(C,$1);
      consider fi such that
A11:    dom fi = B & (for D st D in B holds fi.D = F(D)) from OS_Lambda;
A12:    exp(C,B) = lim fi by A8,A11,ORDINAL2:62;
         fi is increasing
        proof let B1,B2 be Ordinal; assume
A13:       B1 in B2 & B2 in dom fi;
          then B1 in dom fi & OO[B2] by A9,A11,ORDINAL1:19;
          then fi.B1 = exp(C,B1) & fi.B2 = exp(C,B2) & exp(C,B1) in exp(C,B2)
            by A11,A13;
         hence thesis;
        end;
then A14:    sup fi = lim fi by A8,A11,Th8;
         fi.A = exp(C,A) by A10,A11;
       then exp(C,A) in rng fi & sup fi = sup rng fi by A10,A11,FUNCT_1:def 5,
ORDINAL2:35;
      hence thesis by A12,A14,ORDINAL2:27;
     end;
      for B holds OO[B] from Ordinal_Ind(A2,A3,A7);
   hence thesis;
  end;

theorem Th25:
 one in C & (for A st A in dom fi holds fi.A = exp(C,A)) implies
   fi is increasing
  proof assume
A1:  one in C & (for A st A in dom fi holds fi.A = exp(C,A));
   let A,B; assume
A2:  A in B & B in dom fi;
    then A in dom fi by ORDINAL1:19;
    then fi.A = exp(C,A) & fi.B = exp(C,B) by A1,A2;
   hence fi.A in fi.B by A1,A2,Th24;
  end;

theorem
    one in C & A <> {} & A is_limit_ordinal implies
  for fi st dom fi = A & for B st B in A holds fi.B = exp(C,B) holds
   exp(C,A) = sup fi
  proof assume
A1:  one in C & A <> {} & A is_limit_ordinal;
   let fi; assume
A2:  dom fi = A & for B st B in A holds fi.B = exp(C,B);
    then fi is increasing by A1,Th25;
    then lim fi = sup fi by A1,A2,Th8;
   hence thesis by A1,A2,ORDINAL2:62;
  end;

theorem
    C <> {} & A c= B implies exp(C,A) c= exp(C,B)
  proof assume C <> {};
    then {} in C by ORDINAL3:10;
then A1:  one c= C by ORDINAL1:33,ORDINAL2:def 4;
A2: A c< B iff A c= B & A <> B by XBOOLE_0:def 8;
   assume A c= B;
then A3:  A in B or A = B by A2,ORDINAL1:21;
      now per cases;
     suppose C = one;
       then exp(C,A) = one & exp(C,B) = one by ORDINAL2:63;
      hence thesis;
     suppose C <> one;
       then one c< C by A1,XBOOLE_0:def 8;
       then one in C by ORDINAL1:21;
       then exp(C,A) in exp(C,B) or exp(C,A) = exp(C,B) by A3,Th24;
      hence thesis by ORDINAL1:def 2;
    end;
   hence thesis;
  end;

theorem
   A c= B implies exp(A,C) c= exp(B,C)
  proof assume
A1:  A c= B;
     defpred P[Ordinal] means exp(A,$1) c= exp(B,$1);
      exp(A,{}) = one & exp(B,{}) = one by ORDINAL2:60;
then A2:  P[{}];
A3:  for C st P[C] holds P[succ C]
     proof let C;
         exp(A,succ C) = A*^exp(A,C) & exp(B,succ C) = B*^exp(B,C)
        by ORDINAL2:61;
      hence thesis by A1,ORDINAL3:23;
     end;
A4:  for C st C <> {} & C is_limit_ordinal &
      for D st D in C holds P[D] holds P[C]
     proof let C; assume that
A5:    C <> {} & C is_limit_ordinal and
A6:    for D st D in C holds exp(A,D) c= exp(B,D);
      deffunc F(Ordinal) = exp(A,$1);
      consider f1 such that
A7:    dom f1 = C & for D st D in C holds f1.D = F(D) from OS_Lambda;
      deffunc F(Ordinal) = exp(B,$1);
      consider f2 such that
A8:    dom f2 = C & for D st D in C holds f2.D = F(D) from OS_Lambda;
A9:    exp(A,C) is_limes_of f1 & exp(B,C) is_limes_of f2 by A5,A7,A8,Th21;
         now let D; assume D in dom f1;
         then f1.D = exp(A,D) & f2.D = exp(B,D) & exp(A,D) c= exp(B,D) by A6,A7
,A8;
        hence f1.D c= f2.D;
       end;
      hence exp(A,C) c= exp(B,C) by A7,A8,A9,Th6;
     end;
      for C holds P[C] from Ordinal_Ind(A2,A3,A4);
   hence thesis;
  end;

theorem
    one in C & A <> {} implies one in exp(C,A)
  proof assume
A1:  one in C & A <> {};
    then {} in A & exp(C,{}) = one by ORDINAL2:60,ORDINAL3:10;
   hence thesis by A1,Th24;
  end;

theorem
 Th30: exp(C,A+^B) = exp(C,B)*^exp(C,A)
  proof
     defpred P[Ordinal] means exp(C,A+^$1) = exp(C,$1)*^exp(C,A);
      exp(C,A) = one*^exp(C,A) & one = exp(C,{})
      by ORDINAL2:56,60;
then A1:  P[{}] by ORDINAL2:44;
A2:  for B st P[B] holds P[succ B]
     proof let B such that
A3:    exp(C,A+^B) = exp(C,B)*^exp(C,A);
      thus exp(C,A+^succ B) = exp(C,succ(A+^B)) by ORDINAL2:45
               .= C*^exp(C,A+^B) by ORDINAL2:61
               .= C*^exp(C,B)*^exp(C,A) by A3,ORDINAL3:58
               .= exp(C,succ B)*^exp(C,A) by ORDINAL2:61;
     end;
A4:  for B st B <> {} & B is_limit_ordinal &
     for D st D in B holds P[D] holds P[B]
     proof let B such that
A5:    B <> {} & B is_limit_ordinal and
A6:    for D st D in B holds exp(C,A+^D) = exp(C,D)*^exp(C,A);
      deffunc F(Ordinal) = exp(C,$1);
      consider fi such that
A7:    dom fi = B & for D st D in B holds fi.D = F(D) from OS_Lambda;
      consider psi such that
A8:    dom psi = A+^B & for D st D in A+^B holds psi.D = F(D)
      from OS_Lambda;
         A+^B <> {} & A+^B is_limit_ordinal by A5,ORDINAL3:29,32;
then A9:    lim psi = exp(C,A+^B) by A8,ORDINAL2:62;
      deffunc F(Ordinal) = exp(C,$1);
      consider f1 such that
A10:    dom f1 = A & for D st D in A holds f1.D = F(D) from OS_Lambda;
A11:    dom psi = (dom f1)+^(dom(fi*^exp(C,A))) by A7,A8,A10,ORDINAL3:def 5;
A12:    now let D such that
A13:      D in dom f1;
           A c= A+^B by ORDINAL3:27; hence psi.D = exp(C,D) by A8,A10,A13
 .= f1.D by A10,A13;
       end;
A14:    exp(C,B) is_limes_of fi by A5,A7,Th21;
         now let D; assume
           D in dom(fi*^exp(C,A));
then A15:      D in dom fi by ORDINAL3:def 5;
         then A+^D in A+^B by A7,ORDINAL2:49;
        hence psi.((dom f1)+^D) = exp(C,A+^D) by A8,A10
                .= (exp(C,D))*^exp(C,A) by A6,A7,A15
                .= (fi.D)*^exp(C,A) by A7,A15
                .= (fi*^exp(C,A)).D by A15,ORDINAL3:def 5;
       end;
       then psi = f1^(fi*^exp(C,A)) & exp(C,B)*^exp(C,A) is_limes_of fi*^exp(C
,A)
        by A11,A12,A14,Def1,Th5;
       then exp(C,B)*^exp(C,A) is_limes_of psi by Th3;
      hence thesis by A9,ORDINAL2:def 14;
     end;
      for B holds P[B] from Ordinal_Ind(A1,A2,A4);
   hence thesis;
  end;

theorem
   exp(exp(C,A),B) = exp(C,B*^A)
  proof
     defpred P[Ordinal] means exp(exp(C,A),$1) = exp(C,$1*^A);
      exp(exp(C,A),{}) = one & exp(C,{}) = one by ORDINAL2:60;
then A1:  P[{}] by ORDINAL2:52;
A2:  for B st P[B] holds P[succ B]
     proof let B; assume exp(exp(C,A),B) = exp(C,B*^A);
      hence exp(exp(C,A),succ B) = exp(C,A)*^exp(C,B*^A) by ORDINAL2:61
             .= exp(C,B*^A+^A) by Th30 .= exp(C,(succ B)*^A) by ORDINAL2:53;
     end;
A3:  for B st B <> {} & B is_limit_ordinal &
     for D st D in B holds P[D] holds P[B]
     proof let B; assume that
A4:    B <> {} & B is_limit_ordinal and
A5:    for D st D in B holds exp(exp(C,A),D) = exp(C,D*^A);
      deffunc F(Ordinal) = exp(exp(C,A),$1);
      consider fi such that
A6:    dom fi = B & for D st D in
 B holds fi.D = F(D) from OS_Lambda;
      deffunc F(Ordinal) = $1*^A;
      consider f1 such that
A7:    dom f1 = B & for D st D in B holds f1.D = F(D) from OS_Lambda;
      deffunc F(Ordinal) = exp(C,$1);
      consider f2 such that
A8:    dom f2 = B*^A & for D st D in B*^A holds f2.D = F(D) from OS_Lambda;
A9:       exp(C,{}) = one & B*^{} = {} by ORDINAL2:55,60;
         now assume
A10:      A <> {};
A11:       dom(f2*f1) = B
          proof
           thus dom(f2*f1) c= B by A7,RELAT_1:44;
           let x; assume
A12:         x in B;
           then reconsider E = x as Ordinal by ORDINAL1:23;
              E*^A in B*^A & f1.E = E*^A by A7,A10,A12,ORDINAL2:57;
           hence thesis by A7,A8,A12,FUNCT_1:21;
          end;
           now let x; assume
A13:        x in B;
          then reconsider D = x as Ordinal by ORDINAL1:23;
A14:        D*^A in B*^A & f1.D = D*^A by A7,A10,A13,ORDINAL2:57;
          thus fi.x = exp(exp(C,A),D) by A6,A13 .= exp(C,D*^A) by A5,A13
                 .= f2.(f1.D) by A8,A14
                 .= (f2*f1).x by A7,A13,FUNCT_1:23;
         end;
then A15:       fi = f2*f1 by A6,A11,FUNCT_1:9;
           B*^A <> {} & B*^A is_limit_ordinal
          by A4,A10,ORDINAL3:34,48;
then A16:       exp(C,B*^A) is_limes_of f2 by A8,Th21;
A17:      rng f1 c= dom f2
          proof let x; assume x in rng f1;
           then consider y such that
A18:         y in dom f1 & x = f1.y by FUNCT_1:def 5;
           reconsider y as Ordinal by A18,ORDINAL1:23;
              x = y*^A & y*^A in B*^A by A7,A10,A18,ORDINAL2:57;
           hence thesis by A8;
          end;
A19:       sup rng f1 = dom f2
          proof
              sup rng f1 c= sup dom f2 by A17,ORDINAL2:30;
           hence sup rng f1 c= dom f2 by ORDINAL2:26;
           let x; assume
A20:         x in dom f2;
           then reconsider D = x as Ordinal by ORDINAL1:23;
           consider A1 such that
A21:         A1 in B & D in A1*^A by A4,A8,A20,ORDINAL3:49;
              f1.A1 = A1*^A by A7,A21;
            then A1*^A in rng f1 by A7,A21,FUNCT_1:def 5;
            then A1*^A in sup rng f1 by ORDINAL2:27;
           hence thesis by A21,ORDINAL1:19;
          end;
           f1 is increasing by A7,A10,Th19;
         then exp(C,B*^A) is_limes_of fi by A15,A16,A19,Th14;
         then exp(C,B*^A) = lim fi by ORDINAL2:def 14;
        hence thesis by A4,A6,ORDINAL2:62;
       end;
      hence exp(exp(C,A),B) = exp(C,B*^A) by A9,ORDINAL2:63;
     end;
      for B holds P[B] from Ordinal_Ind(A1,A2,A3);
   hence thesis;
  end;

theorem
   one in C implies A c= exp(C,A)
  proof assume
A1:  one in C;
     defpred P[Ordinal] means $1 c= exp(C,$1);
A2:  P[{}] by XBOOLE_1:2;
A3:  P[B] implies P[succ B]
     proof assume
A4:    B c= exp(C,B);
         exp(C,B) <> {} & exp(C,succ B) = C*^exp(C,B) &
       exp(C,B) = one*^exp(C,B)
        by A1,Th22,ORDINAL2:56,61;
       then exp(C,B) in exp(C,succ B) by A1,ORDINAL2:57;
       then B in exp(C,succ B) by A4,ORDINAL1:22;
      hence thesis by ORDINAL1:33;
     end;
A5:  for A st A <> {} & A is_limit_ordinal &
      for B st B in A holds P[B] holds P[A]
     proof let A such that
A6:    A <> {} & A is_limit_ordinal and
A7:    for B st B in A holds B c= exp(C,B);
      deffunc F(Ordinal) = exp(C,$1);
      consider fi such that
A8:    dom fi = A & for B st B in A holds fi.B = F(B) from OS_Lambda;
         fi is increasing by A1,A8,Th25;
then A9:    sup fi = lim fi by A6,A8,Th8 .= exp(C,A) by A6,A8,ORDINAL2:62;
      let x; assume
A10:    x in A;
      then reconsider B = x as Ordinal by ORDINAL1:23;
         fi.B = exp(C,B) by A8,A10;
       then exp(C,B) in rng fi & sup fi = sup rng fi
        by A8,A10,FUNCT_1:def 5,ORDINAL2:35;
       then B c= exp(C,B) & exp(C,B) in sup fi by A7,A10,ORDINAL2:27;
      hence x in exp(C,A) by A9,ORDINAL1:22;
     end;
      P[B] from Ordinal_Ind(A2,A3,A5);
   hence thesis;
  end;

scheme CriticalNumber { phi(Ordinal) -> Ordinal } :
 ex A st phi(A) = A
  provided
A1: for A,B st A in B holds phi(A) in phi(B) and
A2: for A st A <> {} & A is_limit_ordinal
    for phi st dom fi = A & for B st B in A holds phi.B = phi(B) holds
     phi(A) is_limes_of phi
  proof assume
A3:  not thesis;
   deffunc F(Ordinal,Ordinal) = phi($2);
   deffunc G(Ordinal,T-Sequence) = {};
   consider phi such that
   A4: dom phi = omega and
A5: {} in omega implies phi.{} = phi({}) and
A6: for A st succ A in omega holds phi.(succ A) = F(A,phi.A) and
    for A st A in omega & A <> {} & A is_limit_ordinal
          holds phi.A = G(A,phi|A) from OS_Exist;
A7: now
     defpred P[Ordinal] means not $1 c= phi($1);
     assume
A8:    ex A st P[A];
     consider A such that
A9:    P[A] and
A10:    for B st P[B] holds A c= B from Ordinal_Min(A8);
      phi(A) in A by A9,ORDINAL1:26;
      then phi(phi(A)) in phi(A) by A1;
      then not phi(A) c= phi(phi(A)) by ORDINAL1:7;
     hence contradiction by A9,A10;
    end;
A11:  now let A; A c= phi(A) & A <> phi(A) by A3,A7;
     then A c< phi(A) by XBOOLE_0:def 8;
     hence A in phi(A) by ORDINAL1:21;
    end;
A12:  phi is increasing
     proof let A,B; assume
A13:    A in B & B in dom phi;
 then A14:      ex C st B = A+^C & C <> {} by ORDINAL3:31;
        defpred R[Ordinal] means
          A+^$1 in omega & $1 <> {} implies phi.A in phi.(A+^$1);
A15:    R[{}];
A16:    for C st R[C] holds R[succ C]
        proof let C such that
A17:       A+^C in omega & C <> {} implies phi.A in phi.(A+^C) and
A18:       A+^succ C in omega & succ C <> {};
A19:       A+^C in succ(A+^C) & A+^succ C = succ(A+^C)
           by ORDINAL1:10,ORDINAL2:45;
         reconsider D = phi.(A+^C) as Ordinal;
        phi.(A+^succ C) = phi(D) & D in phi(D) & A+^{} = A
           by A6,A11,A18,A19,ORDINAL2:44;
          hence thesis by A17,A18,A19,ORDINAL1:19;
        end;
A20:    for B st B <> {} & B is_limit_ordinal &
        for C st C in B holds R[C] holds R[B]
        proof let B such that
A21:       B <> {} & B is_limit_ordinal and
            for C st C in B holds A+^C in omega & C <> {} implies
           phi.A in phi.(A+^C) and
A22:       A+^B in omega & B <> {};
            A+^B <> {} by A22,ORDINAL3:29;
          then A+^B is_limit_ordinal & {} in A+^B by A21,ORDINAL3:10,32;
          then omega c= A+^B by ORDINAL2:def 5;
         hence thesis by A22,ORDINAL1:7;
        end;
         for C holds R[C] from Ordinal_Ind(A15,A16,A20);
      hence thesis by A4,A13,A14;
     end;
   deffunc F(Ordinal) = phi ($1);
   consider fi such that
A23:  dom fi = sup phi & for A st A in sup phi holds fi.A = F(A)
     from OS_Lambda;
      phi({}) in rng phi & sup rng phi = sup phi
     by A4,A5,FUNCT_1:def 5,ORDINAL2:19,35;
then A24: sup phi <> {} & sup phi is_limit_ordinal
     by A4,A12,Th16,ORDINAL2:19,27;
then A25:  phi(sup phi) is_limes_of fi by A2,A23;
      fi is increasing
     proof let A,B; assume
A26:    A in B & B in dom fi;
       then A in dom fi by ORDINAL1:19;
       then fi.A = phi(A) & fi.B = phi(B) by A23,A26;
      hence thesis by A1,A26;
     end;
then A27:  sup fi = lim fi by A23,A24,Th8 .= phi(sup phi) by A25,ORDINAL2:def
14;
      sup fi c= sup phi
     proof let x; assume
A28:    x in sup fi;
      then reconsider A = x as Ordinal by ORDINAL1:23;
A29:    sup fi = sup rng fi & sup phi = sup rng phi by ORDINAL2:35;
      then consider B such that
A30:    B in rng fi & A c= B by A28,ORDINAL2:29;
      consider y such that
A31:    y in dom fi & B = fi.y by A30,FUNCT_1:def 5;
      reconsider y as Ordinal by A31,ORDINAL1:23;
      consider C such that
A32:    C in rng phi & y c= C by A23,A29,A31,ORDINAL2:29;
      consider z such that
A33:    z in dom phi & C = phi.z by A32,FUNCT_1:def 5;
      reconsider z as Ordinal by A33,ORDINAL1:23;
         succ z in omega by A4,A33,ORDINAL1:41,ORDINAL2:19;
then A34:    phi.succ z = phi(C) & phi.succ z in rng phi & B = phi(y)
        by A4,A6,A23,A31,A33,FUNCT_1:def 5;
         y c< C iff y <> C & y c= C by XBOOLE_0:def 8;
       then y in C or y = C by A32,ORDINAL1:21;
       then phi(y) in phi(C) or y = C by A1;
       then B c= phi(C) & phi(C) in sup phi
        by A29,A34,ORDINAL1:def 2,ORDINAL2:27;
       then B in sup phi by ORDINAL1:22;
      hence thesis by A30,ORDINAL1:22;
     end;
    then not sup phi in phi(sup phi) by A27,ORDINAL1:7;
   hence contradiction by A11;
  end;

 reserve W for Universe;

 definition let W;
  mode Ordinal of W -> Ordinal means:
Def2:   it in W;
   existence
    proof On W <> {} by CLASSES2:55;
      then {} in On W & On W c= W by ORDINAL2:9,ORDINAL3:10; hence thesis;
    end;
  mode Ordinal-Sequence of W -> Ordinal-Sequence means:
Def3:   dom it = On W & rng it c= On W;
   existence
    proof
     deffunc F(Ordinal) = {};
     consider phi such that
A1:    dom phi = On W & for A st A in On W holds phi.A = F(A) from OS_Lambda;
     take phi; thus dom phi = On W by A1;
     let x; assume x in rng phi;
     then consider y such that
A2:    y in dom phi & x = phi.y by FUNCT_1:def 5;
     reconsider y as Ordinal by A2,ORDINAL1:23;
        phi.y = {} & On W <> {} by A1,A2;
     hence x in On W by A2,ORDINAL3:10;
    end;
 end;

definition let W;
 cluster non empty Ordinal of W;
  existence
 proof On W <> {} by CLASSES2:55;
  then {} in On W & On W c= W by ORDINAL2:9,ORDINAL3:10;
  then one in W by CLASSES2:6,ORDINAL2:def 4;
  then one is non empty & one is Ordinal of W by Def2;
  hence thesis;
 end;
end;

 reserve A1,B1 for Ordinal of W,
         phi for Ordinal-Sequence of W;

scheme UOS_Lambda { W() -> Universe, F(set) -> Ordinal of W() } :
 ex phi being Ordinal-Sequence of W() st
   for a being Ordinal of W() holds phi.a = F(a)
  proof
    deffunc FF(Ordinal) = F($1);
    consider psi such that
A1:dom psi = On W() & for A st A in On W() holds psi.A = FF(A) from OS_Lambda;
      rng psi c= On W()
     proof let x; assume x in rng psi;
      then consider y such that
A2:     y in dom psi & x = psi.y by FUNCT_1:def 5;
      reconsider y as Ordinal by A2,ORDINAL1:23;
         x = F(y) & F(y) in W() by A1,A2,Def2;
      hence thesis by ORDINAL2:def 2;
     end;
   then reconsider phi = psi as Ordinal-Sequence of W() by A1,Def3;
   take phi; let a be Ordinal of W(); a in W() by Def2;
    then a in On W() by ORDINAL2:def 2;
   hence thesis by A1;
  end;

 definition let W;
  func 0-element_of W -> Ordinal of W equals:
Def4:   {};
   correctness
    proof On W <> {} by CLASSES2:55;
      then {} in On W & On W c= W by ORDINAL2:9,ORDINAL3:10;
     then reconsider A = {} as Ordinal of W by Def2;
        A = {};
     hence thesis;
    end;
  func 1-element_of W -> non empty Ordinal of W equals:
Def5:    one;
   correctness
    proof On W <> {} by CLASSES2:55;
      then {} in On W & On W c= W by ORDINAL2:9,ORDINAL3:10;
      then one in W by CLASSES2:6,ORDINAL2:def 4;
     then reconsider A = one as Ordinal of W by Def2;
        A = one;
     hence thesis;
    end;
  let phi,A1;
  redefine func phi.A1 -> Ordinal of W;
    coherence
     proof A1 in W by Def2;
then A1:     A1 in On W & dom phi = On W by Def3,ORDINAL2:def 2;
      reconsider B = phi.A1 as Ordinal;
         B in rng phi & rng phi c= On W by A1,Def3,FUNCT_1:def 5;
       then B in On W & On W c= W by ORDINAL2:9; hence thesis by Def2;
     end;
 end;

 definition let W; let p2,p1 be Ordinal-Sequence of W;
  redefine func p1*p2 -> Ordinal-Sequence of W;
    coherence
     proof
         dom p1 = On W & dom p2 = On W & rng p2 c= On W by Def3;
then A1:     dom(p1*p2) = On W & rng(p1*p2) c= rng p1 & rng p1 c= On W
        by Def3,RELAT_1:45,46;
      then reconsider f = p1*p2 as T-Sequence by ORDINAL1:def 7;
A2:     rng f c= On W by A1,XBOOLE_1:1;
      then reconsider f as Ordinal-Sequence by ORDINAL2:def 8;
         f is Ordinal-Sequence of W by A1,A2,Def3;
      hence thesis;
     end;
 end;

canceled 2;

theorem
   0-element_of W = {} & 1-element_of W = one by Def4,Def5;

 definition let W,A1;
  redefine func succ A1 -> non empty Ordinal of W;
    coherence
     proof A1 in W & W is_Tarski-Class by Def2;
       then succ A1 in W by CLASSES2:6;
      hence thesis by Def2;
     end;
   let B1;
   func A1 +^ B1 -> Ordinal of W;
    coherence
     proof
        defpred P[Ordinal] means $1 in W implies A1+^$1 in W;
A1:     for B st for C st C in B holds P[C] holds P[B]
        proof let B such that
A2:       for C st C in B holds C in W implies A1+^C in W and
A3:       B in W;
            0-element_of W in W & 1-element_of W in W by Def2;
then A4:       {0-element_of W} in W & {1-element_of W} in W & A1 in W
            by Def2,CLASSES2:63;
          then [:A1,{0-element_of W}:] in W & [:B,{1-element_of W}:] in W
            by A3,CLASSES2:67;
       then [:A1,{0-element_of W}:] \/ [:B,{1-element_of W}:] in W & {} <>
succ {} &
           W is_Tarski-Class & 0-element_of W = {} & 1-element_of W = one
            by Def4,Def5,CLASSES2:66;
then A5:   Card(A1+^B) = Card([:A1,{0-element_of W}:] \/ [:B,{1-element_of W}:]
) &
           Card([:A1,{0-element_of W}:] \/ [:B,{1-element_of W}:]) <` Card W
            by CARD_2:16,CLASSES2:1;
            A1+^B c= W
           proof let x; assume
A6:          x in A1+^B;
            then reconsider A = x as Ordinal by ORDINAL1:23;
A7:           A1 c= W & (A in A1 or A1 c= A) by A4,ORDINAL1:26,def 2;
               now assume A1 c= A;
              then consider C such that
A8:            A = A1+^C by ORDINAL3:30;
              C in B & B c= W by A3,A6,A8,ORDINAL1:def 2,ORDINAL3:25;
              hence x in W by A2,A8;
             end;
            hence thesis by A7;
           end;
         hence A1+^B in W by A5,CLASSES1:2;
        end;
A9:     for B holds P[B] from Transfinite_Ind(A1);
         B1 in W by Def2;
       then A1+^B1 in W by A9;
      hence thesis by Def2;
     end;
 end;

 definition let W,A1,B1;
  redefine func A1 *^ B1 -> Ordinal of W;
    coherence
     proof
        defpred P[Ordinal] means $1 in W implies $1*^B1 in W;
A1:     for A st for C st C in A holds P[C] holds P[A]
        proof let A such that
A2:       for C st C in A holds C in W implies C*^B1 in W and
A3:       A in W;
A4:       B1 in W & W is_Tarski-Class by Def2;
          then [:A,B1:] in W by A3,CLASSES2:67;
then A5:       Card(A*^B1) = Card [:A,B1:] & Card [:A,B1:] <` Card W
            by CARD_2:18,CLASSES2:1;
            A*^B1 c= W
           proof let x; assume
A6:          x in A*^B1;
            then reconsider B = x as Ordinal by ORDINAL1:23;
               B1 <> {} by A6,ORDINAL2:55;
            then consider C,D such that
A7:          B = C*^B1+^D & D in B1 by ORDINAL3:55;
A8:          B1 c= W & C*^B1 c= B by A4,A7,ORDINAL1:def 2,ORDINAL3:27;
             then C*^B1 in A*^B1 by A6,ORDINAL1:22;
          then C in A & A c= W by A3,ORDINAL1:def 2,ORDINAL3:37;
             then D in W & C*^B1 in W by A2,A7,A8;
            then reconsider CB = C*^B1, D as Ordinal of W by Def2;
               x = CB+^D by A7;
            hence thesis by Def2;
           end;
         hence A*^B1 in W by A5,CLASSES1:2;
        end;
A9:     for A holds P[A] from Transfinite_Ind(A1);
         A1 in W by Def2;
       then A1*^B1 in W by A9;
      hence thesis by Def2;
     end;
 end;

theorem
 Th36: A1 in dom phi
  proof A1 in W & dom phi = On W by Def2,Def3;
   hence thesis by ORDINAL2:def 2;
  end;

theorem
 Th37: dom fi in W & rng fi c= W implies sup fi in W
  proof assume
A1:  dom fi in W & rng fi c= W;
    rng fi = fi.:(dom fi) & W is_Tarski-Class by RELAT_1:146;
    then Card rng fi <=` Card dom fi & Card dom fi <` Card W
     by A1,CARD_2:3,CLASSES2:1;
    then Card rng fi <` Card W by ORDINAL1:22;
    then rng fi in W by A1,CLASSES1:2;
then A2:  union rng fi in W by CLASSES2:65;
   consider A such that
A3:  rng fi c= A by ORDINAL2:def 8;
      for x st x in rng fi holds x is Ordinal by A3,ORDINAL1:23;
   then reconsider B = union rng fi as Ordinal by ORDINAL1:35;
A4:  succ B in W by A2,CLASSES2:6;
      sup fi c= succ B
     proof let x; assume
A5:     x in sup fi;
      then reconsider A = x as Ordinal by ORDINAL1:23;
         sup fi = sup rng fi by ORDINAL2:35;
      then consider C such that
A6:     C in rng fi & A c= C by A5,ORDINAL2:29;
         C c= union rng fi by A6,ZFMISC_1:92;
       then A c= B by A6,XBOOLE_1:1;
      hence x in succ B by ORDINAL1:34;
     end;
   hence thesis by A4,CLASSES1:def 1;
  end;

 reserve L,L1 for T-Sequence;

theorem
   phi is increasing & phi is continuous & omega in W implies
   ex A st A in dom phi & phi.A = A
  proof assume that
A1:  phi is increasing and
A2:  phi is continuous and
A3: omega in W;
   assume
A4:  not thesis;
   reconsider N = phi.(0-element_of W) as Ordinal;
   deffunc C(Ordinal,Ordinal) = phi.$2;
   deffunc D(Ordinal,Ordinal) = {};
   consider L such that
A5: dom L = omega and
A6: {} in omega implies L.{} = N and
A7: for A st succ A in omega holds L.(succ A) = C(A,L.A) and
    for A st A in omega & A <> {} & A is_limit_ordinal
          holds L.A = D(A,L|A) from TS_Exist1;
    defpred P[Ordinal] means $1 in dom L implies L.$1 is Ordinal of W;
A8: P[{}] by A5,A6;
A9: for A st P[A] holds P[succ A]
     proof let A such that
A10:    A in dom L implies L.A is Ordinal of W and
A11:    succ A in dom L;
         A in succ A by ORDINAL1:10;
      then reconsider x = L.A as Ordinal of W by A10,A11,ORDINAL1:19;
         L.succ A = phi.x by A5,A7,A11;
      hence thesis;
     end;
A12: for A st A <> {} & A is_limit_ordinal &
     for B st B in A holds P[B] holds P[A]
     proof let A such that
A13:    A <> {} & A is_limit_ordinal and
         for B st B in A holds B in dom L implies L.B is Ordinal of W and
A14:    A in dom L;
         {} in A by A13,ORDINAL3:10;
       then omega c= A by A13,ORDINAL2:def 5;
      hence thesis by A5,A14,ORDINAL1:7;
     end;
A15:  for A holds P[A] from Ordinal_Ind(A8,A9,A12);
      rng L c= sup rng L
     proof let x; assume
A16:    x in rng L;
      then consider y such that
A17:    y in dom L & x = L.y by FUNCT_1:def 5;
      reconsider y as Ordinal by A17,ORDINAL1:23;
      reconsider A = L.y as Ordinal of W by A15,A17;
         A in sup rng L by A16,A17,ORDINAL2:27;
      hence thesis by A17;
     end;
   then reconsider L as Ordinal-Sequence by ORDINAL2:def 8;
A18:  now let A1; A1 in dom phi by Th36;
      then A1 c= phi.A1 & A1 <> phi.A1 by A1,A4,Th10;
      then A1 c< phi.A1 by XBOOLE_0:def 8;
     hence A1 in phi.A1 by ORDINAL1:21;
    end;
A19:  L is increasing
     proof let A,B; assume
A20:    A in B & B in dom L;
 then A21:      ex C st B = A+^C & C <> {} by ORDINAL3:31;
        defpred P[Ordinal] means
          A+^$1 in omega & $1 <> {} implies L.A in L.(A+^$1);
A22:    P[{}];
A23:    for C st P[C] holds P[succ C]
        proof let C such that
A24:       A+^C in omega & C <> {} implies L.A in L.(A+^C) and
A25:       A+^succ C in omega & succ C <> {};
A26:       A+^C in succ(A+^C) & A+^succ C = succ(A+^C)
           by ORDINAL1:10,ORDINAL2:45;
       then A+^C in omega & A in omega by A5,A20,A25,ORDINAL1:19;
         then reconsider D = L.(A+^C) as Ordinal of W by A5,A15;
        L.(A+^succ C) = phi.D & D in phi.D & A+^{} = A
           by A7,A18,A25,A26,ORDINAL2:44;
          hence thesis by A24,A25,A26,ORDINAL1:19;
        end;
A27:    for B st B <> {} & B is_limit_ordinal &
        for C st C in B holds P[C] holds P[B]
        proof let B such that
A28:       B <> {} & B is_limit_ordinal and
            for C st C in B holds A+^C in omega & C <> {} implies
           L.A in L.(A+^C) and
A29:       A+^B in omega & B <> {};
            A+^B <> {} by A29,ORDINAL3:29;
          then A+^B is_limit_ordinal & {} in A+^B by A28,ORDINAL3:10,32;
          then omega c= A+^B by ORDINAL2:def 5;
         hence thesis by A29,ORDINAL1:7;
        end;
       for C holds P[C] from Ordinal_Ind(A22,A23,A27);
      hence thesis by A5,A20,A21;
     end;
   set fi = phi|sup L;
   N in rng L & sup rng L = sup L
     by A5,A6,FUNCT_1:def 5,ORDINAL2:19,35;
then A30: sup L <> {} & sup L is_limit_ordinal
     by A5,A19,Th16,ORDINAL2:19,27;
A31: rng L c= W
     proof let x; assume x in rng L;
      then consider y such that
A32:    y in dom L & x = L.y by FUNCT_1:def 5;
      reconsider y as Ordinal by A32,ORDINAL1:23;
         L.y is Ordinal of W by A15,A32;
      hence thesis by A32,Def2;
     end;
then A33: sup L in W by A3,A5,Th37;
   then reconsider S = sup L as Ordinal of W by Def2;
A34: S in On W & dom phi = On W by A33,Def3,ORDINAL2:def 2;
then A35: phi.S is_limes_of fi by A2,A30,ORDINAL2:def 17;
      S c= dom phi by A34,ORDINAL1:def 2;
then A36:  dom fi = S by RELAT_1:91;
      fi is increasing
     proof let A,B; assume
A37:    A in B & B in dom fi;
       then A in dom fi & dom fi c= dom phi by FUNCT_1:76,ORDINAL1:19;
       then fi.A = phi.A & fi.B = phi.B & B in dom phi by A37,FUNCT_1:70;
      hence thesis by A1,A37,ORDINAL2:def 16;
     end;
then A38:  sup fi = lim fi by A30,A36,Th8 .= phi.(sup L) by A35,ORDINAL2:def 14
;
      sup fi c= sup L
     proof let x; assume
A39:    x in sup fi;
      then reconsider A = x as Ordinal by ORDINAL1:23;
A40:    sup fi = sup rng fi & sup L = sup rng L by ORDINAL2:35;
      then consider B such that
A41:    B in rng fi & A c= B by A39,ORDINAL2:29;
      consider y such that
A42:    y in dom fi & B = fi.y by A41,FUNCT_1:def 5;
      reconsider y as Ordinal by A42,ORDINAL1:23;
      consider C such that
A43:    C in rng L & y c= C by A36,A40,A42,ORDINAL2:29;
      consider z such that
A44:    z in dom L & C = L.z by A43,FUNCT_1:def 5;
      reconsider z as Ordinal by A44,ORDINAL1:23;
         succ z in omega by A5,A44,ORDINAL1:41,ORDINAL2:19;
then A45:    L.succ z = phi.C & L.succ z in rng L & B = phi.y
        by A5,A7,A42,A44,FUNCT_1:70,def 5;
      reconsider C1 = C as Ordinal of W by A31,A43,Def2;
         y c< C1 iff y c= C1 & y <> C1 by XBOOLE_0:def 8;
       then y in C1 & C1 in dom phi or y = C by A31,A34,A43,ORDINAL1:21,
ORDINAL2:def 2;
       then phi.y in phi.C1 or y = C1 by A1,ORDINAL2:def 16;
       then B c= phi.C1 & phi.C1 in sup L
        by A40,A45,ORDINAL1:def 2,ORDINAL2:27;
       then B in sup L by ORDINAL1:22;
      hence thesis by A41,ORDINAL1:22;
     end;
    then not S in phi.S by A38,ORDINAL1:7;
   hence contradiction by A18;
  end;

Back to top