### The Mizar article:

### Ordinal Arithmetics

**by****Grzegorz Bancerek**

- Received March 1, 1990
Copyright (c) 1990 Association of Mizar Users

- MML identifier: ORDINAL3
- [ 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; definitions TARSKI, XBOOLE_0; theorems TARSKI, XBOOLE_0, FUNCT_1, ORDINAL1, SETFAM_1, ORDINAL2, XBOOLE_1; schemes ORDINAL1, ORDINAL2, XBOOLE_0; begin reserve fi,psi for Ordinal-Sequence, A,B,C,D for Ordinal, X,Y for set, x,y for set; theorem Th1: X c= succ X proof succ X = X \/ {X} by ORDINAL1:def 1; hence thesis by XBOOLE_1:7; end; theorem succ X c= Y implies X c= Y proof X c= succ X by Th1; hence thesis by XBOOLE_1:1; end; canceled 2; theorem A in B iff succ A in succ B proof (A in B iff succ A c= B) & (succ A c= B iff succ A in succ B) by ORDINAL1:33,34; hence thesis; end; theorem X c= A implies union X is Ordinal proof assume X c= A; then for x st x in X holds x is Ordinal by ORDINAL1:23; hence thesis by ORDINAL1:35; end; theorem union On X is Ordinal proof x in On X implies x is Ordinal by ORDINAL2:def 2; hence thesis by ORDINAL1:35; end; theorem Th8: X c= A implies On X = X proof assume A1: X c= A; defpred P[set] means $1 in X & $1 is Ordinal; A2: x in On X iff P[x] by ORDINAL2:def 2; A3: x in X iff P[x] by A1,ORDINAL1:23; thus thesis from Extensionality(A2,A3); end; theorem Th9: On {A} = {A} proof succ A = A \/ {A} by ORDINAL1:def 1; then {A} c= succ A by XBOOLE_1:7; hence thesis by Th8; end; theorem Th10: A <> {} implies {} in A proof assume A1: A <> {}; {} c= A by XBOOLE_1:2; then {} c< A by A1,XBOOLE_0:def 8; hence thesis by ORDINAL1:21; end; theorem inf A = {} proof A1: inf A = meet On A by ORDINAL2:def 6 .= meet A by ORDINAL2:10; now assume A <> {}; then {} in A by Th10; hence thesis by A1,SETFAM_1:5; end; hence thesis by A1,SETFAM_1:def 1; end; theorem inf {A} = A proof thus inf {A} = meet On {A} by ORDINAL2:def 6 .= meet {A} by Th9 .= A by SETFAM_1:11; end; theorem X c= A implies meet X is Ordinal proof assume X c= A; then On X = X by Th8; then inf X = meet X by ORDINAL2:def 6; hence thesis; end; definition let A,B; cluster A \/ B -> ordinal; coherence proof A c= B or B c= A; hence thesis by XBOOLE_1:12; end; cluster A /\ B -> ordinal; coherence proof A c= B or B c= A; hence thesis by XBOOLE_1:28; end; end; canceled; theorem A \/ B = A or A \/ B = B proof A c= B or B c= A; hence thesis by XBOOLE_1:12; end; theorem A /\ B = A or A /\ B = B proof A c= B or B c= A; hence thesis by XBOOLE_1:28; end; theorem Th17: A in one implies A = {} proof assume A in one; hence A c= {} & {} c= A by ORDINAL1:34,ORDINAL2:def 4,XBOOLE_1:2; end; theorem one = {{}} proof now let x; thus x in one implies x = {} proof assume A1: x in one; then reconsider x as Ordinal by ORDINAL1:23; x = {} by A1,Th17; hence thesis; end; thus x = {} implies x in one by ORDINAL1:10,ORDINAL2:def 4; end; hence thesis by TARSKI:def 1; end; theorem Th19: A c= one implies A = {} or A = one proof assume A1: A c= one & A <> {} & A <> one; then A c< one by XBOOLE_0:def 8; then A in one by ORDINAL1:21; hence contradiction by A1,Th17; end; theorem (A c= B or A in B) & C in D implies A+^C in B+^D proof assume A1: (A c= B or A in B) & C in D; then A c= B by ORDINAL1:def 2; then A+^C c= B+^C & B+^C in B+^D by A1,ORDINAL2:49,51; hence A+^C in B+^D by ORDINAL1:22; end; theorem A c= B & C c= D implies A+^C c= B+^D proof assume A c= B & C c= D; then A+^C c= B+^C & B+^C c= B+^D by ORDINAL2:50,51; hence A+^C c= B+^D by XBOOLE_1:1; end; theorem Th22: A in B & (C c= D & D <> {} or C in D) implies A*^C in B*^D proof assume A1: A in B & (C c= D & D <> {} or C in D); then C c= D & D <> {} by ORDINAL1:def 2; then A*^C c= A*^D & A*^D in B*^D by A1,ORDINAL2:57,59; hence A*^C in B*^D by ORDINAL1:22; end; theorem A c= B & C c= D implies A*^C c= B*^D proof assume A c= B & C c= D; then A*^C c= B*^C & B*^C c= B*^D by ORDINAL2:58,59; hence A*^C c= B*^D by XBOOLE_1:1; end; theorem Th24: B+^C = B+^D implies C = D proof assume A1: B+^C = B+^D & C <> D; then C in D or D in C by ORDINAL1:24; then B+^C in B+^C by A1,ORDINAL2:49; hence contradiction; end; theorem Th25: B+^C in B+^D implies C in D proof assume A1: B+^C in B+^D & not C in D; then D c= C by ORDINAL1:26; then B+^D c= B+^C by ORDINAL2:50; hence contradiction by A1,ORDINAL1:7; end; theorem Th26: B+^C c= B+^D implies C c= D proof A1: B+^C c= B+^D & B+^C <> B+^D iff B+^C c< B+^D by XBOOLE_0:def 8; assume B+^C c= B+^D; then B+^C = B+^D or B+^C in B+^D by A1,ORDINAL1:21; then C = D or C in D by Th24,Th25; hence thesis by ORDINAL1:def 2; end; theorem Th27: A c= A+^B & B c= A+^B proof {} c= A & {} c= B by XBOOLE_1:2; then A+^{} c= A+^B & {}+^B c= A+^B & A+^{} = A & {}+^B = B by ORDINAL2:44,47,50,51; hence thesis; end; theorem A in B implies A in B+^C & A in C+^B proof assume A1: A in B; B c= B+^C & B c= C+^B by Th27; hence thesis by A1; end; theorem Th29: A+^B = {} implies A = {} & B = {} proof assume A+^B = {}; then A c= {} & B c= {} by Th27; hence thesis by XBOOLE_1:3; end; theorem Th30: A c= B implies ex C st B = A+^C proof defpred P[Ordinal] means A c= $1 implies ex C st $1 = A+^C; A1: P[{}] proof assume A c= {}; then A = {} by XBOOLE_1:3; then {} = A+^{} by ORDINAL2:47; hence ex C st {} = A+^C; end; A2: for B st P[B] holds P[succ B] proof let B such that A3: A c= B implies ex C st B = A+^C and A4: A c= succ B; A5: A = succ B implies succ B = A+^{} by ORDINAL2:44; now assume A <> succ B; then A c< succ B by A4,XBOOLE_0:def 8; then A in succ B by ORDINAL1:21; then consider C such that A6: B = A+^C by A3,ORDINAL1:34; succ B = A+^succ C by A6,ORDINAL2:45; hence ex C st succ B = A+^C; end; hence ex C st succ B = A+^C by A5; end; A7: 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 A8: B <> {} & B is_limit_ordinal and for C st C in B holds A c= C implies ex D st C = A+^D and A9: A c= B; defpred P[Ordinal] means B c= A+^$1; {} c= A by XBOOLE_1:2; then {}+^B c= A+^B & B = {}+^B by ORDINAL2:47,51; then A10: ex C st P[C]; consider C such that A11: P[C] & for D st P[D] holds C c= D from Ordinal_Min(A10); deffunc F(Ordinal) = A +^ $1; consider L being Ordinal-Sequence such that A12: dom L = C & for D st D in C holds L.D = F(D) from OS_Lambda; A13: now assume C = {}; then A+^C = A by ORDINAL2:44; hence B = A by A9,A11,XBOOLE_0:def 10 .= A+^{} by ORDINAL2:44; end; now assume A14: C <> {}; C is_limit_ordinal proof assume not thesis; then consider D such that A15: C = succ D by ORDINAL1:42; D in C by A15,ORDINAL1:10; then not C c= D by ORDINAL1:7; then not B c= A+^D by A11; then A+^D in B by ORDINAL1:26; then succ(A+^D) = A+^succ D & succ(A+^D) c= B by ORDINAL1:33,ORDINAL2:45; then B = succ(A+^D) by A11,A15,XBOOLE_0:def 10; hence contradiction by A8,ORDINAL1:42; end; then A16: A+^C = sup L by A12,A14,ORDINAL2:46 .= sup rng L by ORDINAL2:35; for D st D in rng L holds D in B proof let D; assume D in rng L; then consider y such that A17: y in dom L & D = L.y by FUNCT_1:def 5; reconsider y as Ordinal by A17,ORDINAL1:23; A18: L.y = A+^y & not C c= y by A12,A17,ORDINAL1:7; then not B c= A+^y by A11; hence D in B by A17,A18,ORDINAL1:26; end; then sup rng L c= B by ORDINAL2:28; then B = A+^C by A11,A16,XBOOLE_0:def 10; hence ex C st B = A+^C; end; hence ex C st B = A+^C by A13; end; for B holds P[B] from Ordinal_Ind(A1,A2,A7); hence thesis; end; theorem Th31: A in B implies ex C st B = A+^C & C <> {} proof assume A1: A in B; then A c= B by ORDINAL1:def 2; then consider C such that A2: B = A+^C by Th30; take C; thus B = A+^C by A2; assume C = {}; then B = A by A2,ORDINAL2:44; hence contradiction by A1; end; theorem Th32: A <> {} & A is_limit_ordinal implies B+^A is_limit_ordinal proof assume A1: A <> {} & A is_limit_ordinal; {} c= A by XBOOLE_1:2; then {} c< A by A1,XBOOLE_0:def 8; then A2: {} in A by ORDINAL1:21; deffunc F(Ordinal) = B +^ $1; consider L being Ordinal-Sequence such that A3: dom L = A & for C st C in A holds L.C = F(C) from OS_Lambda; A4: B+^A = sup L by A1,A3,ORDINAL2:46 .= sup rng L by ORDINAL2:35; for C st C in B+^A holds succ C in B+^A proof let C such that A5: C in B+^A; A6: now assume C in B; then succ C c= B by ORDINAL1:33; then (succ C)+^{} = succ C & (succ C)+^{} c= B+^{} & B+^{} in B+^A by A2,ORDINAL2:44,49,51; hence succ C in B+^A by ORDINAL1:22; end; now assume not C in B; then B c= C by ORDINAL1:26; then consider D such that A7: C = B+^D by Th30; now assume not D in A; then A c= D by ORDINAL1:26; then B+^A c= B+^D by ORDINAL2:50; then C in C by A5,A7; hence contradiction; end; then A8: succ D in A & L.D = B+^D by A1,A3,ORDINAL1:41; then L.(succ D) = B+^succ D by A3 .= succ(B+^D) by ORDINAL2:45; then succ C in rng L by A3,A7,A8,FUNCT_1:def 5; hence succ C in B+^A by A4,ORDINAL2:27; end; hence thesis by A6; end; hence B+^A is_limit_ordinal by ORDINAL1:41; end; theorem Th33: A+^B+^C = A+^(B+^C) proof defpred Sigma[Ordinal] means A+^B+^$1 = A+^(B+^$1); A1: Sigma[{}] proof thus A+^B+^{} = A+^B by ORDINAL2:44 .= A+^(B+^{}) by ORDINAL2:44; end; A2: for C st Sigma[C] holds Sigma[succ C] proof let C such that A3: A+^B+^C = A+^(B+^C); thus A+^B+^succ C = succ(A+^B+^C) by ORDINAL2:45 .= A+^succ(B+^C) by A3,ORDINAL2:45 .= A+^(B+^succ C) by ORDINAL2:45; end; A4: for C st C <> {} & C is_limit_ordinal & for D st D in C holds Sigma[D] holds Sigma[C] proof let C such that A5: C <> {} & C is_limit_ordinal & for D st D in C holds Sigma[D]; deffunc F(Ordinal) = A +^ B +^ $1; consider L being Ordinal-Sequence such that A6: dom L = C & for D st D in C holds L.D = F(D) from OS_Lambda; A7: A+^B+^C = sup L by A5,A6,ORDINAL2:46 .= sup rng L by ORDINAL2:35; deffunc F(Ordinal) = A +^ $1; consider L1 being Ordinal-Sequence such that A8: dom L1 = B+^C & for D st D in B+^C holds L1.D = F(D) from OS_Lambda; B+^C is_limit_ordinal & B+^C <> {} by A5,Th29,Th32; then A9: A+^(B+^C) = sup L1 by A8,ORDINAL2:46 .= sup rng L1 by ORDINAL2:35; rng L c= rng L1 proof let x; assume x in rng L; then consider y such that A10: y in dom L & x = L.y by FUNCT_1:def 5; reconsider y as Ordinal by A10,ORDINAL1:23; L.y = A+^B+^y & Sigma[y] by A5,A6,A10; then A11: L.y = A+^(B+^y) & B+^y in B+^C by A6,A10,ORDINAL2:49; then L1.(B+^y) = A+^(B+^y) by A8; hence x in rng L1 by A8,A10,A11,FUNCT_1:def 5; end; hence A+^B+^C c= A+^(B+^C) by A7,A9,ORDINAL2:30; let x; assume A12: x in A+^(B+^C); then reconsider x' = x as Ordinal by ORDINAL1:23; {} c= C by XBOOLE_1:2; then A13: A+^B+^{} c= A+^B+^C & A+^B+^{} = A+^B by ORDINAL2:44,50; now assume A14: not x in A+^B; then A c= A+^B & A+^B c= x' by Th27,ORDINAL1:26; then A c= x' by XBOOLE_1:1; then consider E being Ordinal such that A15: x' = A+^E by Th30; now assume not B c= E; then E in B by ORDINAL1:26; hence contradiction by A14,A15,ORDINAL2:49; end; then consider F being Ordinal such that A16: E = B+^F by Th30; now assume not F in C; then C c= F by ORDINAL1:26; then B+^C c= B+^F by ORDINAL2:50; then A+^(B+^C) c= A+^(B+^F) by ORDINAL2:50; then x' in x' by A12,A15,A16; hence contradiction; end; then x = A+^B+^F & A+^B+^F in A+^B+^C by A5,A15,A16,ORDINAL2:49; hence x in A+^B+^C; end; hence x in A+^B+^C by A13; end; for C holds Sigma[C] from Ordinal_Ind(A1,A2,A4); hence Sigma[C]; end; theorem A*^B = {} implies A = {} or B = {} proof assume A1: A*^B = {} & A <> {} & B <> {}; {} c= A by XBOOLE_1:2; then {} c< A by A1,XBOOLE_0:def 8; then {} in A by ORDINAL1:21; hence contradiction by A1,ORDINAL2:57; end; theorem A in B & C <> {} implies A in B*^C & A in C*^B proof assume A1: A in B & C <> {}; {} c= C by XBOOLE_1:2; then {} c< C by A1,XBOOLE_0:def 8; then {} in C by ORDINAL1:21; then one c= C by ORDINAL1:33,ORDINAL2:def 4; then B*^one c= B*^C & one*^B c= C*^B & B*^one = B & one*^B = B by ORDINAL2:56,58,59; hence thesis by A1; end; theorem Th36: B*^A = C*^A & A <> {} implies B = C proof assume A1: B*^A = C*^A & A <> {} & B <> C; then B in C or C in B by ORDINAL1:24; then B*^A in B*^A by A1,ORDINAL2:57; hence contradiction; end; theorem Th37: B*^A in C*^A implies B in C proof assume A1: B*^A in C*^A & not B in C; then C c= B by ORDINAL1:26; then C*^A c= B*^A by ORDINAL2:58; hence contradiction by A1,ORDINAL1:7; end; theorem Th38: B*^A c= C*^A & A <> {} implies B c= C proof A1: B*^A c= C*^A & B*^A <> C*^A iff B*^A c< C*^A by XBOOLE_0:def 8; assume B*^A c= C*^A; then B*^A = C*^A or B*^A in C*^A by A1,ORDINAL1:21; then (A <> {} implies B = C) or B in C by Th36,Th37; hence thesis by ORDINAL1:def 2; end; theorem Th39: B <> {} implies A c= A*^B & A c= B*^A proof assume B <> {}; then {} in B by Th10; then one c= B by ORDINAL1:33,ORDINAL2:def 4; then one*^A c= B*^A & A*^one c= A*^B & A*^one = A & one*^A = A by ORDINAL2:56,58,59; hence thesis; end; canceled; theorem A*^B = one implies A = one & B = one proof assume A1: A*^B = one; then A2: B <> {} by ORDINAL2:55; {} c= B by XBOOLE_1:2; then {} c< B by A2,XBOOLE_0:def 8; then {} in B by ORDINAL1:21; then A3: one c= B by ORDINAL1:33,ORDINAL2:def 4; A4: now assume A in one; then A c= {} by ORDINAL1:34,ORDINAL2:def 4; then A = {} by XBOOLE_1:3; hence contradiction by A1,ORDINAL2:52; end; now assume one in A; then one*^B in A*^B & B = one*^B by A2,ORDINAL2:56,57; hence contradiction by A1,A3,ORDINAL1:7; end; hence A = one by A4,ORDINAL1:24; hence thesis by A1,ORDINAL2:56; end; theorem Th42: A in B+^C implies A in B or ex D st D in C & A = B+^D proof assume A1: A in B+^C & not A in B; then B c= A by ORDINAL1:26; then consider D such that A2: A = B+^D by Th30; take D; assume not thesis; then C c= D by A2,ORDINAL1:26; then B+^C c= A by A2,ORDINAL2:50; hence contradiction by A1,ORDINAL1:7; end; definition let C,fi; canceled; func C+^fi -> Ordinal-Sequence means: Def2: dom it = dom fi & for A st A in dom fi holds it.A = C+^(fi.A); existence proof deffunc F(Ordinal) = C+^(fi.$1); thus ex F being Ordinal-Sequence st dom F = dom fi & for A st A in dom fi holds F.A = F(A) from OS_Lambda; end; uniqueness proof let f1,f2 be Ordinal-Sequence such that A1: dom f1 = dom fi & for A st A in dom fi holds f1.A = C+^(fi.A) and A2: dom f2 = dom fi & for A st A in dom fi holds f2.A = C+^(fi.A); now let x; assume A3: x in dom fi; then reconsider A = x as Ordinal by ORDINAL1:23; thus f1.x = C+^(fi.A) by A1,A3 .= f2.x by A2,A3; end; hence thesis by A1,A2,FUNCT_1:9; end; func fi+^C -> Ordinal-Sequence means dom it = dom fi & for A st A in dom fi holds it.A = (fi.A)+^C; existence proof deffunc F(Ordinal) = (fi.$1)+^C; thus ex F being Ordinal-Sequence st dom F = dom fi & for A st A in dom fi holds F.A = F(A) from OS_Lambda; end; uniqueness proof let f1,f2 be Ordinal-Sequence such that A4: dom f1 = dom fi & for A st A in dom fi holds f1.A = (fi.A)+^C and A5: dom f2 = dom fi & for A st A in dom fi holds f2.A = (fi.A)+^C; now let x; assume A6: x in dom fi; then reconsider A = x as Ordinal by ORDINAL1:23; thus f1.x = (fi.A)+^C by A4,A6 .= f2.x by A5,A6; end; hence thesis by A4,A5,FUNCT_1:9; end; func C*^fi -> Ordinal-Sequence means dom it = dom fi & for A st A in dom fi holds it.A = C*^(fi.A); existence proof deffunc F(Ordinal) = C*^(fi.$1); thus ex F being Ordinal-Sequence st dom F = dom fi & for A st A in dom fi holds F.A = F(A) from OS_Lambda; end; uniqueness proof let f1,f2 be Ordinal-Sequence such that A7: dom f1 = dom fi & for A st A in dom fi holds f1.A = C*^(fi.A) and A8: dom f2 = dom fi & for A st A in dom fi holds f2.A = C*^(fi.A); now let x; assume A9: x in dom fi; then reconsider A = x as Ordinal by ORDINAL1:23; thus f1.x = C*^(fi.A) by A7,A9 .= f2.x by A8,A9; end; hence thesis by A7,A8,FUNCT_1:9; end; func fi*^C -> Ordinal-Sequence means: Def5: dom it = dom fi & for A st A in dom fi holds it.A = (fi.A)*^C; existence proof deffunc F(Ordinal) = (fi.$1)*^C; thus ex F being Ordinal-Sequence st dom F = dom fi & for A st A in dom fi holds F.A = F(A) from OS_Lambda; end; uniqueness proof let f1,f2 be Ordinal-Sequence such that A10: dom f1 = dom fi & for A st A in dom fi holds f1.A = (fi.A)*^C and A11: dom f2 = dom fi & for A st A in dom fi holds f2.A = (fi.A)*^C; now let x; assume A12: x in dom fi; then reconsider A = x as Ordinal by ORDINAL1:23; thus f1.x = (fi.A)*^C by A10,A12 .= f2.x by A11,A12; end; hence thesis by A10,A11,FUNCT_1:9; end; end; canceled 4; theorem Th47: {} <> 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 proof assume that A1: {} <> dom fi and A2: dom fi = dom psi and A3: for A,B st A in dom fi & B = fi.A holds psi.A = C+^B; A4: sup rng psi c= C+^sup rng fi proof let x; assume A5: x in sup rng psi; then reconsider A = x as Ordinal by ORDINAL1:23; consider B such that A6: B in rng psi & A c= B by A5,ORDINAL2:29; consider y such that A7: y in dom psi & B = psi.y by A6,FUNCT_1:def 5; reconsider y as Ordinal by A7,ORDINAL1:23; reconsider y' = fi.y as Ordinal; A8: B = C+^y' & y' in rng fi by A2,A3,A7,FUNCT_1:def 5; then y' in sup rng fi by ORDINAL2:27; then B in C+^sup rng fi by A8,ORDINAL2:49; hence thesis by A6,ORDINAL1:22; end; consider z being Element of dom fi; reconsider z as Ordinal by A1,ORDINAL1:23; reconsider z' = fi.z as Ordinal; A9: C+^sup rng fi c= sup rng psi proof let x; assume A10: x in C+^sup rng fi; then reconsider A = x as Ordinal by ORDINAL1:23; A11: now assume A12: A in C; C c= C+^z' & C+^z' = psi.z by A1,A3,Th27; then A13: C+^z' in rng psi & A c= C+^z' by A1,A2,A12,FUNCT_1:def 5, ORDINAL1:def 2; then C+^z' in sup rng psi by ORDINAL2:27; hence A in sup rng psi by A13,ORDINAL1:22; end; now given B such that A14: B in sup rng fi & A = C+^B; consider D such that A15: D in rng fi & B c= D by A14,ORDINAL2:29; consider x such that A16: x in dom fi & D = fi.x by A15,FUNCT_1:def 5; reconsider x as Ordinal by A16,ORDINAL1:23; psi.x = C+^D by A3,A16; then A17: C+^D in rng psi & A c= C+^D by A2,A14,A15,A16,FUNCT_1:def 5, ORDINAL2:50; then C+^D in sup rng psi by ORDINAL2:27; hence A in sup rng psi by A17,ORDINAL1:22; end; hence thesis by A10,A11,Th42; end; sup fi = sup rng fi & sup psi = sup rng psi by ORDINAL2:35; hence sup psi = C+^sup fi by A4,A9,XBOOLE_0:def 10; end; theorem Th48: A is_limit_ordinal implies A*^B is_limit_ordinal proof assume A1: A is_limit_ordinal; now assume A2: A <> {} & A is_limit_ordinal; deffunc F(Ordinal) = $1 *^ B; consider fi such that A3: dom fi = A & for C st C in A holds fi.C = F(C) from OS_Lambda; A4: A*^B = union sup fi by A2,A3,ORDINAL2:54 .= union sup rng fi by ORDINAL2:35; for C st C in A*^B holds succ C in A*^B proof let C; assume A5: C in A*^B; then consider X such that A6: C in X & X in sup rng fi by A4,TARSKI:def 4; reconsider X as Ordinal by A6,ORDINAL1:23; consider D such that A7: D in rng fi & X c= D by A6,ORDINAL2:29; consider x such that A8: x in dom fi & D = fi.x by A7,FUNCT_1:def 5; reconsider x as Ordinal by A8,ORDINAL1:23; B<>{} by A5,ORDINAL2:55; then {} in B by Th10; then succ {} c= B & x*^B+^succ {} = succ(x*^B+^{}) & x*^B+^{} = x*^B by ORDINAL1:33,ORDINAL2:44,45; then A9: succ(x*^B) c= x*^B+^B & x*^B = fi.x by A3,A8,ORDINAL2:50; A10: succ x in dom fi by A2,A3,A8,ORDINAL1:41; then fi.succ x = (succ x)*^B by A3 .= x*^B+^B by ORDINAL2:53; then x*^B+^B in rng fi & C in D by A6,A7,A10,FUNCT_1:def 5; then x*^B+^B in sup rng fi & succ C c= D by ORDINAL1:33,ORDINAL2:27; then succ C in succ D & succ D in sup rng fi by A8,A9,ORDINAL1:22,34; hence succ C in A*^B by A4,TARSKI:def 4; end; hence thesis by ORDINAL1:41; end; hence thesis by A1,ORDINAL2:52; end; theorem Th49: A in B*^C & B is_limit_ordinal implies ex D st D in B & A in D*^C proof assume A1: A in B*^C & B is_limit_ordinal; then A2: B <> {} & C <> {} by ORDINAL2:52,55; deffunc F(Ordinal) = $1 *^ C; consider fi such that A3: dom fi = B & for D st D in B holds fi.D = F(D) from OS_Lambda; B*^C = union sup fi by A1,A2,A3,ORDINAL2:54 .= union sup rng fi by ORDINAL2:35; then consider X such that A4: A in X & X in sup rng fi by A1,TARSKI:def 4; reconsider X as Ordinal by A4,ORDINAL1:23; consider D such that A5: D in rng fi & X c= D by A4,ORDINAL2:29; consider x such that A6: x in dom fi & D = fi.x by A5,FUNCT_1:def 5; reconsider x as Ordinal by A6,ORDINAL1:23; take E = succ x; thus E in B by A1,A3,A6,ORDINAL1:41; A7: E*^C = x*^C+^C by ORDINAL2:53 .= D+^C by A3,A6; D+^{} = D & {} in C by A2,Th10,ORDINAL2:44; then D in E*^C & A in D by A4,A5,A7,ORDINAL2:49; hence A in E*^C by ORDINAL1:19; end; theorem Th50: {} <> 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 proof assume that {} <> dom fi and A1: dom fi = dom psi and A2: C <> {} and A3: sup fi is_limit_ordinal and A4: for A,B st A in dom fi & B = fi.A holds psi.A = B*^C; A5: sup rng psi c= (sup rng fi)*^C proof let x; assume A6: x in sup rng psi; then reconsider A = x as Ordinal by ORDINAL1:23; consider B such that A7: B in rng psi & A c= B by A6,ORDINAL2:29; consider y such that A8: y in dom psi & B = psi.y by A7,FUNCT_1:def 5; reconsider y as Ordinal by A8,ORDINAL1:23; reconsider y' = fi.y as Ordinal; A9: B = y'*^C & y' in rng fi by A1,A4,A8,FUNCT_1:def 5; then y' in sup rng fi by ORDINAL2:27; then B in (sup rng fi)*^C by A2,A9,ORDINAL2:57; hence thesis by A7,ORDINAL1:22; end; A10: sup fi = sup rng fi & sup psi = sup rng psi by ORDINAL2:35; (sup rng fi)*^C c= sup rng psi proof let x; assume A11: x in (sup rng fi)*^C; then reconsider A = x as Ordinal by ORDINAL1:23; consider B such that A12: B in sup rng fi & A in B*^C by A3,A10,A11,Th49; consider D such that A13: D in rng fi & B c= D by A12,ORDINAL2:29; consider y such that A14: y in dom fi & D = fi.y by A13,FUNCT_1:def 5; reconsider y as Ordinal by A14,ORDINAL1:23; reconsider y' = psi.y as Ordinal; y' in rng psi & y' = D*^C by A1,A4,A14,FUNCT_1:def 5; then D*^C in sup rng psi & B*^C c= D*^C by A13,ORDINAL2:27,58; hence thesis by A12,ORDINAL1:19; end; hence sup psi = (sup fi)*^C by A5,A10,XBOOLE_0:def 10; end; theorem Th51: {} <> dom fi implies sup (C+^fi) = C+^sup fi proof A1: dom (C+^fi) = dom fi by Def2; for A,B st A in dom fi & B = fi.A holds (C+^fi).A = C+^B by Def2; hence thesis by A1,Th47; end; theorem Th52: {} <> dom fi & C <> {} & sup fi is_limit_ordinal implies sup (fi*^C) = (sup fi)*^C proof A1: dom (fi*^C) = dom fi by Def5; for A,B st A in dom fi & B = fi.A holds (fi*^C).A = B*^C by Def5; hence thesis by A1,Th50; end; theorem Th53: B <> {} implies union(A+^B) = A+^union B proof assume A1: B <> {}; A2: now given C such that A3: B = succ C; thus union(A+^B) = union succ (A+^C) by A3,ORDINAL2:45 .= A+^C by ORDINAL2:2 .= A+^union B by A3,ORDINAL2:2; end; now assume not ex C st B = succ C; then A4: B is_limit_ordinal by ORDINAL1:42; then A+^B is_limit_ordinal by A1,Th32; then union(A+^B) = A+^B & union B = B by A4,ORDINAL1:def 6; hence thesis; end; hence thesis by A2; end; theorem Th54: (A+^B)*^C = A*^C +^ B*^C proof defpred S[Ordinal] means (A+^$1)*^C = A*^C +^ $1*^C; A1: S[{}] proof thus (A+^{})*^C = A*^C by ORDINAL2:44 .= A*^C +^ {} by ORDINAL2:44 .= A*^C +^ {}*^C by ORDINAL2:52; end; A2: for B st S[B] holds S[succ B] proof let B such that A3: (A+^B)*^C = A*^C +^ B*^C; thus (A+^succ B)*^C = (succ(A+^B))*^C by ORDINAL2:45 .= A*^C +^ B*^C +^ C by A3,ORDINAL2:53 .= A*^C +^ (B*^C +^ C) by Th33 .= A*^C +^ (succ B)*^C by ORDINAL2:53; end; A4: for B st B <> {} & B is_limit_ordinal & for D st D in B holds S[D] holds S[B] proof let B such that A5: B <> {} & B is_limit_ordinal & for D st D in B holds S[D]; deffunc F(Ordinal) = 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 *^ C; consider psi such that A7: dom psi = B & for D st D in B holds psi.D = F(D) from OS_Lambda; A8: A+^B = sup fi & A+^B is_limit_ordinal by A5,A6,Th32,ORDINAL2:46; A9: dom (fi*^C) = dom fi & dom (A*^C+^psi) = dom psi by Def2,Def5; now let x; assume A10: x in B; then reconsider k = x as Ordinal by ORDINAL1:23; reconsider m = fi.k, n = psi.k as Ordinal; thus (fi*^C).x = m*^C by A6,A10,Def5 .= (A+^k)*^C by A6,A10 .= A*^C+^k*^C by A5,A10 .= A*^C+^n by A7,A10 .= (A*^C+^psi).x by A7,A10,Def2; end; then A11: fi*^C = A*^C+^psi by A6,A7,A9,FUNCT_1:9; A12: {} in B by A5,Th10; reconsider k = psi.{} as Ordinal; k in rng psi by A7,A12,FUNCT_1:def 5; then k in sup rng psi by ORDINAL2:27; then A13: sup psi <> {} & (A+^B)*^C is_limit_ordinal by A8,Th48,ORDINAL2:35; A14: now assume C <> {}; then (A+^B)*^C = sup(fi*^C) by A5,A6,A8,Th52 .= A*^C+^sup psi by A5,A7,A11,Th51; hence (A+^B)*^C = union(A*^C+^sup psi) by A13,ORDINAL1:def 6 .= A*^C+^union sup psi by A13,Th53 .= A*^C+^B*^C by A5,A7,ORDINAL2:54; end; now assume C = {}; then (A+^B)*^C = {} & A*^C = {} & B*^C = {} & {}+^{} = {} by ORDINAL2:44,55; hence thesis; end; hence thesis by A14; end; for B holds S[B] from Ordinal_Ind(A1,A2,A4); hence S[B]; end; theorem Th55: A <> {} implies ex C,D st B = C*^A+^D & D in A proof assume A1: A <> {}; defpred I[Ordinal] means ex C,D st $1 = C*^A+^D & D in A; A2: I[{}] proof take C = {}, D = {}; thus {} = {}+^{} by ORDINAL2:44 .= C*^A+^D by ORDINAL2:52; thus thesis by A1,Th10; end; A3: for B st I[B] holds I[succ B] proof let B; given C,D such that A4: B = C*^A+^D & D in A; A5: now assume A6: succ D in A; take C1 = C, D1 = succ D; thus C1*^A+^D1 = succ B by A4,ORDINAL2:45; thus D1 in A by A6; end; now assume not succ D in A; then A c= succ D & succ D c= A by A4,ORDINAL1:26,33; then A7: A = succ D by XBOOLE_0:def 10; take C1 = succ C, D1 = {}; thus C1*^A+^D1 = C1*^A by ORDINAL2:44 .= C*^A+^A by ORDINAL2:53 .= succ B by A4,A7,ORDINAL2:45; thus D1 in A by A1,Th10; end; hence thesis by A5; end; A8: for B st B <> {} & B is_limit_ordinal & for A st A in B holds I[A] holds I[B] proof let B such that A9: B <> {} & B is_limit_ordinal & for A st A in B holds I[A]; {} in A by A1,Th10; then succ {} c= A & B*^one = B by ORDINAL1:33,ORDINAL2:56; then A10: B c= B*^A by ORDINAL2:59,def 4; A11: B = B*^A implies B = B*^A+^{} & {} in A by A1,Th10,ORDINAL2:44; defpred P[Ordinal] means $1 in B & B in $1*^A; now assume B <> B*^A; then B c< B*^A by A10,XBOOLE_0:def 8; then B in B*^A by ORDINAL1:21; then A12: ex C st P[C] by A9,Th49; consider C such that A13: P[C] and A14: for C1 being Ordinal st P[C1] holds C c= C1 from Ordinal_Min(A12); now assume C is_limit_ordinal; then consider C1 being Ordinal such that A15: C1 in C & B in C1*^A by A13,Th49; C1 in B by A13,A15,ORDINAL1:19; then C c= C1 by A14,A15; hence contradiction by A15,ORDINAL1:7; end; then consider C1 being Ordinal such that A16: C = succ C1 by ORDINAL1:42; C1 in C by A16,ORDINAL1:10; then C1 in B & not C c= C1 by A13,ORDINAL1:7,19; then not B in C1*^A by A14; then C1*^A c= B by ORDINAL1:26; then consider D such that A17: B = C1*^A+^D by Th30; thus I[B] proof take C1,D; thus B = C1*^A+^D by A17; C1*^A+^D in C1*^A+^A by A13,A16,A17,ORDINAL2:53; hence thesis by Th25; end; end; hence thesis by A11; end; for B holds I[B] from Ordinal_Ind(A2,A3,A8); hence I[B]; end; theorem Th56: 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 proof let C1,D1,C2,D2 be Ordinal such that A1: C1*^A+^D1 = C2*^A+^D2 & D1 in A & D2 in A; set B = C1*^A+^D1; A2: now assume C1 in C2; then consider C such that A3: C2 = C1+^C & C <> {} by Th31; B = C1*^A+^C*^A+^D2 by A1,A3,Th54 .= C1*^A+^(C*^A+^D2) by Th33; then D1 = C*^A+^D2 & A c= C*^A & C*^A c= C*^A+^D2 by A3,Th24,Th27,Th39; hence contradiction by A1,ORDINAL1:7; end; now assume C2 in C1; then consider C such that A4: C1 = C2+^C & C <> {} by Th31; B = C2*^A+^C*^A+^D1 by A4,Th54 .= C2*^A+^(C*^A+^D1) by Th33; then D2 = C*^A+^D1 & A c= C*^A & C*^A c= C*^A+^D1 by A1,A4,Th24,Th27,Th39 ; hence contradiction by A1,ORDINAL1:7; end; hence C1 = C2 by A2,ORDINAL1:24; hence D1 = D2 by A1,Th24; end; theorem Th57: 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 proof assume A1: one in B & A <> {} & A is_limit_ordinal; let fi; assume A2: dom fi = A & for C st C in A holds fi.C = C*^B; then A3: A*^B = union sup fi by A1,ORDINAL2:54; now given C such that A4: sup fi = succ C; A5: C in sup fi & sup fi = sup rng fi by A4,ORDINAL1:10,ORDINAL2:35; then consider D such that A6: D in rng fi & C c= D by ORDINAL2:29; D in sup fi by A5,A6,ORDINAL2:27; then succ D c= succ C & succ C c= succ D by A4,A6,ORDINAL1:33,ORDINAL2:1 ; then succ C = succ D by XBOOLE_0:def 10; then C = D by ORDINAL1:12; then consider x such that A7: x in dom fi & C = fi.x by A6,FUNCT_1:def 5; reconsider x as Ordinal by A7,ORDINAL1:23; A8: succ x in dom fi by A1,A2,A7,ORDINAL1:41; then C = x*^B & fi.succ x = (succ x)*^B & C+^one in C+^B & (succ x)*^B = x*^B+^B by A1,A2,A7,ORDINAL2:49,53; then C+^B in rng fi & sup fi in C+^B by A4,A8,FUNCT_1:def 5,ORDINAL2:48; hence contradiction by A5,ORDINAL2:27; end; then sup fi is_limit_ordinal by ORDINAL1:42; hence A*^B = sup fi by A3,ORDINAL1:def 6; end; theorem (A*^B)*^C = A*^(B*^C) proof defpred P[Ordinal] means ($1*^B)*^C = $1*^(B*^C); {}*^B = {} & {}*^C = {} & {}*^(B*^C) = {} by ORDINAL2:52; then A1: P[{}]; A2: for A st P[A] holds P[succ A] proof let A such that A3: (A*^B)*^C = A*^(B*^C); thus ((succ A)*^B)*^C = (A*^B+^B)*^C by ORDINAL2:53 .= A*^(B*^C)+^B*^C by A3,Th54 .= A*^(B*^C)+^one*^(B*^C) by ORDINAL2:56 .= (A+^one)*^(B*^C) by Th54 .= (succ A)*^(B*^C) by ORDINAL2:48; end; A4: for A st A <> {} & A is_limit_ordinal & for D st D in A holds P[D] holds P[A] proof let A such that A5: A <> {} & A is_limit_ordinal and A6: for D st D in A holds (D*^B)*^C = D*^(B*^C); A7: now assume not (one in B & one in C); then B c= one or C c= one by ORDINAL1:26; then A8: B = {} or B = one or C = {} or C = one by Th19; A*^{} = {} & {}*^C = {} & A*^one = A & one*^C = C & (A*^B)*^{} = {} & B*^{} = {} & A*^B*^one = A*^B & B*^one = B by ORDINAL2:52,55,56; hence (A*^B)*^C = A*^(B*^C) by A8; end; now assume A9: one in B & one in C; one = one*^one by ORDINAL2:56; then A10: one in B*^C & C <> {} by A9,Th22; deffunc F(Ordinal) = $1 *^ B; consider fi such that A11: dom fi = A & for D st D in A holds fi.D = F(D) from OS_Lambda; dom(fi*^C) = A & for D st D in A holds (fi*^C).D = D*^(B*^C) proof thus dom(fi*^C) = A by A11,Def5; let D; assume D in A; then (fi*^C).D = (fi.D)*^C & fi.D = D*^B & D*^B*^C = D*^(B*^C) by A6,A11,Def5; hence (fi*^C).D = D*^(B*^C); end; then A*^B = sup fi & A*^(B*^C) = sup(fi*^C) & A*^B is_limit_ordinal by A5,A9,A10,A11,Th48,Th57; hence A*^B*^C = A*^(B*^C) by A5,A9,A11,Th52; end; hence (A*^B)*^C = A*^(B*^C) by A7; end; for A holds P[A] from Ordinal_Ind(A1,A2,A4); hence thesis; end; definition let A,B; func A -^ B -> Ordinal means: Def6: A = B+^it if B c= A otherwise it = {}; existence by Th30; uniqueness by Th24; consistency; func A div^ B -> Ordinal means: Def7: ex C st A = it*^B+^C & C in B if B <> {} otherwise it = {}; consistency; existence by Th55; uniqueness by Th56; end; definition let A,B; func A mod^ B -> Ordinal equals: Def8: A-^(A div^ B)*^B; correctness; end; canceled; theorem A in B implies B = A+^(B-^A) proof assume A in B; then A c= B by ORDINAL1:def 2; hence thesis by Def6; end; canceled 4; theorem Th65: A+^B-^A = B proof A c= A+^B by Th27; hence thesis by Def6; end; theorem Th66: A in B & (C c= A or C in A) implies A-^C in B-^C proof assume A1: A in B & (C c= A or C in A); then A c= B & C c= A by ORDINAL1:def 2; then A2: A = C+^(A-^C) & C c= B by Def6,XBOOLE_1:1; then B = C+^(B-^C) by Def6; hence A-^C in B-^C by A1,A2,Th25; end; theorem Th67: A-^A = {} proof A+^{} = A & A c= A by ORDINAL2:44; hence thesis by Def6; end; theorem A in B implies B-^A <> {} & {} in B-^A proof assume A in B; then A-^A in B-^A & A-^A = {} by Th66,Th67; hence thesis; end; theorem Th69: A-^{} = A & {}-^A = {} proof A1: {} c= A & {}+^A = A by ORDINAL2:47,XBOOLE_1:2; hence A-^{} = A by Def6; not A c= {} or A c= {}; then thesis or A = {} by Def6,XBOOLE_1:3; hence thesis by A1,Def6; end; theorem A-^(B+^C) = (A-^B)-^C proof now per cases; suppose B+^C c= A; then A = B+^C+^(A-^(B+^C)) by Def6; then A = B+^(C+^(A-^(B+^C))) by Th33; then C+^(A-^(B+^C)) = A-^B by Th65; hence thesis by Th65; suppose A1: not B+^C c= A; then A2: A-^(B+^C) = {} by Def6; B c= A or not B c= A; then A3: A = B+^(A-^B) or A-^B = {} by Def6; now assume A = B+^(A-^B); then not C c= A-^B by A1,ORDINAL2:50; hence A-^B-^C = {} by Def6; end; hence thesis by A2,A3,Th69; end; hence thesis; end; theorem A c= B implies C-^B c= C-^A proof assume A1: A c= B; then A2: B = A+^(B-^A) by Def6; A3: now assume B c= C; then A c= C & C = B+^(C-^B) by A1,Def6,XBOOLE_1:1; then B+^(C-^B) = A+^(C-^A) by Def6; then A+^((B-^A)+^(C-^B)) = A+^(C-^A) by A2,Th33; then (B-^A)+^(C-^B) = C-^A by Th24; hence thesis by Th27; end; now assume not B c= C; then C-^B = {} by Def6; hence thesis by XBOOLE_1:2; end; hence thesis by A3; end; theorem A c= B implies A-^C c= B-^C proof assume A1: A c= B; A2: now assume C c= A; then C c= B & A = C+^(A-^C) by A1,Def6,XBOOLE_1:1; then C+^(A-^C) c= C+^(B-^C) by A1,Def6; hence thesis by Th26; end; now assume not C c= A; then A-^C = {} by Def6; hence thesis by XBOOLE_1:2; end; hence thesis by A2; end; theorem C <> {} & A in B+^C implies A-^B in C proof assume A1: C <> {}; A2: (B c= A implies A = B+^(A-^B)) & (not B c= A implies A-^B = {}) by Def6; B+^C-^B = C by Th65; hence thesis by A1,A2,Th10,Th66; end; theorem A+^B in C implies B in C-^A proof A c= A+^B & A+^B-^A = B by Th27,Th65; hence thesis by Th66; end; theorem A c= B+^(A-^B) proof now per cases; suppose B c= A; hence thesis by Def6; suppose not B c= A; then A-^B = {} & A in B & B+^{} = B by Def6,ORDINAL1:26,ORDINAL2:44; hence thesis by ORDINAL1:def 2; end; hence thesis; end; theorem A*^C -^ B*^C = (A-^B)*^C proof A1: now assume B c= A; then A = B+^(A-^B) by Def6; then A*^C = B*^C+^(A-^B)*^C by Th54; hence thesis by Th65; end; now assume not B c= A; then A-^B = {} & (not B*^C c= A*^C or C = {}) & A*^{} = {} & {}*^C = {} by Def6,Th38,ORDINAL2:52,55; hence thesis by Def6,Th69; end; hence thesis by A1; end; theorem Th77: (A div^ B)*^B c= A proof now per cases; suppose B <> {}; then ex C st A = (A div^ B)*^B+^C & C in B by Def7 ; hence thesis by Th27; suppose B = {}; then A div^ B = {} by Def7; then (A div^ B)*^B = {} by ORDINAL2:52; hence thesis by XBOOLE_1:2; end; hence thesis; end; theorem Th78: A = (A div^ B)*^B+^(A mod^ B) proof (A div^ B)*^B c= A & A mod^ B = A-^(A div^ B)*^B by Def8,Th77; hence thesis by Def6; end; theorem A = B*^C+^D & D in C implies B = A div^ C & D = A mod^ C proof assume A1: A = B*^C+^D & D in C; hence B = A div^ C by Def7; then A-^(A div^ C)*^C = D by A1,Th65; hence D = A mod^ C by Def8; end; theorem A in B*^C implies A div^ C in B & A mod^ C in C proof assume A1: A in B*^C; then C <> {} by ORDINAL2:55; then A2: ex D st A = (A div^ C)*^C+^D & D in C by Def7; assume A3: not thesis; A = (A div^ C)*^C+^(A mod^ C) by Th78; then B c= A div^ C by A2,A3,Th24,ORDINAL1:26; then B*^C c= (A div^ C)*^C & (A div^ C)*^C c= A by A2,Th27,ORDINAL2:58; hence contradiction by A1,ORDINAL1:7; end; theorem Th81: B <> {} implies A*^B div^ B = A proof assume B <> {}; then {} in B & A*^B = A*^B+^{} by Th10,ORDINAL2:44; hence thesis by Def7; end; theorem A*^B mod^ B = {} proof A*^{} = {} & {} div^ {} = {} & A*^B mod^ B = A*^B-^(A*^B div^ B)*^B & {}-^(A*^B div^ B)*^B = {} & (B = {} or B <> {}) & A*^B-^A*^B = {} by Def7,Def8,Th67,Th69,ORDINAL2:55; hence thesis by Th81; end; theorem {} div^ A = {} & {} mod^ A = {} & A mod^ {} = A proof {} = {}*^A & (A = {} or A <> {}) by ORDINAL2:52; hence {} div^ A = {} by Def7,Th81; thus {} mod^ A = {}-^({} div^ A)*^A by Def8 .= {} by Th69; thus A mod^ {} = A-^(A div^ {})*^{} by Def8 .= A-^{} by ORDINAL2:55 .= A by Th69; end; theorem A div^ one = A & A mod^ one = {} proof A = A*^one & A = A+^{} & {} in one by Th10,ORDINAL2:44,56; hence A div^ one = A by Def7; hence A mod^ one = A-^A*^one by Def8 .= A-^A by ORDINAL2:56 .= {} by Th67; end;

Back to top