:: Ordinal Arithmetics
:: by Grzegorz Bancerek
::
:: Received March 1, 1990
:: Copyright (c) 1990-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies ORDINAL2, ORDINAL1, TARSKI, XBOOLE_0, SETFAM_1, RELAT_1, FUNCT_1,
SUBSET_1, ORDINAL3, CARD_1;
notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, SETFAM_1,
ORDINAL2;
constructors SETFAM_1, ORDINAL2, XTUPLE_0;
registrations XBOOLE_0, ORDINAL1, ORDINAL2;
requirements SUBSET, BOOLE, NUMERALS;
definitions ORDINAL2, ORDINAL1, TARSKI, XBOOLE_0;
equalities ORDINAL2, ORDINAL1;
expansions ORDINAL2, ORDINAL1, TARSKI, XBOOLE_0;
theorems TARSKI, FUNCT_1, ORDINAL1, SETFAM_1, ORDINAL2, XBOOLE_1, ZFMISC_1;
schemes ORDINAL1, ORDINAL2, XBOOLE_0;
begin
reserve fi,psi for Ordinal-Sequence,
A,A1,B,C,D for Ordinal,
X,Y for set,
x,y for object;
theorem
X c= succ X by XBOOLE_1:7;
theorem
succ X c= Y implies X c= Y
proof
X c= succ X by XBOOLE_1:7;
hence thesis;
end;
theorem
A in B iff succ A in succ B
proof
A in B iff succ A c= B by ORDINAL1:21;
hence thesis by ORDINAL1:22;
end;
theorem
X c= A implies union X is epsilon-transitive epsilon-connected set
proof
assume X c= A;
then for x st x in X holds x is Ordinal;
hence thesis by ORDINAL1:23;
end;
theorem Th5:
union On X is epsilon-transitive epsilon-connected set
proof
x in On X implies x is Ordinal by ORDINAL1:def 9;
hence thesis by ORDINAL1:23;
end;
theorem Th6:
X c= A implies On X = X
proof
defpred P[object] means $1 in X & $1 is Ordinal;
assume X c= A;
then
A1: for x being object holds x in X iff P[x];
A2: for x being object holds x in On X iff P[x] by ORDINAL1:def 9;
thus thesis from XBOOLE_0:sch 2(A2,A1);
end;
theorem Th7:
On {A} = {A}
proof
{A} c= succ A by XBOOLE_1:7;
hence thesis by Th6;
end;
theorem Th8:
A <> {} implies {} in A
proof
A1: {} c= A;
assume A <> {};
then {} c< A by A1;
hence thesis by ORDINAL1:11;
end;
theorem
inf A = {}
proof
A1: inf A = meet A by ORDINAL2:8;
then A <> {} implies thesis by Th8,SETFAM_1:4;
hence thesis by A1,SETFAM_1:def 1;
end;
theorem
inf {A} = A
proof
thus inf {A} = meet {A} by Th7
.= A by SETFAM_1:10;
end;
theorem
X c= A implies meet X is Ordinal
proof
assume X c= A;
then inf X = meet X by Th6;
hence thesis;
end;
registration
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;
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;
Lm1: 1 = succ 0;
theorem Th14:
A in 1 implies A = {}
proof
assume A in 1;
hence A c= {} & {} c= A by Lm1,ORDINAL1:22;
end;
theorem
1 = {{}} by Lm1;
theorem Th16:
A c= 1 implies A = {} or A = 1
proof
assume that
A1: A c= 1 and
A2: A <> {} and
A3: A <> 1;
A c< 1 by A1,A3;
hence contradiction by A2,Th14,ORDINAL1:11;
end;
theorem
(A c= B or A in B) & C in D implies A+^C in B+^D
proof
assume that
A1: A c= B or A in B and
A2: C in D;
A3: B+^C in B+^D by A2,ORDINAL2:32;
A c= B by A1,ORDINAL1:def 2;
hence thesis by A3,ORDINAL1:12,ORDINAL2:34;
end;
theorem
A c= B & C c= D implies A+^C c= B+^D
proof
assume that
A1: A c= B and
A2: C c= D;
A3: B+^C c= B+^D by A2,ORDINAL2:33;
A+^C c= B+^C by A1,ORDINAL2:34;
hence thesis by A3;
end;
theorem Th19:
A in B & (C c= D & D <> {} or C in D) implies A*^C in B*^D
proof
assume that
A1: A in B and
A2: C c= D & D <> {} or C in D;
A3: C c= D by A2,ORDINAL1:def 2;
A*^D in B*^D by A1,A2,ORDINAL2:40;
hence thesis by A3,ORDINAL1:12,ORDINAL2:42;
end;
theorem
A c= B & C c= D implies A*^C c= B*^D
proof
assume that
A1: A c= B and
A2: C c= D;
A3: B*^C c= B*^D by A2,ORDINAL2:42;
A*^C c= B*^C by A1,ORDINAL2:41;
hence thesis by A3;
end;
theorem Th21:
B+^C = B+^D implies C = D
proof
assume that
A1: B+^C = B+^D and
A2: C <> D;
C in D or D in C by A2,ORDINAL1:14;
then B+^C in B+^C by A1,ORDINAL2:32;
hence contradiction;
end;
theorem Th22:
B+^C in B+^D implies C in D
proof
assume that
A1: B+^C in B+^D and
A2: not C in D;
D c= C by A2,ORDINAL1:16;
hence contradiction by A1,ORDINAL1:5,ORDINAL2:33;
end;
theorem Th23:
B+^C c= B+^D implies C c= D
proof
assume
A1: B+^C c= B+^D;
B+^C c= B+^D & B+^C <> B+^D iff B+^C c< B+^D;
then C = D or C in D by A1,Th21,Th22,ORDINAL1:11;
hence thesis by ORDINAL1:def 2;
end;
theorem Th24:
A c= A+^B & B c= A+^B
proof
A1: {}+^B c= A+^B by ORDINAL2:34,XBOOLE_1:2;
A+^{} c= A+^B by ORDINAL2:33,XBOOLE_1:2;
hence thesis by A1,ORDINAL2:27,30;
end;
theorem
A in B implies A in B+^C & A in C+^B
proof
assume
A1: A in B;
A2: B c= C+^B by Th24;
B c= B+^C by Th24;
hence thesis by A1,A2;
end;
theorem Th26:
A+^B = {} implies A = {} & B = {} by Th24,XBOOLE_1:3;
theorem Th27:
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: for B st P[B] holds P[succ B]
proof
let B such that
A2: A c= B implies ex C st B = A+^C and
A3: A c= succ B;
A4: now
assume A <> succ B;
then A c< succ B by A3;
then A in succ B by ORDINAL1:11;
then consider C such that
A5: B = A+^C by A2,ORDINAL1:22;
succ B = A+^succ C by A5,ORDINAL2:28;
hence thesis;
end;
A = succ B implies succ B = A+^{} by ORDINAL2:27;
hence thesis by A4;
end;
A6: for B st B <> 0 & B is limit_ordinal & for C st C in B holds P[C]
holds P[B]
proof
deffunc F(Ordinal) = A +^ $1;
let B such that
B <> 0 and
A7: B is limit_ordinal and
for C st C in B holds A c= C implies ex D st C = A+^D and
A8: A c= B;
defpred P[Ordinal] means B c= A+^$1;
A9: B = {}+^B by ORDINAL2:30;
{}+^B c= A+^B by ORDINAL2:34,XBOOLE_1:2;
then
A10: ex C st P[C] by A9;
consider C such that
A11: P[C] & for D st P[D] holds C c= D from ORDINAL1:sch 1(A10);
consider L being Ordinal-Sequence such that
A12: dom L = C & for D st D in C holds L.D = F(D) from ORDINAL2:sch 3;
A13: now
for D st D in rng L holds D in B
proof
let D;
assume D in rng L;
then consider y being object such that
A14: y in dom L and
A15: D = L.y by FUNCT_1:def 3;
reconsider y as Ordinal by A14;
A16: not C c= y by A12,A14,ORDINAL1:5;
L.y = A+^y by A12,A14;
hence thesis by A11,A15,A16,ORDINAL1:16;
end;
then
A17: sup rng L c= B by ORDINAL2:20;
A18: C is limit_ordinal
proof
assume not thesis;
then consider D such that
A19: C = succ D by ORDINAL1:29;
not C c= D by A19,ORDINAL1:5,6;
then A+^D in B by A11,ORDINAL1:16;
then
A20: succ(A+^D) c= B by ORDINAL1:21;
succ(A+^D) = A+^succ D by ORDINAL2:28;
then B = succ(A+^D) by A11,A19,A20;
hence contradiction by A7,ORDINAL1:29;
end;
assume C <> {};
then A+^C = sup L by A12,A18,ORDINAL2:29
.= sup rng L;
then B = A+^C by A11,A17;
hence thesis;
end;
C = {} implies B = A+^{} by A8,A11,ORDINAL2:27;
hence thesis by A13;
end;
A21: P[0]
proof
assume A c= 0;
then A = {} by XBOOLE_1:3;
then {} = A+^{} by ORDINAL2:30;
hence thesis;
end;
for B holds P[B] from ORDINAL2:sch 1(A21,A1,A6);
hence thesis;
end;
theorem Th28:
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 Th27;
take C;
thus B = A+^C by A2;
assume C = {};
then B = A by A2,ORDINAL2:27;
hence contradiction by A1;
end;
theorem Th29:
A <> {} & A is limit_ordinal implies B+^A is limit_ordinal
proof
assume that
A1: A <> {} and
A2: A is limit_ordinal;
{} c= A;
then
A3: {} c< A by A1;
deffunc F(Ordinal) = B +^ $1;
consider L being Ordinal-Sequence such that
A4: dom L = A & for C st C in A holds L.C = F(C) from ORDINAL2:sch 3;
A5: B+^A = sup L by A1,A2,A4,ORDINAL2:29
.= sup rng L;
for C st C in B+^A holds succ C in B+^A
proof
let C such that
A6: C in B+^A;
A7: now
assume not C in B;
then consider D such that
A8: C = B+^D by Th27,ORDINAL1:16;
now
assume not D in A;
then B+^A c= B+^D by ORDINAL1:16,ORDINAL2:33;
then C in C by A6,A8;
hence contradiction;
end;
then
A9: succ D in A by A2,ORDINAL1:28;
then L.(succ D) = B+^succ D by A4
.= succ(B+^D) by ORDINAL2:28;
then succ C in rng L by A4,A8,A9,FUNCT_1:def 3;
hence thesis by A5,ORDINAL2:19;
end;
now
assume C in B;
then
A10: succ C c= B by ORDINAL1:21;
A11: (succ C)+^{} = succ C by ORDINAL2:27;
B+^{} in B+^A by A3,ORDINAL1:11,ORDINAL2:32;
hence thesis by A10,A11,ORDINAL1:12,ORDINAL2:34;
end;
hence thesis by A7;
end;
hence thesis by ORDINAL1:28;
end;
theorem Th30:
A+^B+^C = A+^(B+^C)
proof
defpred Sigma[Ordinal] means A+^B+^$1 = A+^(B+^$1);
A1: for C st Sigma[C] holds Sigma[succ C]
proof
let C such that
A2: A+^B+^C = A+^(B+^C);
thus A+^B+^succ C = succ(A+^B+^C) by ORDINAL2:28
.= A+^succ(B+^C) by A2,ORDINAL2:28
.= A+^(B+^succ C) by ORDINAL2:28;
end;
A3: for C st C <> 0 & C is limit_ordinal & for D st D in C holds Sigma[D]
holds Sigma[C]
proof
deffunc F(Ordinal) = A +^ B +^ $1;
let C such that
A4: C <> 0 and
A5: C is limit_ordinal and
A6: for D st D in C holds Sigma[D];
consider L being Ordinal-Sequence such that
A7: dom L = C & for D st D in C holds L.D = F(D) from ORDINAL2:sch 3;
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
ORDINAL2:sch 3;
A9: rng L c= rng L1
proof
let x be object;
assume x in rng L;
then consider y being object such that
A10: y in dom L and
A11: x = L.y by FUNCT_1:def 3;
reconsider y as Ordinal by A10;
A12: B+^y in B+^C by A7,A10,ORDINAL2:32;
L.y = A+^B+^y by A7,A10;
then
A13: L.y = A+^(B+^y) by A6,A7,A10;
L1.(B+^y) = A+^(B+^y) by A7,A8,A10,ORDINAL2:32;
hence thesis by A8,A11,A13,A12,FUNCT_1:def 3;
end;
A14: B+^C <> {} by A4,Th26;
B+^C is limit_ordinal by A4,A5,Th29;
then
A15: A+^(B+^C) = sup L1 by A8,A14,ORDINAL2:29
.= sup rng L1;
A+^B+^C = sup L by A4,A5,A7,ORDINAL2:29
.= sup rng L;
hence A+^B+^C c= A+^(B+^C) by A15,A9,ORDINAL2:22;
let x be object;
assume
A16: x in A+^(B+^C);
then reconsider x9 = x as Ordinal;
A17: now
A18: A c= A+^B by Th24;
assume
A19: not x in A+^B;
then A+^B c= x9 by ORDINAL1:16;
then consider E being Ordinal such that
A20: x9 = A+^E by A18,Th27,XBOOLE_1:1;
B c= E by A19,A20,ORDINAL1:16,ORDINAL2:32;
then consider F being Ordinal such that
A21: E = B+^F by Th27;
A22: now
assume not F in C;
then B+^C c= B+^F by ORDINAL1:16,ORDINAL2:33;
then A+^(B+^C) c= A+^(B+^F) by ORDINAL2:33;
then x9 in x9 by A16,A20,A21;
hence contradiction;
end;
then x = A+^B+^F by A6,A20,A21;
hence thesis by A22,ORDINAL2:32;
end;
A23: A+^B+^{} = A+^B by ORDINAL2:27;
A+^B+^{} c= A+^B+^C by ORDINAL2:33,XBOOLE_1:2;
hence thesis by A23,A17;
end;
A+^B+^{} = A+^B by ORDINAL2:27
.= A+^(B+^{}) by ORDINAL2:27;
then
A24: Sigma[0];
for C holds Sigma[C] from ORDINAL2:sch 1(A24,A1,A3);
hence thesis;
end;
theorem
A*^B = {} implies A = {} or B = {}
proof
assume that
A1: A*^B = {} and
A2: A <> {} and
A3: B <> {};
{} c= A;
then {} c< A by A2;
hence contradiction by A1,A3,ORDINAL1:11,ORDINAL2:40;
end;
theorem
A in B & C <> {} implies A in B*^C & A in C*^B
proof
assume that
A1: A in B and
A2: C <> {};
{} c= C;
then {} c< C by A2;
then {} in C by ORDINAL1:11;
then
A3: 1 c= C by Lm1,ORDINAL1:21;
then
A4: 1*^B c= C*^B by ORDINAL2:41;
A5: 1*^B = B by ORDINAL2:39;
A6: B*^1 = B by ORDINAL2:39;
B*^1 c= B*^C by A3,ORDINAL2:42;
hence thesis by A1,A4,A6,A5;
end;
theorem Th33:
B*^A = C*^A & A <> {} implies B = C
proof
assume that
A1: B*^A = C*^A and
A2: A <> {} and
A3: B <> C;
B in C or C in B by A3,ORDINAL1:14;
then B*^A in B*^A by A1,A2,ORDINAL2:40;
hence contradiction;
end;
theorem Th34:
B*^A in C*^A implies B in C
proof
assume that
A1: B*^A in C*^A and
A2: not B in C;
C c= B by A2,ORDINAL1:16;
hence contradiction by A1,ORDINAL1:5,ORDINAL2:41;
end;
theorem Th35:
B*^A c= C*^A & A <> {} implies B c= C
proof
assume
A1: B*^A c= C*^A;
B*^A c= C*^A & B*^A <> C*^A iff B*^A c< C*^A;
then (A <> {} implies B = C) or B in C by A1,Th33,Th34,ORDINAL1:11;
hence thesis by ORDINAL1:def 2;
end;
theorem Th36:
B <> {} implies A c= A*^B & A c= B*^A
proof
assume B <> {};
then {} in B by Th8;
then
A1: 1 c= B by Lm1,ORDINAL1:21;
then
A2: A*^1 c= A*^B by ORDINAL2:42;
1*^A c= B*^A by A1,ORDINAL2:41;
hence thesis by A2,ORDINAL2:39;
end;
theorem
A*^B = 1 implies A = 1 & B = 1
proof
assume
A1: A*^B = 1;
then
A2: B <> {} by ORDINAL2:38;
{} c= B;
then {} c< B by A2;
then {} in B by ORDINAL1:11;
then
A3: 1 c= B by Lm1,ORDINAL1:21;
A4: now
A5: B = 1*^B by ORDINAL2:39;
assume 1 in A;
hence contradiction by A1,A2,A3,A5,ORDINAL1:5,ORDINAL2:40;
end;
now
assume A in 1;
then A c= {} by Lm1,ORDINAL1:22;
then A = {} by XBOOLE_1:3;
hence contradiction by A1,ORDINAL2:35;
end;
hence A = 1 by A4,ORDINAL1:14;
hence thesis by A1,ORDINAL2:39;
end;
theorem Th38:
A in B+^C implies A in B or ex D st D in C & A = B+^D
proof
assume that
A1: A in B+^C and
A2: not A in B;
consider D such that
A3: A = B+^D by A2,Th27,ORDINAL1:16;
take D;
assume not thesis;
then C c= D by A3,ORDINAL1:16;
hence contradiction by A1,A3,ORDINAL1:5,ORDINAL2:33;
end;
definition
let C,fi;
func C+^fi -> Ordinal-Sequence means
: Def1:
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 ORDINAL2:sch 3;
end;
uniqueness
proof
let f1,f2 be Ordinal-Sequence such that
A1: dom f1 = dom fi and
A2: for A st A in dom fi holds f1.A = C+^(fi.A) and
A3: dom f2 = dom fi and
A4: for A st A in dom fi holds f2.A = C+^(fi.A);
now
let x be object;
assume
A5: x in dom fi;
then reconsider A = x as Ordinal;
thus f1.x = C+^(fi.A) by A2,A5
.= f2.x by A4,A5;
end;
hence thesis by A1,A3,FUNCT_1:2;
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 ORDINAL2:sch 3;
end;
uniqueness
proof
let f1,f2 be Ordinal-Sequence such that
A6: dom f1 = dom fi and
A7: for A st A in dom fi holds f1.A = (fi.A)+^C and
A8: dom f2 = dom fi and
A9: for A st A in dom fi holds f2.A = (fi.A)+^C;
now
let x be object;
assume
A10: x in dom fi;
then reconsider A = x as Ordinal;
thus f1.x = (fi.A)+^C by A7,A10
.= f2.x by A9,A10;
end;
hence thesis by A6,A8,FUNCT_1:2;
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 ORDINAL2:sch 3;
end;
uniqueness
proof
let f1,f2 be Ordinal-Sequence such that
A11: dom f1 = dom fi and
A12: for A st A in dom fi holds f1.A = C*^(fi.A) and
A13: dom f2 = dom fi and
A14: for A st A in dom fi holds f2.A = C*^(fi.A);
now
let x be object;
assume
A15: x in dom fi;
then reconsider A = x as Ordinal;
thus f1.x = C*^(fi.A) by A12,A15
.= f2.x by A14,A15;
end;
hence thesis by A11,A13,FUNCT_1:2;
end;
func fi*^C -> Ordinal-Sequence means
: Def4:
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 ORDINAL2:sch 3;
end;
uniqueness
proof
let f1,f2 be Ordinal-Sequence such that
A16: dom f1 = dom fi and
A17: for A st A in dom fi holds f1.A = (fi.A)*^C and
A18: dom f2 = dom fi and
A19: for A st A in dom fi holds f2.A = (fi.A)*^C;
now
let x be object;
assume
A20: x in dom fi;
then reconsider A = x as Ordinal;
thus f1.x = (fi.A)*^C by A17,A20
.= f2.x by A19,A20;
end;
hence thesis by A16,A18,FUNCT_1:2;
end;
end;
theorem Th39:
{} <> 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;
set z = the Element of dom fi;
reconsider z9 = fi.z as Ordinal;
A4: C+^sup rng fi c= sup rng psi
proof
let x be object;
assume
A5: x in C+^sup rng fi;
then reconsider A = x as Ordinal;
A6: now
given B such that
A7: B in sup rng fi and
A8: A = C+^B;
consider D such that
A9: D in rng fi and
A10: B c= D by A7,ORDINAL2:21;
consider x being object such that
A11: x in dom fi and
A12: D = fi.x by A9,FUNCT_1:def 3;
reconsider x as Ordinal by A11;
psi.x = C+^D by A3,A11,A12;
then C+^D in rng psi by A2,A11,FUNCT_1:def 3;
then C+^D in sup rng psi by ORDINAL2:19;
hence A in sup rng psi by A8,A10,ORDINAL1:12,ORDINAL2:33;
end;
now
C+^z9 = psi.z by A1,A3;
then C+^z9 in rng psi by A1,A2,FUNCT_1:def 3;
then
A13: C+^z9 in sup rng psi by ORDINAL2:19;
assume
A14: A in C;
C c= C+^z9 by Th24;
then A c= C+^z9 by A14,ORDINAL1:def 2;
hence A in sup rng psi by A13,ORDINAL1:12;
end;
hence thesis by A5,A6,Th38;
end;
sup rng psi c= C+^sup rng fi
proof
let x be object;
assume
A15: x in sup rng psi;
then reconsider A = x as Ordinal;
consider B such that
A16: B in rng psi and
A17: A c= B by A15,ORDINAL2:21;
consider y being object such that
A18: y in dom psi and
A19: B = psi.y by A16,FUNCT_1:def 3;
reconsider y as Ordinal by A18;
reconsider y9 = fi.y as Ordinal;
y9 in rng fi by A2,A18,FUNCT_1:def 3;
then
A20: y9 in sup rng fi by ORDINAL2:19;
B = C+^y9 by A2,A3,A18,A19;
then B in C+^sup rng fi by A20,ORDINAL2:32;
hence thesis by A17,ORDINAL1:12;
end;
hence thesis by A4;
end;
theorem Th40:
A is limit_ordinal implies A*^B is limit_ordinal
proof
A1: now
deffunc F(Ordinal) = $1 *^ B;
assume that
A2: A <> {} and
A3: A is limit_ordinal;
consider fi such that
A4: dom fi = A & for C st C in A holds fi.C = F(C) from ORDINAL2:sch 3;
A5: A*^B = union sup fi by A2,A3,A4,ORDINAL2:37
.= union sup rng fi;
for C st C in A*^B holds succ C in A*^B
proof
let C;
assume
A6: C in A*^B;
then consider X such that
A7: C in X and
A8: X in sup rng fi by A5,TARSKI:def 4;
reconsider X as Ordinal by A8;
consider D such that
A9: D in rng fi and
A10: X c= D by A8,ORDINAL2:21;
consider x being object such that
A11: x in dom fi and
A12: D = fi.x by A9,FUNCT_1:def 3;
succ C c= D by A7,A10,ORDINAL1:21;
then
A13: succ C in succ D by ORDINAL1:22;
reconsider x as Ordinal by A11;
A14: succ x in dom fi by A3,A4,A11,ORDINAL1:28;
then fi.succ x = (succ x)*^B by A4
.= x*^B+^B by ORDINAL2:36;
then x*^B+^B in rng fi by A14,FUNCT_1:def 3;
then
A15: x*^B+^B in sup rng fi by ORDINAL2:19;
A16: x*^B+^succ {} = succ(x*^B+^{}) by ORDINAL2:28;
B<>{} by A6,ORDINAL2:38;
then {} in B by Th8;
then
A17: succ {} c= B by ORDINAL1:21;
A18: x*^B+^{} = x*^B by ORDINAL2:27;
x*^B = fi.x by A4,A11;
then succ D in sup rng fi by A12,A17,A16,A18,A15,ORDINAL1:12,ORDINAL2:33;
hence thesis by A5,A13,TARSKI:def 4;
end;
hence thesis by ORDINAL1:28;
end;
assume A is limit_ordinal;
hence thesis by A1,ORDINAL2:35;
end;
theorem Th41:
A in B*^C & B is limit_ordinal implies ex D st D in B & A in D*^ C
proof
assume that
A1: A in B*^C and
A2: B is limit_ordinal;
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 ORDINAL2:sch 3;
B <> {} by A1,ORDINAL2:35;
then B*^C = union sup fi by A2,A3,ORDINAL2:37
.= union sup rng fi;
then consider X such that
A4: A in X and
A5: X in sup rng fi by A1,TARSKI:def 4;
reconsider X as Ordinal by A5;
consider D such that
A6: D in rng fi and
A7: X c= D by A5,ORDINAL2:21;
consider x being object such that
A8: x in dom fi and
A9: D = fi.x by A6,FUNCT_1:def 3;
reconsider x as Ordinal by A8;
take E = succ x;
thus E in B by A2,A3,A8,ORDINAL1:28;
A10: D+^{} = D by ORDINAL2:27;
A11: C <> {} by A1,ORDINAL2:38;
E*^C = x*^C+^C by ORDINAL2:36
.= D+^C by A3,A8,A9;
then D in E*^C by A11,A10,Th8,ORDINAL2:32;
hence thesis by A4,A7,ORDINAL1:10;
end;
theorem Th42:
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
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 fi)*^C c= sup rng psi
proof
let x be object;
assume
A6: x in (sup rng fi)*^C;
then reconsider A = x as Ordinal;
consider B such that
A7: B in sup rng fi and
A8: A in B*^C by A3,A6,Th41;
consider D such that
A9: D in rng fi and
A10: B c= D by A7,ORDINAL2:21;
consider y being object such that
A11: y in dom fi and
A12: D = fi.y by A9,FUNCT_1:def 3;
reconsider y as Ordinal by A11;
reconsider y9 = psi.y as Ordinal;
A13: y9 in rng psi by A1,A11,FUNCT_1:def 3;
y9 = D*^C by A4,A11,A12;
then
A14: D*^C in sup rng psi by A13,ORDINAL2:19;
B*^C c= D*^C by A10,ORDINAL2:41;
hence thesis by A8,A14,ORDINAL1:10;
end;
sup rng psi c= (sup rng fi)*^C
proof
let x be object;
assume
A15: x in sup rng psi;
then reconsider A = x as Ordinal;
consider B such that
A16: B in rng psi and
A17: A c= B by A15,ORDINAL2:21;
consider y being object such that
A18: y in dom psi and
A19: B = psi.y by A16,FUNCT_1:def 3;
reconsider y as Ordinal by A18;
reconsider y9 = fi.y as Ordinal;
y9 in rng fi by A1,A18,FUNCT_1:def 3;
then
A20: y9 in sup rng fi by ORDINAL2:19;
B = y9*^C by A1,A4,A18,A19;
then B in (sup rng fi)*^C by A2,A20,ORDINAL2:40;
hence thesis by A17,ORDINAL1:12;
end;
hence thesis by A5;
end;
theorem Th43:
{} <> dom fi implies sup (C+^fi) = C+^sup fi
proof
A1: for A,B st A in dom fi & B = fi.A holds (C+^fi).A = C+^B by Def1;
dom (C+^fi) = dom fi by Def1;
hence thesis by A1,Th39;
end;
theorem Th44:
{} <> dom fi & C <> {} & sup fi is limit_ordinal implies sup (fi
*^C) = (sup fi)*^C
proof
A1: for A,B st A in dom fi & B = fi.A holds (fi*^C).A = B*^C by Def4;
dom (fi*^C) = dom fi by Def4;
hence thesis by A1,Th42;
end;
theorem Th45:
B <> {} implies union(A+^B) = A+^union B
proof
assume
A1: B <> {};
A2: now
assume not ex C st B = succ C;
then
A3: B is limit_ordinal by ORDINAL1:29;
then A+^B is limit_ordinal by A1,Th29;
then union(A+^B) = A+^B;
hence thesis by A3;
end;
now
given C such that
A4: B = succ C;
thus union(A+^B) = union succ (A+^C) by A4,ORDINAL2:28
.= A+^C by ORDINAL2:2
.= A+^union B by A4,ORDINAL2:2;
end;
hence thesis by A2;
end;
theorem Th46:
(A+^B)*^C = A*^C +^ B*^C
proof
defpred S[Ordinal] means (A+^$1)*^C = A*^C +^ $1*^C;
A1: for B st S[B] holds S[succ B]
proof
let B such that
A2: (A+^B)*^C = A*^C +^ B*^C;
thus (A+^succ B)*^C = (succ(A+^B))*^C by ORDINAL2:28
.= A*^C +^ B*^C +^ C by A2,ORDINAL2:36
.= A*^C +^ (B*^C +^ C) by Th30
.= A*^C +^ (succ B)*^C by ORDINAL2:36;
end;
A3: for B st B <> 0 & B is limit_ordinal & for D st D in B holds S[D] holds
S[B]
proof
deffunc F(Ordinal) = A +^ $1;
let B such that
A4: B <> 0 and
A5: B is limit_ordinal and
A6: for D st D in B holds S[D];
consider fi such that
A7: dom fi = B & for D st D in B holds fi.D = F(D) from ORDINAL2:sch
3;
A+^B is limit_ordinal by A4,A5,Th29;
then
A8: (A+^B)*^C is limit_ordinal by Th40;
A9: dom (fi*^C) = dom fi by Def4;
A10: now
assume
A11: C = {};
then
A12: A*^C = {} by ORDINAL2:38;
A13: B*^C = {} by A11,ORDINAL2:38;
(A+^B)*^C = {} by A11,ORDINAL2:38;
hence thesis by A12,A13,ORDINAL2:27;
end;
deffunc F(Ordinal) = $1 *^ C;
consider psi such that
A14: dom psi = B & for D st D in B holds psi.D = F(D) from ORDINAL2:
sch 3;
A15: now
let x be object;
assume
A16: x in B;
then reconsider k = x as Ordinal;
reconsider m = fi.k, n = psi.k as Ordinal;
thus (fi*^C).x = m*^C by A7,A16,Def4
.= (A+^k)*^C by A7,A16
.= A*^C+^k*^C by A6,A16
.= A*^C+^n by A14,A16
.= (A*^C+^psi).x by A14,A16,Def1;
end;
reconsider k = psi.{} as Ordinal;
{} in B by A4,Th8;
then k in rng psi by A14,FUNCT_1:def 3;
then
A17: k in sup rng psi by ORDINAL2:19;
dom (A*^C+^psi) = dom psi by Def1;
then
A18: fi*^C = A*^C+^psi by A7,A14,A9,A15,FUNCT_1:2;
A19: A+^B = sup fi by A4,A5,A7,ORDINAL2:29;
now
assume C <> {};
then (A+^B)*^C = sup(fi*^C) by A4,A5,A7,A19,Th29,Th44
.= A*^C+^sup psi by A4,A14,A18,Th43;
hence (A+^B)*^C = union(A*^C+^sup psi) by A8
.= A*^C+^union sup psi by A17,Th45
.= A*^C+^B*^C by A4,A5,A14,ORDINAL2:37;
end;
hence thesis by A10;
end;
(A+^{})*^C = A*^C by ORDINAL2:27
.= A*^C +^ {} by ORDINAL2:27
.= A*^C +^ {}*^C by ORDINAL2:35;
then
A20: S[0];
for B holds S[B] from ORDINAL2:sch 1(A20,A1,A3);
hence thesis;
end;
theorem Th47:
A <> {} implies ex C,D st B = C*^A+^D & D in A
proof
defpred I[Ordinal] means ex C,D st $1 = C*^A+^D & D in A;
assume
A1: A <> {};
A2: for B st B <> 0 & B is limit_ordinal & for A1 st A1 in B holds I[A1]
holds I[B]
proof
{} in A by A1,Th8;
then
A3: succ 0 c= A by ORDINAL1:21;
let B such that
B <> 0 and
A4: B is limit_ordinal and
for A1 st A1 in B holds I[A1];
defpred P[Ordinal] means $1 in B & B in $1*^A;
B*^1 = B by ORDINAL2:39;
then
A5: B c= B*^A by A3,ORDINAL2:42;
A6: now
assume B <> B*^A;
then B c< B*^A by A5;
then B in B*^A by ORDINAL1:11;
then
A7: ex C st P[C] by A4,Th41;
consider C such that
A8: P[C] and
A9: for C1 being Ordinal st P[C1] holds C c= C1 from ORDINAL1:sch 1
(A7);
now
assume C is limit_ordinal;
then consider C1 being Ordinal such that
A10: C1 in C and
A11: B in C1*^A by A8,Th41;
C1 in B by A8,A10,ORDINAL1:10;
hence contradiction by A9,A10,A11,ORDINAL1:5;
end;
then consider C1 being Ordinal such that
A12: C = succ C1 by ORDINAL1:29;
A13: C1 in C by A12,ORDINAL1:6;
then C1 in B by A8,ORDINAL1:10;
then not B in C1*^A by A9,A13,ORDINAL1:5;
then consider D such that
A14: B = C1*^A+^D by Th27,ORDINAL1:16;
thus I[B]
proof
take C1,D;
thus B = C1*^A+^D by A14;
C1*^A+^D in C1*^A+^A by A8,A12,A14,ORDINAL2:36;
hence thesis by Th22;
end;
end;
B = B*^A implies B = B*^A+^{} & {} in A by A1,Th8,ORDINAL2:27;
hence thesis by A6;
end;
A15: for B st I[B] holds I[succ B]
proof
let B;
given C,D such that
A16: B = C*^A+^D and
A17: D in A;
A18: now
assume not succ D in A;
then
A19: A c= succ D by ORDINAL1:16;
take C1 = succ C, D1 = {};
succ D c= A by A17,ORDINAL1:21;
then
A20: A = succ D by A19;
thus C1*^A+^D1 = C1*^A by ORDINAL2:27
.= C*^A+^A by ORDINAL2:36
.= succ B by A16,A20,ORDINAL2:28;
thus D1 in A by A1,Th8;
end;
now
assume
A21: succ D in A;
take C1 = C, D1 = succ D;
thus C1*^A+^D1 = succ B by A16,ORDINAL2:28;
thus D1 in A by A21;
end;
hence thesis by A18;
end;
A22: I[0]
proof
take C = {}, D = {};
thus 0 = {}+^{} by ORDINAL2:27
.= C*^A+^D by ORDINAL2:35;
thus thesis by A1,Th8;
end;
for B holds I[B] from ORDINAL2:sch 1(A22,A15,A2);
hence thesis;
end;
theorem Th48:
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 and
A2: D1 in A and
A3: D2 in A;
set B = C1*^A+^D1;
A4: now
assume C2 in C1;
then consider C such that
A5: C1 = C2+^C and
A6: C <> {} by Th28;
B = C2*^A+^C*^A+^D1 by A5,Th46
.= C2*^A+^(C*^A+^D1) by Th30;
then
A7: D2 = C*^A+^D1 by A1,Th21;
A8: C*^A c= C*^A+^D1 by Th24;
A c= C*^A by A6,Th36;
hence contradiction by A3,A7,A8,ORDINAL1:5;
end;
now
assume C1 in C2;
then consider C such that
A9: C2 = C1+^C and
A10: C <> {} by Th28;
B = C1*^A+^C*^A+^D2 by A1,A9,Th46
.= C1*^A+^(C*^A+^D2) by Th30;
then
A11: D1 = C*^A+^D2 by Th21;
A12: C*^A c= C*^A+^D2 by Th24;
A c= C*^A by A10,Th36;
hence contradiction by A2,A11,A12,ORDINAL1:5;
end;
hence C1 = C2 by A4,ORDINAL1:14;
hence thesis by A1,Th21;
end;
theorem Th49:
1 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 that
A1: 1 in B and
A2: A <> {} and
A3: A is limit_ordinal;
let fi;
assume that
A4: dom fi = A and
A5: for C st C in A holds fi.C = C*^B;
now
given C such that
A6: sup fi = succ C;
consider D such that
A7: D in rng fi and
A8: C c= D by A6,ORDINAL1:6,ORDINAL2:21;
D in sup fi by A7,ORDINAL2:19;
then
A9: succ D c= succ C by A6,ORDINAL1:21;
succ C c= succ D by A8,ORDINAL2:1;
then succ C = succ D by A9;
then C = D by ORDINAL1:7;
then consider x being object such that
A10: x in dom fi and
A11: C = fi.x by A7,FUNCT_1:def 3;
reconsider x as Ordinal by A10;
A12: C = x*^B by A4,A5,A10,A11;
C+^1 in C+^B by A1,ORDINAL2:32;
then
A13: sup fi in C+^B by A6,ORDINAL2:31;
A14: (succ x)*^B = x*^B+^B by ORDINAL2:36;
A15: succ x in dom fi by A3,A4,A10,ORDINAL1:28;
then fi.succ x = (succ x)*^B by A4,A5;
then C+^B in rng fi by A15,A12,A14,FUNCT_1:def 3;
hence contradiction by A13,ORDINAL2:19;
end;
then
A16: sup fi is limit_ordinal by ORDINAL1:29;
A*^B = union sup fi by A2,A3,A4,A5,ORDINAL2:37;
hence thesis by A16;
end;
theorem
(A*^B)*^C = A*^(B*^C)
proof
defpred P[Ordinal] means ($1*^B)*^C = $1*^(B*^C);
A1: {}*^C = {} by ORDINAL2:35;
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:36
.= A*^(B*^C)+^B*^C by A3,Th46
.= A*^(B*^C)+^1*^(B*^C) by ORDINAL2:39
.= (A+^1)*^(B*^C) by Th46
.= (succ A)*^(B*^C) by ORDINAL2:31;
end;
A4: for A st A <> 0 & A is limit_ordinal & for D st D in A holds P[D] holds
P[A]
proof
let A such that
A5: A <> 0 and
A6: A is limit_ordinal and
A7: for D st D in A holds (D*^B)*^C = D*^(B*^C);
A8: now
deffunc F(Ordinal) = $1 *^ B;
assume that
A9: 1 in B and
A10: 1 in C;
consider fi such that
A11: dom fi = A & for D st D in A holds fi.D = F(D) from ORDINAL2:
sch 3;
A12: 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,Def4;
let D;
assume
A13: D in A;
then
A14: fi.D = D*^B by A11;
(fi*^C).D = (fi.D)*^C by A11,A13,Def4;
hence thesis by A7,A13,A14;
end;
1 = 1*^1 by ORDINAL2:39;
then 1 in B*^C by A9,A10,Th19;
then
A15: A*^(B*^C) = sup(fi*^C) by A5,A6,A12,Th49;
A*^B = sup fi by A5,A6,A9,A11,Th49;
hence thesis by A5,A6,A10,A11,A15,Th40,Th44;
end;
now
assume not (1 in B & 1 in C);
then
A16: B = {} or B = 1 or C = {} or C = 1 by Th16,ORDINAL1:16;
A17: {}*^C = {} by ORDINAL2:35;
A18: A*^B*^1 = A*^B by ORDINAL2:39;
A19: (A*^B)*^{} = {} by ORDINAL2:38;
A20: A*^1 = A by ORDINAL2:39;
A*^{} = {} by ORDINAL2:38;
hence thesis by A16,A17,A20,A19,A18,ORDINAL2:38,39;
end;
hence thesis by A8;
end;
{}*^B = {} by ORDINAL2:35;
then
A21: P[0] by A1,ORDINAL2:35;
for A holds P[A] from ORDINAL2:sch 1(A21,A2,A4);
hence thesis;
end;
definition
let A,B;
func A -^ B -> Ordinal means
: Def5:
A = B+^it if B c= A otherwise it = {};
existence by Th27;
uniqueness by Th21;
consistency;
func A div^ B -> Ordinal means
: Def6:
ex C st A = it*^B+^C & C in B if B <> {} otherwise it = {};
consistency;
existence by Th47;
uniqueness by Th48;
end;
definition
let A,B;
func A mod^ B -> Ordinal equals
A-^(A div^ B)*^B;
correctness;
end;
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 Def5;
end;
theorem Th52:
A+^B-^A = B
proof
A c= A+^B by Th24;
hence thesis by Def5;
end;
theorem Th53:
A in B & (C c= A or C in A) implies A-^C in B-^C
proof
assume that
A1: A in B and
A2: C c= A or C in A;
A c= B by A1,ORDINAL1:def 2;
then C c= B by A2,ORDINAL1:def 2;
then
A3: B = C+^(B-^C) by Def5;
C c= A by A2,ORDINAL1:def 2;
then A = C+^(A-^C) by Def5;
hence thesis by A1,A3,Th22;
end;
theorem Th54:
A-^A = {}
proof
A+^{} = A by ORDINAL2:27;
hence thesis by Def5;
end;
theorem
A in B implies B-^A <> {} & {} in B-^A
proof
assume A in B;
then A-^A in B-^A by Th53;
hence thesis by Th54;
end;
theorem Th56:
A-^{} = A & {}-^A = {}
proof
A1: {}+^A = A by ORDINAL2:30;
{} c= A;
hence A-^{} = A by A1,Def5;
not A c= {} or A c= {};
then thesis or A = {} by Def5,XBOOLE_1:3;
hence thesis by A1,Def5;
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 Def5;
then A = B+^(C+^(A-^(B+^C))) by Th30;
then C+^(A-^(B+^C)) = A-^B by Th52;
hence thesis by Th52;
end;
suppose
A1: not B+^C c= A;
A2: now
assume A = B+^(A-^B);
then not C c= A-^B by A1,ORDINAL2:33;
hence A-^B-^C = {} by Def5;
end;
B c= A or not B c= A;
then
A3: A = B+^(A-^B) or A-^B = {} by Def5;
A-^(B+^C) = {} by A1,Def5;
hence thesis by A3,A2,Th56;
end;
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 Def5;
A3: now
assume
A4: B c= C;
then
A5: C = B+^(C-^B) by Def5;
A c= C by A1,A4;
then B+^(C-^B) = A+^(C-^A) by A5,Def5;
then A+^((B-^A)+^(C-^B)) = A+^(C-^A) by A2,Th30;
then (B-^A)+^(C-^B) = C-^A by Th21;
hence thesis by Th24;
end;
not B c= C implies thesis by Def5;
hence thesis by A3;
end;
theorem
A c= B implies A-^C c= B-^C
proof
assume
A1: A c= B;
A2: now
assume
A3: C c= A;
then
A4: A = C+^(A-^C) by Def5;
C c= B by A1,A3;
then C+^(A-^C) c= C+^(B-^C) by A1,A4,Def5;
hence thesis by Th23;
end;
not C c= A implies thesis by Def5;
hence thesis by A2;
end;
theorem
C <> {} & A in B+^C implies A-^B in C
proof
assume
A1: C <> {};
A2: B+^C-^B = C by Th52;
not B c= A implies A-^B = {} by Def5;
hence thesis by A1,A2,Th8,Th53;
end;
theorem
A+^B in C implies B in C-^A
proof
A1: A+^B-^A = B by Th52;
A c= A+^B by Th24;
hence thesis by A1,Th53;
end;
theorem
A c= B+^(A-^B)
proof
now
per cases;
suppose
B c= A;
hence thesis by Def5;
end;
suppose
A1: not B c= A;
then A-^B = {} by Def5;
hence thesis by A1,ORDINAL2:27;
end;
end;
hence thesis;
end;
theorem
A*^C -^ B*^C = (A-^B)*^C
proof
A1: now
assume
A2: not B c= A;
then
A3: not B*^C c= A*^C or C = {} by Th35;
A4: {}*^C = {} by ORDINAL2:35;
A5: A*^{} = {} by ORDINAL2:38;
A-^B = {} by A2,Def5;
hence thesis by A3,A5,A4,Def5,Th56;
end;
now
assume B c= A;
then A = B+^(A-^B) by Def5;
then A*^C = B*^C+^(A-^B)*^C by Th46;
hence thesis by Th52;
end;
hence thesis by A1;
end;
theorem Th64:
(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 Def6;
hence thesis by Th24;
end;
suppose
B = {};
then A div^ B = {} by Def6;
then (A div^ B)*^B = {} by ORDINAL2:35;
hence thesis;
end;
end;
hence thesis;
end;
theorem Th65:
A = (A div^ B)*^B+^(A mod^ B)
proof
(A div^ B)*^B c= A by Th64;
hence thesis by Def5;
end;
theorem
A = B*^C+^D & D in C implies B = A div^ C & D = A mod^ C
proof
assume that
A1: A = B*^C+^D and
A2: D in C;
thus B = A div^ C by A1,A2,Def6;
hence thesis by A1,Th52;
end;
theorem
A in B*^C implies A div^ C in B & A mod^ C in C
proof
A1: A = (A div^ C)*^C+^(A mod^ C) by Th65;
assume
A2: A in B*^C;
then C <> {} by ORDINAL2:38;
then
A3: ex D st A = (A div^ C)*^C+^D & D in C by Def6;
then
A4: (A div^ C)*^C c= A by Th24;
assume not thesis;
then B*^C c= (A div^ C)*^C by A3,A1,Th21,ORDINAL1:16,ORDINAL2:41;
hence contradiction by A2,A4,ORDINAL1:5;
end;
theorem Th68:
B <> {} implies A*^B div^ B = A
proof
assume B <> {};
then
A1: {} in B by Th8;
A*^B = A*^B+^{} by ORDINAL2:27;
hence thesis by A1,Def6;
end;
theorem
A*^B mod^ B = {}
proof
A1: A*^{} = {} by ORDINAL2:38;
A2: A*^B-^A*^B = {} by Th54;
{}-^(A*^B div^ B)*^B = {} by Th56;
hence thesis by A1,A2,Th68;
end;
theorem
{} div^ A = {} & {} mod^ A = {} & A mod^ {} = A
proof
A1: A = {} or A <> {};
{} = {}*^A by ORDINAL2:35;
hence {} div^ A = {} by A1,Def6,Th68;
thus {} mod^ A = {} by Th56;
thus A mod^ {} = A-^{} by ORDINAL2:38
.= A by Th56;
end;
theorem
A div^ 1 = A & A mod^ 1 = {}
proof
A1: A = A*^1 by ORDINAL2:39;
A2: A = A+^{} by ORDINAL2:27;
1 = succ 0 .= { 0 };
then
A3: {} in 1 by Th8;
hence A div^ 1 = A by A1,A2,Def6;
thus A mod^ 1 = A-^A by A1,A2,A3,Def6
.= {} by Th54;
end;
begin :: Addenda
:: from ZF_REFLE, 2007.03.13, A.T.
theorem
sup X c= succ union On X
proof
reconsider A = union On X as Ordinal by Th5;
On X c= succ A
proof
let x be object;
assume
A1: x in On X;
then reconsider a = x as Ordinal by ORDINAL1:def 9;
a c= A by A1,ZFMISC_1:74;
hence thesis by ORDINAL1:22;
end;
hence thesis by ORDINAL2:def 3;
end;
:: from ZFREFLE1, 2007.03.14, A.T.
reserve e,u for set;
theorem
succ A is_cofinal_with 1
proof
deffunc F(set) = A;
consider psi such that
A1: dom psi = 1 & for B st B in 1 holds psi.B = F(B) from ORDINAL2:sch 3;
take psi;
thus dom psi = 1 by A1;
thus rng psi c= succ A
proof
let e be object;
assume e in rng psi;
then consider u being object such that
A2: u in 1 and
A3: e = psi.u by A1,FUNCT_1:def 3;
reconsider u as Ordinal by A2;
psi.u = A by A1,A2;
hence thesis by A3,ORDINAL1:6;
end;
thus psi is increasing
by A1,Th14;
A4: psi.{} = A by A1,Lm1,ORDINAL1:6;
rng psi = {psi.{}} by A1,Lm1,FUNCT_1:4;
hence thesis by A4,ORDINAL2:23;
end;
:: from ARYTM_3, 2007.10.23, A.T.
theorem Th74:
for a,b being Ordinal st a+^b is natural holds a in omega & b in omega
by Th24,ORDINAL1:12;
registration
let a, b be natural Ordinal;
cluster a -^ b -> natural;
coherence
proof
not b c= a or b c= a;
then a -^ b = {} or a = b+^(a-^b) by Def5;
hence a-^b in omega by Th74,ORDINAL1:def 11;
end;
cluster a *^ b -> natural;
coherence
proof
defpred P[natural Ordinal] means $1*^b is natural;
A1: now
let a be natural Ordinal;
assume P[a];
then reconsider c = a*^b as natural Ordinal;
(succ a)*^b = c+^b by ORDINAL2:36;
hence P[succ a];
end;
A2: P[0] by ORDINAL2:35;
P[a] from ORDINAL2:sch 17(A2,A1);
hence thesis;
end;
end;
theorem
for a,b being Ordinal st a*^b is natural non empty holds a in omega &
b in omega
proof
let x,y be Ordinal such that
A1: x*^y in omega;
assume
A2: x*^y is non empty;
then y <> {} by ORDINAL2:38;
then
A3: x c= x*^y by Th36;
x <> {} by A2,ORDINAL2:35;
then y c= x*^y by Th36;
hence thesis by A1,A3,ORDINAL1:12;
end;
definition
let a,b be natural Ordinal;
redefine func a+^b;
commutativity
proof
let a,b be natural Ordinal;
defpred R[natural Ordinal] means a+^$1 = $1+^a;
A1: now
let b be natural Ordinal;
assume
A2: R[b];
defpred P[natural Ordinal] means (succ b)+^$1 = succ (b+^$1);
A3: now
let a be natural Ordinal;
assume
A4: P[a];
(succ b)+^succ a = succ ((succ b)+^a) by ORDINAL2:28
.= succ (b+^succ a) by A4,ORDINAL2:28;
hence P[succ a];
end;
(succ b)+^{} = succ b by ORDINAL2:27
.= succ (b+^{}) by ORDINAL2:27;
then
A5: P[0];
P[a] from ORDINAL2:sch 17(A5,A3);
hence R[succ b] by A2,ORDINAL2:28;
end;
a+^{} = a by ORDINAL2:27
.= {}+^a by ORDINAL2:30;
then
A6: R[0];
thus R[b] from ORDINAL2:sch 17(A6,A1);
end;
end;
definition
let a,b be natural Ordinal;
redefine func a*^b;
commutativity
proof
let a,b be natural Ordinal;
defpred R[natural Ordinal] means a*^$1 = $1*^a;
A1: now
let b be natural Ordinal;
defpred P[natural Ordinal] means $1*^succ b = $1*^b+^$1;
assume
A2: R[b];
A3: now
let a be natural Ordinal;
assume
A4: P[a];
(succ a)*^succ b = a*^(succ b)+^succ b by ORDINAL2:36
.= a*^b+^(a+^succ b) by A4,Th30
.= a*^b+^succ (a+^b) by ORDINAL2:28
.= succ (a*^b+^(a+^b)) by ORDINAL2:28
.= succ (a*^b+^b+^a) by Th30
.= succ ((succ a)*^b+^a) by ORDINAL2:36
.= (succ a)*^b+^succ a by ORDINAL2:28;
hence P[succ a];
end;
{}*^succ b = {} by ORDINAL2:35
.= {}+^{} by ORDINAL2:27
.= {}*^b+^{} by ORDINAL2:35;
then
A5: P[0];
P[a] from ORDINAL2:sch 17(A5,A3);
hence R[succ b] by A2,ORDINAL2:36;
end;
a*^{} = {} by ORDINAL2:38
.= {}*^a by ORDINAL2:35;
then
A6: R[0];
thus R[b] from ORDINAL2:sch 17(A6,A1);
end;
end;