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

### Ordinal Arithmetics

by
Grzegorz Bancerek

MML identifier: ORDINAL3
[ Mizar article, MML identifier index ]

```environ

vocabulary ORDINAL2, ORDINAL1, BOOLE, TARSKI, SETFAM_1, FUNCT_1, RELAT_1,
ORDINAL3;
notation TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, SETFAM_1,
ORDINAL2;
constructors SETFAM_1, ORDINAL2, XBOOLE_0;
clusters ORDINAL1, ZFMISC_1, XBOOLE_0, ORDINAL2;
requirements SUBSET, BOOLE;

begin

reserve fi,psi for Ordinal-Sequence,
A,B,C,D for Ordinal,
X,Y for set,
x,y for set;

theorem :: ORDINAL3:1
X c= succ X;

theorem :: ORDINAL3:2
succ X c= Y implies X c= Y;

canceled 2;

theorem :: ORDINAL3:5
A in B iff succ A in succ B;

theorem :: ORDINAL3:6
X c= A implies union X is Ordinal;

theorem :: ORDINAL3:7
union On X is Ordinal;

theorem :: ORDINAL3:8
X c= A implies On X = X;

theorem :: ORDINAL3:9
On {A} = {A};

theorem :: ORDINAL3:10
A <> {} implies {} in A;

theorem :: ORDINAL3:11
inf A = {};

theorem :: ORDINAL3:12
inf {A} = A;

theorem :: ORDINAL3:13
X c= A implies meet X is Ordinal;

definition let A,B;
cluster A \/ B -> ordinal;
cluster A /\ B -> ordinal;
end;

canceled;

theorem :: ORDINAL3:15
A \/ B = A or A \/ B = B;

theorem :: ORDINAL3:16
A /\ B = A or A /\ B = B;

theorem :: ORDINAL3:17
A in one implies A = {};

theorem :: ORDINAL3:18
one = {{}};

theorem :: ORDINAL3:19
A c= one implies A = {} or A = one;

theorem :: ORDINAL3:20
(A c= B or A in B) & C in D implies A+^C in B+^D;

theorem :: ORDINAL3:21
A c= B & C c= D implies A+^C c= B+^D;

theorem :: ORDINAL3:22
A in B & (C c= D & D <> {} or C in D) implies A*^C in B*^D;

theorem :: ORDINAL3:23
A c= B & C c= D implies A*^C c= B*^D;

theorem :: ORDINAL3:24
B+^C = B+^D implies C = D;

theorem :: ORDINAL3:25
B+^C in B+^D implies C in D;

theorem :: ORDINAL3:26
B+^C c= B+^D implies C c= D;

theorem :: ORDINAL3:27
A c= A+^B & B c= A+^B;

theorem :: ORDINAL3:28
A in B implies A in B+^C & A in C+^B;

theorem :: ORDINAL3:29
A+^B = {} implies A = {} & B = {};

theorem :: ORDINAL3:30
A c= B implies ex C st B = A+^C;

theorem :: ORDINAL3:31
A in B implies ex C st B = A+^C & C <> {};

theorem :: ORDINAL3:32
A <> {} & A is_limit_ordinal implies B+^A is_limit_ordinal;

theorem :: ORDINAL3:33
A+^B+^C = A+^(B+^C);

theorem :: ORDINAL3:34
A*^B = {} implies A = {} or B = {};

theorem :: ORDINAL3:35
A in B & C <> {} implies A in B*^C & A in C*^B;

theorem :: ORDINAL3:36
B*^A = C*^A & A <> {} implies B = C;

theorem :: ORDINAL3:37
B*^A in C*^A implies B in C;

theorem :: ORDINAL3:38
B*^A c= C*^A & A <> {} implies B c= C;

theorem :: ORDINAL3:39
B <> {} implies A c= A*^B & A c= B*^A;

canceled;

theorem :: ORDINAL3:41
A*^B = one implies A = one & B = one;

theorem :: ORDINAL3:42
A in B+^C implies A in B or ex D st D in C & A = B+^D;

definition let C,fi;
canceled;

func C+^fi -> Ordinal-Sequence means
:: ORDINAL3:def 2
dom it = dom fi & for A st A in dom fi holds it.A = C+^(fi.A);
func fi+^C -> Ordinal-Sequence means
:: ORDINAL3:def 3
dom it = dom fi & for A st A in dom fi holds it.A = (fi.A)+^C;
func C*^fi -> Ordinal-Sequence means
:: ORDINAL3:def 4
dom it = dom fi & for A st A in dom fi holds it.A = C*^(fi.A);
func fi*^C -> Ordinal-Sequence means
:: ORDINAL3:def 5
dom it = dom fi & for A st A in dom fi holds it.A = (fi.A)*^C;
end;

canceled 4;

theorem :: ORDINAL3:47
{} <> dom fi & dom fi = dom psi &
(for A,B st A in dom fi & B = fi.A holds psi.A = C+^B) implies
sup psi = C+^sup fi;

theorem :: ORDINAL3:48
A is_limit_ordinal implies A*^B is_limit_ordinal;

theorem :: ORDINAL3:49
A in B*^C & B is_limit_ordinal implies ex D st D in B & A in D*^C;

theorem :: ORDINAL3:50
{} <> dom fi & dom fi = dom psi & C <> {} & sup fi is_limit_ordinal &
(for A,B st A in dom fi & B = fi.A holds psi.A = B*^C) implies
sup psi = (sup fi)*^C;

theorem :: ORDINAL3:51
{} <> dom fi implies sup (C+^fi) = C+^sup fi;

theorem :: ORDINAL3:52
{} <> dom fi & C <> {} & sup fi is_limit_ordinal implies
sup (fi*^C) = (sup fi)*^C;

theorem :: ORDINAL3:53
B <> {} implies union(A+^B) = A+^union B;

theorem :: ORDINAL3:54
(A+^B)*^C = A*^C +^ B*^C;

theorem :: ORDINAL3:55
A <> {} implies ex C,D st B = C*^A+^D & D in A;

theorem :: ORDINAL3:56
for C1,D1,C2,D2 being Ordinal st C1*^A+^D1 = C2*^A+^D2 & D1 in A & D2 in
A
holds C1 = C2 & D1 = D2;

theorem :: ORDINAL3:57
one in B & A <> {} & A is_limit_ordinal implies
for fi st dom fi = A & for C st C in A holds fi.C = C*^B holds A*^B = sup fi
;

theorem :: ORDINAL3:58
(A*^B)*^C = A*^(B*^C);

definition let A,B;
func A -^ B -> Ordinal means
:: ORDINAL3:def 6
A = B+^it if B c= A otherwise it = {};
func A div^ B -> Ordinal means
:: ORDINAL3:def 7
ex C st A = it*^B+^C & C in B if B <> {} otherwise it = {};
end;

definition let A,B;
func A mod^ B -> Ordinal equals
:: ORDINAL3:def 8
A-^(A div^ B)*^B;
end;

canceled;

theorem :: ORDINAL3:60
A in B implies B = A+^(B-^A);

canceled 4;

theorem :: ORDINAL3:65
A+^B-^A = B;

theorem :: ORDINAL3:66
A in B & (C c= A or C in A) implies A-^C in B-^C;

theorem :: ORDINAL3:67
A-^A = {};

theorem :: ORDINAL3:68
A in B implies B-^A <> {} & {} in B-^A;

theorem :: ORDINAL3:69
A-^{} = A & {}-^A = {};

theorem :: ORDINAL3:70
A-^(B+^C) = (A-^B)-^C;

theorem :: ORDINAL3:71
A c= B implies C-^B c= C-^A;

theorem :: ORDINAL3:72
A c= B implies A-^C c= B-^C;

theorem :: ORDINAL3:73
C <> {} & A in B+^C implies A-^B in C;

theorem :: ORDINAL3:74
A+^B in C implies B in C-^A;

theorem :: ORDINAL3:75
A c= B+^(A-^B);

theorem :: ORDINAL3:76
A*^C -^ B*^C = (A-^B)*^C;

theorem :: ORDINAL3:77
(A div^ B)*^B c= A;

theorem :: ORDINAL3:78
A = (A div^ B)*^B+^(A mod^ B);

theorem :: ORDINAL3:79
A = B*^C+^D & D in C implies B = A div^ C & D = A mod^ C;

theorem :: ORDINAL3:80
A in B*^C implies A div^ C in B & A mod^ C in C;

theorem :: ORDINAL3:81
B <> {} implies A*^B div^ B = A;

theorem :: ORDINAL3:82
A*^B mod^ B = {};

theorem :: ORDINAL3:83
{} div^ A = {} & {} mod^ A = {} & A mod^ {} = A;

theorem :: ORDINAL3:84
A div^ one = A & A mod^ one = {};
```