The abstract of the Mizar article:

Increasing and Continuous Ordinal Sequences

by

Grzegorz Bancerek

Received May 31, 1990

MML identifier: ORDINAL4

[ Mizar article, 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;


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;
end;

theorem :: ORDINAL4:1
   dom fi = succ A implies last fi is_limes_of fi & lim fi = last fi;

definition let fi,psi be T-Sequence;
 func fi^psi -> T-Sequence means
:: ORDINAL4:def 1
    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);
end;

definition let fi,psi;
 cluster fi^psi -> Ordinal-yielding;
end;

canceled;

theorem :: ORDINAL4:3
  A is_limes_of psi implies A is_limes_of fi^psi;

theorem :: ORDINAL4:4
    A is_limes_of fi implies B+^A is_limes_of B+^fi;

theorem :: ORDINAL4:5
  A is_limes_of fi implies A*^B is_limes_of fi*^B;

theorem :: ORDINAL4:6
  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;

 reserve f1,f2 for Ordinal-Sequence;

theorem :: ORDINAL4:7
   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;

theorem :: ORDINAL4:8
  dom fi <> {} & dom fi is_limit_ordinal & fi is increasing implies
   sup fi is_limes_of fi & lim fi = sup fi;

theorem :: ORDINAL4:9
  fi is increasing & A c= B & B in dom fi implies fi.A c= fi.B;

theorem :: ORDINAL4:10
  fi is increasing & A in dom fi implies A c= fi.A;

theorem :: ORDINAL4:11
  phi is increasing implies phi"A is Ordinal;

theorem :: ORDINAL4:12
  f1 is increasing implies f2*f1 is Ordinal-Sequence;

theorem :: ORDINAL4:13
   f1 is increasing & f2 is increasing implies
   ex phi st phi = f1*f2 & phi is increasing;

theorem :: ORDINAL4:14
 f1 is increasing & A is_limes_of f2 & sup rng f1 = dom f2 &
   fi = f2*f1 implies A is_limes_of fi;

theorem :: ORDINAL4:15
  phi is increasing implies phi|A is increasing;

theorem :: ORDINAL4:16
  phi is increasing & dom phi is_limit_ordinal implies
   sup phi is_limit_ordinal;

theorem :: ORDINAL4:17
   fi is increasing & fi is continuous & psi is continuous &
   phi = psi*fi implies phi is continuous;

theorem :: ORDINAL4:18
   (for A st A in dom fi holds fi.A = C+^A) implies fi is increasing;

theorem :: ORDINAL4:19
 C <> {} & (for A st A in dom fi holds fi.A = A*^C) implies fi is increasing;

theorem :: ORDINAL4:20
  A <> {} implies exp({},A) = {};

theorem :: ORDINAL4:21
  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;

theorem :: ORDINAL4:22
  C <> {} implies exp(C,A) <> {};

theorem :: ORDINAL4:23
  one in C implies exp(C,A) in exp(C,succ A);

theorem :: ORDINAL4:24
  one in C & A in B implies exp(C,A) in exp(C,B);

theorem :: ORDINAL4:25
 one in C & (for A st A in dom fi holds fi.A = exp(C,A)) implies
   fi is increasing;

theorem :: ORDINAL4:26
    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;

theorem :: ORDINAL4:27
    C <> {} & A c= B implies exp(C,A) c= exp(C,B);

theorem :: ORDINAL4:28
   A c= B implies exp(A,C) c= exp(B,C);

theorem :: ORDINAL4:29
    one in C & A <> {} implies one in exp(C,A);

theorem :: ORDINAL4:30
  exp(C,A+^B) = exp(C,B)*^exp(C,A);

theorem :: ORDINAL4:31
   exp(exp(C,A),B) = exp(C,B*^A);

theorem :: ORDINAL4:32
   one in C implies A c= exp(C,A);

scheme CriticalNumber { phi(Ordinal) -> Ordinal } :
 ex A st phi(A) = A
  provided
 for A,B st A in B holds phi(A) in phi(B) and
 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;

 reserve W for Universe;

 definition let W;
  mode Ordinal of W -> Ordinal means
:: ORDINAL4:def 2
   it in W;
  mode Ordinal-Sequence of W -> Ordinal-Sequence means
:: ORDINAL4:def 3
   dom it = On W & rng it c= On W;
 end;

definition let W;
 cluster non empty Ordinal of W;
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);

 definition let W;
  func 0-element_of W -> Ordinal of W equals
:: ORDINAL4:def 4
   {};
  func 1-element_of W -> non empty Ordinal of W equals
:: ORDINAL4:def 5
    one;
  let phi,A1;
  redefine func phi.A1 -> Ordinal of W;
 end;

 definition let W; let p2,p1 be Ordinal-Sequence of W;
  redefine func p1*p2 -> Ordinal-Sequence of W;
 end;

canceled 2;

theorem :: ORDINAL4:35
   0-element_of W = {} & 1-element_of W = one;

 definition let W,A1;
  redefine func succ A1 -> non empty Ordinal of W;
   let B1;
   func A1 +^ B1 -> Ordinal of W;
 end;

 definition let W,A1,B1;
  redefine func A1 *^ B1 -> Ordinal of W;
 end;

theorem :: ORDINAL4:36
  A1 in dom phi;

theorem :: ORDINAL4:37
  dom fi in W & rng fi c= W implies sup fi in W;

 reserve L,L1 for T-Sequence;

theorem :: ORDINAL4:38
   phi is increasing & phi is continuous & omega in W implies
   ex A st A in dom phi & phi.A = A;