The abstract of the Mizar article:

Ordinal Arithmetics

by

Grzegorz Bancerek

Received March 1, 1990

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 = {};