Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990 Association of Mizar Users

### Increasing and Continuous Ordinal Sequences

by
Grzegorz Bancerek

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