:: Epsilon Numbers and Cantor Normal Form
:: by Grzegorz Bancerek
::
:: Received October 20, 2009
:: Copyright (c) 2009 Association of Mizar Users
environ
vocabularies NUMBERS, ORDINAL1, ORDINAL2, TARSKI, MATROID0, XBOOLE_0, CARD_1,
FINSET_1, AFINSQ_1, ORDINAL4, RELAT_1, FUNCT_1, VALUED_0, CARD_3,
SUBSET_1, ARYTM_3, NAT_1, XXREAL_0, NEWTON, ORDINAL3, FINSEQ_1, ORDINAL5;
notations XBOOLE_0, TARSKI, RELAT_1, FUNCT_1, SUBSET_1, FINSET_1, NUMBERS,
MATROID0, ORDINAL1, NAT_1, XCMPLX_0, XXREAL_0, NEWTON, ORDINAL2,
AFINSQ_1, ORDINAL3, ORDINAL4, CARD_3;
constructors XBOOLE_0, TARSKI, ZFMISC_1, SUBSET_1, FINSET_1, NUMBERS, NEWTON,
XCMPLX_0, ORDINAL1, NAT_1, XXREAL_0, ORDINAL2, AFINSQ_1, ORDINAL3,
CARD_3, ORDINAL4;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, NAT_1, XXREAL_0, XREAL_0,
ORDINAL2, ORDINAL4, CARD_1, CARD_5, CARD_LAR, NEWTON, XCMPLX_0, AFINSQ_1,
FINSET_1;
requirements SUBSET, BOOLE, NUMERALS, ARITHM, REAL;
definitions ORDINAL1, TARSKI, XBOOLE_0, RELAT_1, ORDINAL2, CARD_3;
theorems TARSKI, FUNCT_1, FINSET_1, NAT_1, ORDERS_1, AFINSQ_1, RELAT_1,
ORDINAL1, ORDINAL2, ORDINAL3, ORDINAL4, CARD_2, CARD_3, CARD_5, XBOOLE_0,
XBOOLE_1, ZFMISC_1, NEWTON, XXREAL_0, NAT_4, PEPIN, CARD_1;
schemes NAT_1, ORDINAL1, ORDINAL2, AFINSQ_1;
begin :: Preliminaries
reserve a,b,c,d,e for ordinal number, m,n for natural number,
f for Ordinal-Sequence,
x for set;
theorem Th001:
a c= succ b implies a c= b or a = succ b
proof assume
A0: a c= succ b;
assume a c/= b; then
A1: b in a by ORDINAL1:26;
thus a c= succ b by A0;
thus thesis by A1,ORDINAL1:33;
end;
registration
cluster omega -> limit_ordinal;
:: rezultat innych rejestracji, ale nalezy przeniesc do ORDINAL1
coherence;
cluster -> Ordinal-yielding (empty set);
coherence
proof let f be empty set;
take 0;
thus thesis;
end;
end;
registration
cluster non empty finite T-Sequence;
existence
proof
consider x;
take <%x%>;
thus thesis;
end;
end;
registration
let f be T-Sequence;
let g be non empty T-Sequence;
cluster f^g -> non empty;
coherence
proof
(dom f)+^dom g <> 0 by ORDINAL3:29; then
dom(f^g) <> 0 by ORDINAL4:def 1;
hence thesis;
end;
cluster g^f -> non empty;
coherence
proof
(dom g)+^dom f <> 0 by ORDINAL3:29; then
dom(g^f) <> 0 by ORDINAL4:def 1;
hence thesis;
end;
end;
reserve S,S1,S2 for T-Sequence;
theorem Th65:
dom S = a+^b implies ex S1,S2 st S = S1^S2 & dom S1 = a & dom S2 = b
proof assume
A0: dom S = a+^b;
set S1 = S|a;
a c= a+^b by ORDINAL3:27; then
B1: dom S1 = a by A0,RELAT_1:91;
deffunc F(Ordinal) = S.(a+^$1);
consider S2 such that
A1: dom S2 = b & for c st c in b holds S2.c = F(c) from ORDINAL2:sch 2;
take S1,S2; set s = S1^S2;
A2: dom S = dom s by A0,B1,A1,ORDINAL4:def 1;
now let x be set; assume
A3: x in dom S; then reconsider z = x as Ordinal;
per cases by A0,A3,ORDINAL3:42;
suppose
A4: z in a;
hence S.x = S1.z by FUNCT_1:72 .= s.x by A4,B1,ORDINAL4:def 1;
end;
suppose ex c st c in b & z = a+^c; then
consider c such that
A5: c in b & z = a+^c;
thus S.x = S2.c by A1,A5 .= s.x by A5,B1,A1,ORDINAL4:def 1;
end;
end;
hence thesis by B1,A1,A2,FUNCT_1:9;
end;
theorem ThS1:
rng S1 c= rng(S1^S2) & rng S2 c= rng(S1^S2)
proof
set q = S1^S2;
A0: dom q = (dom S1)+^dom S2 by ORDINAL4:def 1; then
A2: dom S1 c= dom q by ORDINAL3:27;
thus rng S1 c= rng(S1^S2)
proof
let x; assume x in rng S1; then
consider z being set such that
A1: z in dom S1 & x = S1.z by FUNCT_1:def 5;
reconsider z as Ordinal by A1;
q.z = x & z in dom q by A1,A2,ORDINAL4:def 1;
hence thesis by FUNCT_1:def 5;
end;
let x; assume x in rng S2; then
consider z being set such that
A1: z in dom S2 & x = S2.z by FUNCT_1:def 5;
reconsider z as Ordinal by A1;
q.((dom S1)+^z) = x & (dom S1)+^z in dom q
by A0,A1,ORDINAL4:def 1,ORDINAL3:20;
hence thesis by FUNCT_1:def 5;
end;
theorem ThS2:
S1^S2 is Ordinal-yielding implies
S1 is Ordinal-yielding & S2 is Ordinal-yielding
proof
given a such that
A0: rng (S1^S2) c= a;
thus S1 is Ordinal-yielding
proof
take a;
rng S1 c= rng(S1^S2) by ThS1;
hence thesis by A0,XBOOLE_1:1;
end;
take a;
rng S2 c= rng(S1^S2) by ThS1;
hence thesis by A0,XBOOLE_1:1;
end;
definition
let f be T-Sequence;
attr f is decreasing means
for a,b st a in b & b in dom f holds f.b in f.a;
attr f is non-decreasing means:
ND:
for a,b st a in b & b in dom f holds f.a c= f.b;
attr f is non-increasing means
for a,b st a in b & b in dom f holds f.b c= f.a;
end;
registration
cluster increasing -> non-decreasing Ordinal-Sequence;
coherence
proof
let f be Ordinal-Sequence such that
A1: for a,b st a in b & b in dom f holds f.a in f.b;
let a,b; f.a in f.b implies f.a c= f.b by ORDINAL1:def 2;
hence thesis by A1;
end;
cluster decreasing -> non-increasing Ordinal-Sequence;
coherence
proof
let f be Ordinal-Sequence such that
A1: for a,b st a in b & b in dom f holds f.b in f.a;
let a,b; f.b in f.a implies f.b c= f.a by ORDINAL1:def 2;
hence thesis by A1;
end;
end;
theorem ThO:
for f being T-Sequence holds f is infinite iff omega c= dom f
proof
let f be T-Sequence;
f is infinite iff dom f is infinite by FINSET_1:29;
hence thesis by CARD_3:102;
end;
registration
cluster decreasing -> finite T-Sequence;
coherence
proof
let f be T-Sequence such that
A1: for a,b st a in b & b in dom f holds f.b in f.a;
set X = f.:omega;
assume f is infinite; then
A2: 0 in omega & omega c= dom f by ThO; then
f.0 in X by FUNCT_1:def 12; then
consider x being set such that
A3: x in X & not ex y being set st y in X & y in x by TARSKI:7;
consider a being set such that
A4: a in dom f & a in omega & x = f.a by A3,FUNCT_1:def 12;
reconsider a as Ordinal by A4;
A5: succ a in omega by A4,ORDINAL1:41; then
a in succ a & succ a in dom f by A2,ORDINAL1:10; then
f.succ a in x & f.succ a in X by A1,A4,A5,FUNCT_1:def 12;
hence thesis by A3;
end;
cluster -> decreasing increasing (empty set);
coherence
proof
let e be empty set;
thus e is decreasing proof let a; thus thesis; end;
let a; thus thesis;
end;
end;
registration
let a;
cluster <%a%> -> Ordinal-yielding;
coherence
proof
take succ a;
let x; assume x in rng <%a%>; then
x in {a} by AFINSQ_1:36; then
x = a by TARSKI:def 1;
hence thesis by ORDINAL1:10;
end;
end;
registration
let a;
cluster <%a%> -> decreasing increasing;
coherence
proof set f = <%a%>;
A1: dom <%a%> = 1 & <%a%>.0 = a by AFINSQ_1:def 5;
hence for c,b st c in b & b in dom f holds f.b in f.c
by TARSKI:def 1,ORDINAL3:18;
let c,b; thus thesis by A1,TARSKI:def 1,ORDINAL3:18;
end;
end;
registration
cluster decreasing increasing non-decreasing non-increasing finite
non empty Ordinal-Sequence;
existence
proof
consider a;
take <%a%>; thus thesis;
end;
end;
theorem ThND:
for f being non-decreasing Ordinal-Sequence
st dom f is non empty holds Union f is_limes_of f
proof
let f be non-decreasing Ordinal-Sequence such that
Z0: dom f is non empty;
set a0 = the Element of dom f;
per cases;
case
Z1: Union f = {};
take a0; thus a0 in dom f by Z0;
let c; assume a0 c= c & c in dom f; then
f.c in rng f by FUNCT_1:def 5;
hence f.c = {} by Z1,ORDERS_1:91;
end;
case Union f <> {};
let b,c; assume
A1: b in Union f & Union f in c; then
consider x being set such that
A2: x in dom f & b in f.x by CARD_5:10;
reconsider x as Ordinal by A2;
take x; thus x in dom f by A2;
let E be Ordinal; assume
Z2: x c= E & E in dom f; then
x = E or x c< E by XBOOLE_0:def 8; then
x = E or x in E by ORDINAL1:21; then
f.x c= f.E by Z2,ND;
hence b in f.E by A2;
f.E in rng f by Z2,FUNCT_1:def 5; then
f.E c= Union f by ZFMISC_1:92;
hence f.E in c by A1,ORDINAL1:22;
end;
end;
theorem
a in b implies n*^exp(omega, a) in exp(omega, b)
proof
assume a in b; then
succ a c= b by ORDINAL1:33; then
A1: exp(omega, succ a) c= exp(omega, b) by ORDINAL4:27;
A2: exp(omega, succ a) = omega*^exp(omega, a) by ORDINAL2:61;
n in omega by ORDINAL1:def 13; then
n*^exp(omega, a) in omega*^exp(omega, a) by ORDINAL4:22,ORDINAL3:22;
hence thesis by A1,A2;
end;
theorem Th003:
0 in a & (for b st b in dom f holds f.b = exp(a,b)) implies
f is non-decreasing
proof assume
Z0: 0 in a & for b st b in dom f holds f.b = exp(a,b);
let b,d; assume
C1: b in d & d in dom f; then
b in dom f by ORDINAL1:19; then
b c= d & f.b = exp(a,b) & f.d = exp(a,d) by Z0,C1,ORDINAL1:def 2;
hence thesis by Z0,ORDINAL4:27;
end;
theorem Th002:
a is limit_ordinal & 0 in b implies exp(a,b) is limit_ordinal
proof assume
A0: a is limit_ordinal & 0 in b;
per cases by ORDINAL3:10;
suppose a = 0;
hence thesis by A0,ORDINAL4:20;
end;
suppose
0A: 0 in a;
defpred P[Ordinal] means 0 in $1 implies exp(a,$1) is limit_ordinal;
A1: P[{}];
A2: P[c] implies P[succ c]
proof
exp(a, succ c) = a*^exp(a,c) by ORDINAL2:61;
hence thesis by A0,ORDINAL3:48;
end;
A3: c <> {} & c is limit_ordinal & (for b st b in c holds P[b]) implies P[c]
proof assume that
Z0: c <> {} & c is limit_ordinal and
Z1: for b st b in c holds P[b];
deffunc F(Ordinal) = exp(a,$1);
consider f such that
B1: dom f = c & for b st b in c holds f.b = F(b) from ORDINAL2:sch 3;
B2: exp(a,c) = lim f by Z0,B1,ORDINAL2:62;
f is non-decreasing by 0A,B1,Th003; then
Union f is_limes_of f by Z0,B1,ThND; then
B3: exp(a,c) = Union f by B2,ORDINAL2:def 14;
for d st d in exp(a,c) holds succ d in exp(a,c)
proof let d; assume d in exp(a,c); then
consider b being set such that
B4: b in dom f & d in f.b by B3,CARD_5:10;
reconsider b as Ordinal by B4;
B5: succ b in dom f by Z0,B1,B4,ORDINAL1:41; then
B6: f.b = F(b) & f.succ b = F(succ b) & P[succ b] by Z1,B1,B4;
F(b) c= F(succ b) by 0A,ORDINAL4:27,ORDINAL3:1; then
succ d in f.succ b by B6,ORDINAL1:41,B4,ORDINAL3:10;
hence succ d in exp(a,c) by B3,B5,CARD_5:10;
end;
hence P[c] by ORDINAL1:41;
end;
P[c] from ORDINAL2:sch 1(A1,A2,A3);
hence thesis by A0;
end;
end;
theorem
1 in a & (for b st b in dom f holds f.b = exp(a,b)) implies f is increasing
proof assume
Z0: 1 in a & for b st b in dom f holds f.b = exp(a,b);
let b,d; assume
C1: b in d & d in dom f; then
f.b = exp(a,b) & f.d = exp(a,d) by Z0,ORDINAL1:19;
hence thesis by Z0,C1,ORDINAL4:24;
end;
theorem Th005:
0 in a & b is non empty limit_ordinal implies
(x in exp(a,b) iff ex c st c in b & x in exp(a,c))
proof assume
Z0: 0 in a & b is non empty limit_ordinal;
deffunc F(Ordinal) = exp(a,$1);
consider f such that
Z1: dom f = b & for c st c in b holds f.c = F(c) from ORDINAL2:sch 3;
f is non-decreasing by Z0,Z1,Th003; then
Union f is_limes_of f by Z0,Z1,ThND; then
Z2: Union f = lim f by ORDINAL2:def 14 .= exp(a,b) by Z0,Z1,ORDINAL2:62;
hereby assume x in exp(a,b); then
consider c being set such that
Z4: c in dom f & x in f.c by Z2,CARD_5:10;
reconsider c as Ordinal by Z4;
take c;
thus c in b by Z1,Z4;
thus x in exp(a,c) by Z1,Z4;
end;
given c such that
A1: c in b & x in exp(a,c);
f.c = F(c) by Z1,A1;
hence x in exp(a,b) by Z1,Z2,A1,CARD_5:10;
end;
theorem Th006:
0 in a & exp(a,b) in exp(a,c) implies b in c
proof assume
A0: 0 in a & exp(a,b) in exp(a,c);
assume not b in c; then
exp(a,c) c= exp(a,b) by A0,ORDINAL4:27,ORDINAL1:26; then
exp(a,b) in exp(a,b) by A0;
hence thesis;
end;
begin :: Tetration (Knuth's arrow notation) of ordinals
definition
let a,b be Ordinal;
func a|^|^b -> Ordinal means:
KNUTH:
ex phi being Ordinal-Sequence st it = last phi & dom phi = succ b &
phi.{} = 1 &
(for c being Ordinal st succ c in succ b holds phi.succ c = exp(a,phi.c))&
for c being Ordinal st c in succ b & c <> {} & c is limit_ordinal
holds phi.c = lim(phi|c);
correctness
proof
deffunc C(Ordinal,Ordinal) = exp(a,$2);
deffunc D(Ordinal,Ordinal-Sequence) = lim $2;
(ex F being Ordinal,fi being Ordinal-Sequence
st F = last fi & dom fi = succ b & fi.{} = 1 &
(for c being Ordinal st succ c in succ b holds fi.succ c = C(c,fi.c)) &
for c being Ordinal st c in succ b & c <> {} & c is limit_ordinal
holds fi.c = D(c,fi|c) ) & for A1,A2 being Ordinal st
(ex fi being Ordinal-Sequence
st A1 = last fi & dom fi = succ b & fi.{} = 1 &
(for C being Ordinal st succ C in succ b holds fi.succ C = C(C,fi.C)) &
for C being Ordinal st C in succ b & C <> {} & C is limit_ordinal
holds fi.C = D(C,fi|C) ) &
(ex fi being Ordinal-Sequence
st A2 = last fi & dom fi = succ b & fi.{} = 1 &
(for C being Ordinal st succ C in succ b holds fi.succ C = C(C,fi.C)) &
for C being Ordinal st C in succ b & C <> {} & C is limit_ordinal
holds fi.C = D(C,fi|C) ) holds A1 = A2 from ORDINAL2:sch 13;
hence thesis;
end;
end;
theorem Th0:
a |^|^ 0 = 1
proof
deffunc F(Ordinal) = a|^|^$1;
deffunc D(Ordinal,Ordinal-Sequence) = lim $2;
deffunc C(Ordinal,Ordinal) = exp(a,$2);
A1: for b,c holds c = F(b) iff
ex fi being Ordinal-Sequence st c = last fi & dom fi = succ b &
fi.{} = 1 & (for c st succ c in succ b holds fi.succ c = C(c,fi.c)) &
for c st c in succ b & c <> {} & c is limit_ordinal
holds fi.c = D(c,fi|c) by KNUTH;
thus F({}) = 1 from ORDINAL2:sch 14(A1);
end;
theorem Th1:
a |^|^ succ b = exp(a, a|^|^b)
proof
deffunc F(Ordinal) = a|^|^$1;
deffunc D(Ordinal,Ordinal-Sequence) = lim $2;
deffunc C(Ordinal,Ordinal) = exp(a, $2);
A1: for b,c holds c = F(b) iff
ex fi being Ordinal-Sequence st c = last fi & dom fi = succ b &
fi.{} = 1 & (for c st succ c in succ b holds fi.succ c = C(c,fi.c)) &
for c st c in succ b & c <> {} & c is limit_ordinal
holds fi.c = D(c,fi|c) by KNUTH;
for b holds F(succ b) = C(b,F(b)) from ORDINAL2:sch 15(A1);
hence thesis;
end;
theorem Th2:
b <> {} & b is limit_ordinal implies
for phi being Ordinal-Sequence st dom phi = b &
for c st c in b holds phi.c = a |^|^ c
holds a |^|^ b = lim phi
proof
assume
A1: b <> {} & b is limit_ordinal;
deffunc F(Ordinal) = a |^|^ $1;
deffunc D(Ordinal,Ordinal-Sequence) = lim $2;
deffunc C(Ordinal,Ordinal) = exp(a,$2);
let fi being Ordinal-Sequence such that
A2: dom fi = b and
A3: for c st c in b holds fi.c = F(c);
A4: for b,c holds c = F(b) iff
ex fi being Ordinal-Sequence st c = last fi & dom fi = succ b &
fi.{} = 1 & (for c st succ c in succ b holds fi.succ c = C(c,fi.c)) &
for c st c in succ b & c <> {} & c is limit_ordinal
holds fi.c = D(c,fi|c) by KNUTH;
thus F(b) = D(b,fi) from ORDINAL2:sch 16(A4,A1,A2,A3);
end;
theorem Th3:
a |^|^ 1 = a
proof
0+1 = succ 0;
hence a |^|^ 1 = exp(a, a|^|^0) by Th1 .= exp(a, 1) by Th0
.= a by ORDINAL2:63;
end;
theorem Th4:
1 |^|^ a = 1
proof
defpred P[Ordinal] means 1 |^|^ $1 = 1;
A1: P[{}] by Th0;
A2: for a st P[a] holds P[succ a]
proof
let A be Ordinal;
assume P[A];
hence 1 |^|^ succ A = exp(1,1) by Th1
.= 1 by ORDINAL2:63;
end;
A3: for A being Ordinal st A <> {} & A is limit_ordinal &
for B being Ordinal st B in A holds P[B] holds P[A]
proof
let A be Ordinal such that
A4: A <> {} & A is limit_ordinal and
A5: for B being Ordinal st B in A holds 1|^|^B = 1;
deffunc F(Ordinal) = 1 |^|^ $1;
consider fi being Ordinal-Sequence such that
A6: dom fi = A & for B being Ordinal st B in A holds fi.B = F(B)
from ORDINAL2:sch 3;
A7: 1 |^|^ A = lim fi by A4,A6,Th2;
A8: rng fi c= { 1 }
proof
let x being set;
assume x in rng fi; then
consider y being set such that
A9: y in dom fi & x = fi.y by FUNCT_1:def 5;
reconsider y as Ordinal by A9;
x = 1 |^|^ y by A6,A9
.= 1 by A5,A6,A9;
hence x in { 1 } by TARSKI:def 1;
end;
now
thus {} <> 1;
let b,c such that
A10: b in 1 & 1 in c;
consider x being Element of A;
reconsider x as Ordinal;
take D = x; thus D in dom fi by A4,A6;
let E be Ordinal;
assume D c= E & E in dom fi; then
fi.E in rng fi by FUNCT_1:def 5;
hence b in fi.E & fi.E in c by A8,A10,TARSKI:def 1;
end; then
1 is_limes_of fi by ORDINAL2:def 13;
hence 1 |^|^ A = 1 by A7,ORDINAL2:def 14;
end;
for a holds P[a] from ORDINAL2:sch 1(A1,A2,A3);
hence thesis;
end;
theorem Th3':
a |^|^ 2 = exp(a, a)
proof
2 = succ 1;
hence a |^|^ 2 = exp(a, a|^|^1) by Th1 .= exp(a, a) by Th3;
end;
theorem
a |^|^ 3 = exp(a,exp(a, a))
proof
3 = succ 2;
hence a |^|^ 3 = exp(a, a|^|^2) by Th1 .= exp(a,exp(a, a)) by Th3';
end;
theorem
for n being natural number holds
0 |^|^ (2*n) = 1 & 0 |^|^ (2*n+1) = 0
proof
defpred P[Nat] means 0 |^|^ (2*$1) = 1 & 0 |^|^ (2*$1+1) = 0;
A1: P[0] by Th0,Th3;
A2: now
let n be Nat; assume
A3: P[n];
thus P[n+1]
proof
thus
A4: 0 |^|^ (2*(n+1)) = 0 |^|^ (2*n+1+1)
.= 0 |^|^ succ (2*n+1) by NAT_1:def 2
.= exp(0, 0) by A3,Th1
.= 1 by ORDINAL2:60;
thus 0 |^|^ (2*(n+1)+1) = 0 |^|^ succ (2*(n+1)) by NAT_1:def 2
.= exp(0, 1) by A4,Th1 .= 0 by ORDINAL2:63;
end;
end;
thus for n being Nat holds P[n] from NAT_1:sch 2(A1,A2);
end;
theorem Th5:
a c= b & 0 in c implies c |^|^ a c= c |^|^ b
proof assume that
A1: a c= b and
A2: 0 in c;
succ 0 c= c & succ 0 = 0+1 by A2,ORDINAL1:33; then
AA: 1 c< c or 1 = c by XBOOLE_0:def 8;
per cases by AA,ORDINAL1:21;
suppose c = 1; then
c |^|^ a = 1 & c |^|^ b = 1 by Th4;
hence thesis;
end;
suppose
A0: 1 in c;
defpred H[Ordinal] means
for a,b st a c= b & b c= $1 holds c |^|^ a c= c |^|^ b;
P0: H[{}]
proof let a,b;
assume
B0: a c= b & b c= {}; then
b = {} by XBOOLE_1:3;
hence thesis by B0,XBOOLE_1:3;
end;
P1: now let d such that
A3: H[d];
c |^|^ (succ d) = exp(c, c |^|^ d) by Th1; then
A6: c |^|^ d c= c |^|^ (succ d) by A0,ORDINAL4:32;
thus H[succ d]
proof let a,b such that
A4: a c= b & b c= succ d;
A5: a c= succ d by A4,XBOOLE_1:1;
per cases by A4,A5,Th001;
suppose b c= d;
hence thesis by A3,A4;
end;
suppose b = succ d & a = succ d;
hence thesis;
end;
suppose
A7: b = succ d & a c= d; then
c |^|^ a c= c |^|^ d by A3;
hence thesis by A6,A7,XBOOLE_1:1;
end;
end;
end;
P2: now let d such that
B1: d <> {} & d is limit_ordinal and
B2: for e st e in d holds H[e];
deffunc E(Ordinal) = c|^|^$1;
consider f being Ordinal-Sequence such that
B3: dom f = d & for e st e in d holds f.e = E(e) from ORDINAL2:sch 3;
f is non-decreasing
proof let a,b; assume
C0: a in b & b in dom f; then
a c= b & H[b] by B2,B3,ORDINAL1:def 2; then
c |^|^ a c= c |^|^ b & a in d & f.b = E(b) by B3,C0,ORDINAL1:22;
hence thesis by B3;
end; then
B4: Union f is_limes_of f by B1,B3,ThND;
c|^|^d = lim f by B1,B3,Th2; then
B5: c|^|^d = Union f by B4,ORDINAL2:def 14;
thus H[d]
proof
let a,b; assume
C1: a c= b & b c= d; then
C2: (b c< d or b = d) & (a c< b or a = b) by XBOOLE_0:def 8;
per cases by C2,ORDINAL1:21;
suppose b in d;
hence E(a) c= E(b) by C1,B2;
end;
suppose
C3: b = d & a in d; then
f.a in rng f & f.a = E(a) by B3,FUNCT_1:def 5;
hence E(a) c= E(b) by B5,C3,ZFMISC_1:92;
end;
suppose b = d & a = d;
hence E(a) c= E(b);
end;
end;
end;
for b holds H[b] from ORDINAL2:sch 1(P0,P1,P2);
hence thesis by A1;
end;
end;
theorem
0 in a & (for b st b in dom f holds f.b = a|^|^b)
implies f is non-decreasing
proof assume that
Z0: 0 in a and
Z1: for b st b in dom f holds f.b = a|^|^b;
let b,c; assume
Z2: b in c & c in dom f; then
b c= c by ORDINAL1:def 2; then
a|^|^b c= a|^|^c & a|^|^c = f.c by Z0,Z1,Z2,Th5;
hence f.b c= f.c by Z1,Z2,ORDINAL1:19;
end;
theorem Th6:
0 in a & 0 in b implies a c= a |^|^ b
proof assume
A0: 0 in a & 0 in b;
defpred J[Ordinal] means 0 in $1 implies a c= a |^|^ $1;
A1: J[0];
A2: now let b; assume
B1: J[b];
B2: a |^|^ succ b = exp(a, a |^|^ b) by Th1;
B4: succ 0 = 0+1;
thus J[succ b]
proof
per cases by ORDINAL3:10;
suppose 0 in b; then
1 c= a |^|^ b by B4,ORDINAL1:33,A0,B1; then
exp(a, 1) c= exp(a, a |^|^ b) by A0,ORDINAL4:27;
hence thesis by B2,ORDINAL2:63;
end;
suppose
b = 0; then
a |^|^ b = 1 by Th0;
hence thesis by B2,ORDINAL2:63;
end;
end;
end;
A3: now let c such that
C1: c <> {} & c is limit_ordinal & for b st b in c holds J[b];
deffunc F(Ordinal) = a |^|^ $1;
consider phi being Ordinal-Sequence such that
C2: dom phi = c & for b st b in c holds phi.b = F(b) from ORDINAL2:sch 3;
phi is non-decreasing
proof
let e,b; assume
D1: e in b & b in dom phi; then
D2: phi.b = F(b) & e in c by C2,ORDINAL1:19; then
phi.e = F(e) & e c= b by C2,D1,ORDINAL1:def 2;
hence thesis by A0,D2,Th5;
end; then
C3: Union phi is_limes_of phi by C1,C2,ThND;
lim phi = F(c) by C1,C2,Th2; then
C4: F(c) = Union phi by C3,ORDINAL2:def 14;
thus J[c]
proof
assume 0 in c; then
succ 0 in c by C1,ORDINAL1:41; then
phi.1 in rng phi & phi.1 = F(1) & F(1) = a by C2,Th3,FUNCT_1:def 5;
hence thesis by C4,ZFMISC_1:92;
end;
end;
for b holds J[b] from ORDINAL2:sch 1(A1,A2,A3);
hence thesis by A0;
end;
theorem Th7:
1 in a & m < n implies a |^|^ m in a |^|^ n
proof assume
A0: 1 in a & m < n; then m+1 <= n by NAT_1:13; then
consider k being Nat such that
A1: n = m+1+k by NAT_1:10;
defpred Q[Nat] means a|^|^$1 in a|^|^($1+1);
defpred P[Nat] means a |^|^ m in a |^|^ (m+1+$1);
a|^|^0 = 1 by Th0; then
B0: Q[0] by A0,Th3;
B1: now let n; assume Q[n]; then
B2: exp(a, a|^|^n) in exp(a, a|^|^(n+1)) by A0,ORDINAL4:24;
succ n = n+1 & succ (n+1) = n+1+1 by NAT_1:39; then
a|^|^(n+1) = exp(a, a|^|^n) & a|^|^((n+1)+1) = exp(a, a|^|^(n+1)) by Th1;
hence Q[n+1] by B2;
end;
BB: for n holds Q[n] from NAT_1:sch 2(B0,B1); then
A2: P[0];
A3: now let k be Nat; assume
A4: P[k];
a|^|^(m+1+k) in a|^|^((m+1+k)+1) by BB;
hence P[k+1] by A4,ORDINAL1:19;
end;
for k being Nat holds P[k] from NAT_1:sch 2(A2,A3);
hence thesis by A1;
end;
:: theorem :: false a |^|^ succ omega = a |^|^ omega for a > 0
:: 1 in c & a in b implies c |^|^ a in c |^|^ b
theorem Th8:
1 in a & dom f c= omega & (for b st b in dom f holds f.b = a|^|^b)
implies f is increasing
proof assume that
Z0: 1 in a and
Z1: dom f c= omega and
Z2: for n being Ordinal st n in dom f holds f.n = a|^|^n;
let b,c; assume
Z3: b in c & c in dom f; then
Z4: b in dom f by ORDINAL1:19; then
reconsider b,c as Element of omega by Z1,Z3;
f.b = a|^|^b & f.c = a|^|^c & b < c by Z2,Z3,Z4,NAT_1:45;
hence thesis by Z0,Th7;
end;
theorem Th9:
1 in a & 1 in b implies a in a |^|^ b
proof assume
Z0: 1 in a;
assume 1 in b; then
succ 1 c= b by ORDINAL1:33; then
Z1: 2 c= b;
0 in 1 by NAT_1:45; then
Z2: 0 in a by Z0,ORDINAL1:19;
a|^|^1 in a|^|^2 & a|^|^2 c= a|^|^b by Z0,Z1,Z2,Th5,Th7; then
a|^|^1 in a|^|^b;
hence a in a |^|^ b by Th3;
end;
theorem LemExp:
for n,k being Nat holds exp(n,k) = n|^k
proof let n be Nat;
defpred P[Nat] means exp(n,$1) = n|^$1;
exp(n,0) = 1 by ORDINAL2:60; then
A0: P[0] by NEWTON:9;
A1: now
let k be Nat such that
A2: P[k];
reconsider n' = n, nk = n|^k as Element of NAT by ORDINAL1:def 13;
k+1 = succ k by NAT_1:39; then
exp(n,k+1) = n *^ exp(n,k) by ORDINAL2:61 .= n' * nk by A2,CARD_2:50;
hence P[k+1] by NEWTON:11;
end;
thus for k being Nat holds P[k] from NAT_1:sch 2(A0,A1);
end;
registration
let n,k be Nat;
cluster exp(n,k) -> natural;
coherence
proof
exp(n,k) = n|^k by LemExp;
hence thesis;
end;
end;
registration
let n,k be Nat;
cluster n |^|^ k -> natural;
coherence
proof
defpred O[Nat] means n |^|^ $1 is natural;
A0: O[0] by Th0;
A1: now let k be Nat;
assume O[k]; then
reconsider nk = n|^|^k as natural number;
k+1 = succ k by NAT_1:39; then
n|^|^(k+1) = exp(n, nk) by Th1;
hence O[k+1];
end;
for k being Nat holds O[k] from NAT_1:sch 2(A0,A1);
hence thesis;
end;
end;
theorem ThA1:
for n,k being Nat st n > 1 holds n |^|^ k > k
proof
let n,k be Nat such that
A0: n > 1;
defpred H[Nat] means n |^|^ $1 > $1;
A1: H[0] by Th0;
A2: now
let k be Nat such that
A3: H[k];
succ k = k+1 by NAT_1:39; then
n |^|^ (k+1) = exp(n, n |^|^ k) by Th1 .= n |^ (n |^|^ k) by LemExp; then
A4: n |^|^ (k+1) > n |^ k by A0,A3,PEPIN:71;
n |^ k > k by A0,NAT_4:3; then
n |^ k >= k+1 by NAT_1:13;
hence H[k+1] by A4,XXREAL_0:2;
end;
for k being Nat holds H[k] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
theorem
for n being Nat st n > 1 holds n |^|^ omega = omega
proof
let n be Nat such that
Z0: n > 1;
deffunc F(Ordinal) = n |^|^ $1;
consider phi being Ordinal-Sequence such that
A1: dom phi = omega & for b st b in omega holds phi.b = F(b)
from ORDINAL2:sch 3;
AA: rng phi c= omega
proof
let x be set; assume x in rng phi; then
consider a being set such that
B1: a in dom phi & x = phi.a by FUNCT_1:def 5;
reconsider a as Element of omega by A1,B1;
x = n |^|^ a by A1,B1;
hence thesis by ORDINAL1:def 13;
end;
A2: n |^|^ omega = lim phi by A1,Th2;
now
thus {} <> omega;
let b,c such that
A3: b in omega & omega in c;
reconsider x = b as Element of omega by A3;
take D = n |^|^ x; thus D in dom phi by A1,ORDINAL1:def 13;
x < D by Z0,ThA1; then
A4: b in D by NAT_1:45;
let E be Ordinal;
assume
A5: D c= E & E in dom phi; then
reconsider e = E as Element of omega by A1;
x < e & e < n |^|^ e by Z0,ThA1,NAT_1:45,A4,A5; then
A6: x < n |^|^ e & phi.e = F(e) by A1,XXREAL_0:2;
phi.E in rng phi by A5,FUNCT_1:def 5;
hence b in phi.E & phi.E in c by A3,A6,ORDINAL1:19,NAT_1:45,AA;
end; then
omega is_limes_of phi by ORDINAL2:def 13;
hence n |^|^ omega = omega by A2,ORDINAL2:def 14;
end;
theorem Th11:
1 in a implies a |^|^ omega is limit_ordinal
proof assume
Z0: 1 in a;
deffunc F(Ordinal) = a |^|^ $1;
consider phi being Ordinal-Sequence such that
A1: dom phi = omega & for b st b in omega holds phi.b = F(b)
from ORDINAL2:sch 3;
phi is increasing
proof
let b,c; assume
A3: b in c & c in dom phi; then
reconsider b,c as Element of NAT by A1,ORDINAL1:19;
b < c by A3,NAT_1:45; then
phi.b = F(b) & F(b) in F(c) by Z0,A1,Th7;
hence thesis by A1;
end; then
lim phi = sup phi & sup phi is limit_ordinal by A1,ORDINAL4:8,16;
hence thesis by A1,Th2;
end;
theorem Th12:
0 in a implies exp(a, a |^|^ omega) = a |^|^ omega
proof assume 0 in a; then
1 = succ 0 & succ 0 c= a by ORDINAL1:33; then
A0: 1 = a or 1 c< a by XBOOLE_0:def 8;
per cases by A0,ORDINAL1:21;
suppose
A1: a = 1;
hence exp(a, a |^|^ omega) = 1 by ORDINAL2:63 .= a |^|^ omega by A1,Th4;
end;
suppose
A2: 1 in a;
deffunc T(Ordinal) = a|^|^$1;
deffunc E(Ordinal) = exp(a, $1);
consider T being Ordinal-Sequence such that
A4: dom T = omega & for a st a in omega holds T.a = T(a) from ORDINAL2:sch 3;
consider E being Ordinal-Sequence such that
A5: dom E = a|^|^omega & for b st b in a|^|^omega holds E.b = E(b)
from ORDINAL2:sch 3;
0 in 1 by NAT_1:45; then
0 in a & 0 in omega by A2,ORDINAL1:19; then
a c= a|^|^omega by Th6; then
A6: a|^|^omega is non empty limit_ordinal by A2,Th11;
E is increasing Ordinal-Sequence by A2,A5,ORDINAL4:25; then
lim E = exp(a, a|^|^omega) & Union E is_limes_of E
by A5,A6,ThND,ORDINAL2:62; then
A7: exp(a, a|^|^omega) = Union E by ORDINAL2:def 14;
T is increasing Ordinal-Sequence by A2,A4,Th8; then
lim T = a|^|^omega & Union T is_limes_of T by A4,Th2,ThND; then
A8: a|^|^omega = Union T by ORDINAL2:def 14;
thus exp(a, a |^|^ omega) c= a |^|^ omega
proof
let x be set; assume x in exp(a, a |^|^ omega); then
consider b being set such that
B1: b in dom E & x in E.b by A7,CARD_5:10;
consider c being set such that
B2: c in dom T & b in T.c by A5,A8,B1,CARD_5:10;
reconsider b as Ordinal by B1;
reconsider c as Element of omega by A4,B2;
B3: exp(a, b) in exp(a, T.c) by A2,B2,ORDINAL4:24;
B4: succ c in omega by ORDINAL1:41; then
E.b = E(b) & T.c = T(c) & T.succ c = T(succ c) by B1,A4,A5; then
E.b in T.(succ c) by B3,Th1; then
x in T.(succ c) by B1,ORDINAL1:19;
hence thesis by A4,A8,B4,CARD_5:10;
end;
thus a |^|^ omega c= exp(a, a |^|^ omega) by A2,ORDINAL4:32;
end;
end;
theorem
0 in a & omega c= b implies a |^|^ b = a |^|^ omega
proof assume
Z0: 0 in a;
assume omega c= b; then
Z1: b = omega+^(b-^omega) by ORDINAL3:def 6;
defpred P[Ordinal] means a |^|^ (omega+^$1) = a |^|^ omega;
A0: P[{}] by ORDINAL2:44;
A1: P[c] implies P[succ c]
proof
assume P[c]; then
B1: exp(a, a |^|^ (omega+^c)) = a |^|^ omega by Z0,Th12;
thus a |^|^ (omega+^succ c) = a |^|^ succ (omega+^c) by ORDINAL2:45
.= a |^|^ omega by B1,Th1;
end;
A2: c <> {} & c is limit_ordinal & (for b st b in c holds P[b]) implies P[c]
proof assume
Z2: c <> {} & c is limit_ordinal;
assume
Z3: for b st b in c holds P[b];
deffunc F(Ordinal) = a |^|^ $1;
consider f such that
A3: dom f = omega+^c & for b st b in omega+^c holds f.b = F(b)
from ORDINAL2:sch 3;
omega+^c <> {} & omega+^c is limit_ordinal by Z2,ORDINAL3:29,32; then
A5: a|^|^(omega+^c) = lim f by A3,Th2;
now a c= a|^|^omega by Z0,Th6;
hence a|^|^omega <> {} by Z0;
let B,C be Ordinal;
assume
A7: B in a|^|^omega & a|^|^omega in C;
take D = omega;
omega+^({} qua Ordinal) = omega & {} in c
by Z2,ORDINAL2:44,ORDINAL3:10;
hence D in dom f by A3,ORDINAL2:49;
let E be Ordinal;
assume
A6: D c= E & E in dom f; then
E-^D in (omega+^c)-^omega by A3,ORDINAL3:66; then
E-^D in c by ORDINAL3:65; then
P[E-^D] by Z3; then
a|^|^omega = a|^|^E by A6,ORDINAL3:def 6;
hence B in f.E & f.E in C by A3,A7,A6;
end; then
a|^|^omega is_limes_of f by ORDINAL2:def 13;
hence P[c] by A5,ORDINAL2:def 14;
end;
P[c] from ORDINAL2:sch 1(A0,A1,A2);
hence a |^|^ b = a |^|^ omega by Z1;
end;
begin :: Critical numbers
Lm1: {} in omega by ORDINAL1:def 12;
scheme CriticalNumber2
{a() -> Ordinal, f() -> Ordinal-Sequence, phi(Ordinal) -> Ordinal}:
a() c= Union f() & phi(Union f()) = Union f() &
for b st a() c= b & phi(b) = b holds Union f() c= b
provided
A1: for a,b st a in b holds phi(a) in phi(b)
and
A2: for a st a is non empty limit_ordinal
for phi being Ordinal-Sequence
st dom phi = a & for b st b in a holds phi.b = phi(b)
holds phi(a) is_limes_of phi
and
F1: dom f() = omega & f().0 = a()
and
F2: for a st a in omega holds f().(succ a) = phi(f().a)
proof
F0: a() in rng f() by F1,FUNCT_1:def 5;
hence a() c= Union f() by ZFMISC_1:92;
set phi = f();
A7: now :: a c= phi(a)
defpred P[Ordinal] means not $1 c= phi($1);
assume
A8: ex a st P[a];
consider a such that
A9: P[a] and
A10: for b st P[b] holds a c= b from ORDINAL1:sch 1(A8);
phi(phi(a)) in phi(a) by A1,A9,ORDINAL1:26; then
not phi(a) c= phi(phi(a)) by ORDINAL1:7;
hence contradiction by A9,A10;
end; then
a() c= phi(a()); then
F3: a() c< phi(a()) or a() = phi(a()) by XBOOLE_0:def 8;
per cases by F3,ORDINAL1:21;
suppose
A3: phi(a()) = a();
A4: for a be set st a in omega holds f().a = a()
proof
let a be set; assume a in omega; then
reconsider a as Element of omega;
defpred P[Nat] means f().$1 = a();
C0: P[0] by F1;
C1: now let n be Nat; assume
C2: P[n];
n in omega by ORDINAL1:def 13; then
f().succ n = phi(a()) by F2,C2;
hence P[n+1] by A3,NAT_1:39;
end;
for n being Nat holds P[n] from NAT_1:sch 2(C0,C1); then
P[a];
hence thesis;
end;
rng f() = {a()}
proof
thus rng f() c= {a()}
proof
let x be set; assume x in rng f(); then
consider a being set such that
G1: a in dom f() & x = f().a by FUNCT_1:def 5;
x = a() by A4,G1,F1;
hence thesis by TARSKI:def 1;
end;
thus thesis by F0,ZFMISC_1:37;
end; then
Union f() = a() by ZFMISC_1:31;
hence phi(Union f()) = Union f() &
for b st a() c= b & phi(b) = b holds Union f() c= b by A3;
end;
suppose
A3: a() in phi(a());
deffunc F(Ordinal,Ordinal) = phi($2);
deffunc G(Ordinal,T-Sequence) = {};
A6: now let a such that
G1: succ a in omega;
a in succ a by ORDINAL1:10;
hence phi.(succ a) = F(a,phi.a) by F2,G1,ORDINAL1:19;
end;
B1: for a st a in omega holds a() c= phi.a & phi.a in phi.succ a
proof let a; assume a in omega; then
reconsider a as Element of omega;
defpred N[Nat] means a() c= phi.$1 & phi.$1 in phi.succ $1;
B01: N[0] by A3,F1,F2;
B02: now
let n be Nat; assume
B03: N[n];
B04: n+1 = succ n & n+1+1 = succ (n+1) &
n+1 in omega & n+1+1 in omega by ORDINAL1:def 13,NAT_1:39; then
phi.(n+1) = phi(phi.n) & phi.(n+1+1) = phi(phi.(n+1)) by A6; then
phi.n c= phi.(n+1) & phi.(n+1) in phi.(n+1+1) by A1,A7,B03,B04;
hence N[n+1] by B03,B04,XBOOLE_1:1;
end;
for n being Nat holds N[n] from NAT_1:sch 2(B01,B02); then
N[a];
hence thesis;
end;
deffunc phi(Ordinal) = phi($1);
consider fi being Ordinal-Sequence such that
A23: dom fi = Union phi & for a st a in Union phi holds fi.a = phi(a)
from ORDINAL2:sch 3;
1 = succ 0; then
f().1 = phi(a()) by F1,F2; then
phi(a()) in rng phi by F1,FUNCT_1:def 5; then
phi(a()) c= Union phi by ZFMISC_1:92; then
A24: Union phi <> {} by A3;
now
let c; assume c in Union phi; then
consider x being set such that
V1: x in dom phi & c in phi.x by CARD_5:10;
reconsider x as Element of omega by F1,V1;
succ c c= phi.x & phi.x in phi.succ x by B1,V1,ORDINAL1:33; then
succ c in phi.succ x & succ x in omega by ORDINAL1:22,def 13;
hence succ c in Union phi by F1,CARD_5:10;
end; then
A24': Union phi is limit_ordinal by ORDINAL1:41; then
A25: phi(Union phi) is_limes_of fi by A2,A23,A24;
fi is increasing
proof
let a,b;
assume
A26: a in b & b in dom fi; then
fi.a = phi(a) & fi.b = phi(b) by A23,ORDINAL1:19;
hence thesis by A1,A26;
end; then
A27: sup fi = lim fi by A23,A24,A24',ORDINAL4:8
.= phi(Union phi) by A25,ORDINAL2:def 14;
thus phi(Union phi) c= Union phi
proof
let x be set;
assume
A28: x in phi(Union phi); then
reconsider A = x as Ordinal;
consider b such that
A29: b in rng fi & A c= b by A27,A28,ORDINAL2:29;
consider y being set such that
A30: y in dom fi & b = fi.y by A29,FUNCT_1:def 5;
reconsider y as Ordinal by A30;
consider z being set such that
A32: z in dom phi & y in phi.z by A23,A30,CARD_5:10;
reconsider z as Ordinal by A32;
set c = phi.z;
succ z in omega by F1,A32,ORDINAL1:41; then
A33: phi.succ z = phi(c) & phi.succ z in rng phi & b = phi(y)
by F1,A6,A23,A30,FUNCT_1:def 5;
b in phi(c) & phi(c) c= Union phi by A33,ZFMISC_1:92,A1,A32;
hence thesis by A29,ORDINAL1:22;
end;
thus Union f() c= phi(Union f()) by A7;
let b; assume
Z1: a() c= b & phi(b) = b;
rng f() c= b
proof
let x be set; assume x in rng f(); then
consider a being set such that
Z2: a in dom f() & x = f().a by FUNCT_1:def 5;
reconsider a as Element of omega by F1,Z2;
defpred P[Nat] means f().$1 in b;
a() <> b by A3,Z1; then
a() c< b by Z1,XBOOLE_0:def 8; then
Z3: P[0] by F1,ORDINAL1:21;
Z4: now let n be Nat; assume P[n]; then
phi(f().n) in b & n in omega by A1,Z1,ORDINAL1:def 13; then
f().succ n in b by F2;
hence P[n+1] by NAT_1:39;
end;
for n being Nat holds P[n] from NAT_1:sch 2(Z3,Z4); then
P[a];
hence thesis by Z2;
end; then
Union f() c= union b & union b c= b by ZFMISC_1:95,ORDINAL2:5;
hence Union f() c= b by XBOOLE_1:1;
end;
end;
scheme CriticalNumber3{a() -> Ordinal, phi(Ordinal) -> Ordinal}:
ex a st a() in a & phi(a) = a
provided
A1: for a,b st a in b holds phi(a) in phi(b)
and
A2: for a st a is non empty limit_ordinal
for phi being Ordinal-Sequence
st dom phi = a & for b st b in a holds phi.b = phi(b)
holds phi(a) is_limes_of phi
proof assume
A3: not thesis;
deffunc F(Ordinal,Ordinal) = phi($2);
deffunc G(Ordinal,T-Sequence) = {};
consider phi being Ordinal-Sequence such that
A4: dom phi = omega and
A5: {} in omega implies phi.{} = succ a() and
A6: for a st succ a in omega holds phi.(succ a) = F(a,phi.a) and
for a st a in omega & a <> {} & a is limit_ordinal
holds phi.a = G(a,phi|a) from ORDINAL2:sch 11;
A7: now
defpred P[Ordinal] means not $1 c= phi($1);
assume
A8: ex a st P[a];
consider a such that
A9: P[a] and
A10: for b st P[b] holds a c= b from ORDINAL1:sch 1(A8);
phi(phi(a)) in phi(a) by A1,A9,ORDINAL1:26; then
not phi(a) c= phi(phi(a)) by ORDINAL1:7;
hence contradiction by A9,A10;
end;
A11:now
let a;
assume a() in a; then
a c= phi(a) & a <> phi(a) by A3,A7; then
a c< phi(a) by XBOOLE_0:def 8;
hence a in phi(a) by ORDINAL1:21;
end;
B1: for a st a in omega holds a() in phi.a
proof let a; assume a in omega; then
reconsider a as Element of omega;
defpred N[Nat] means a() in phi.$1;
B01: N[0] by ORDINAL1:10,A5;
B02: now
let n be Nat; assume
B03: N[n];
n+1 = succ n & n+1 in omega by ORDINAL1:def 13,NAT_1:39; then
phi.(n+1) = phi(phi.n) by A6; then
phi.n in phi.(n+1) by B03,A11;
hence N[n+1] by B03,ORDINAL1:19;
end;
for n being Nat holds N[n] from NAT_1:sch 2(B01,B02); then
N[a];
hence thesis;
end;
A12:phi is increasing
proof
let a,b;
assume
A13: a in b & b in dom phi; then
A14: ex c st b = a+^c & c <> {} by ORDINAL3:31;
defpred R[Ordinal] means
a+^$1 in omega & $1 <> {} implies phi.a in phi.(a+^$1);
A15: R[{}];
A16: for c st R[c] holds R[succ c]
proof
let c such that
A17: a+^c in omega & c <> {} implies phi.a in phi.(a+^c) and
A18: a+^succ c in omega & succ c <> {};
A19: a+^c in succ(a+^c) & a+^succ c = succ(a+^c) by ORDINAL1:10,ORDINAL2:45;
reconsider d = phi.(a+^c) as Ordinal;
a+^c in omega by A18,A19,ORDINAL1:19; then
phi.(a+^succ c) = phi(d) & d in phi(d) & a+^({} qua Ordinal) = a
by A6,A11,A18,A19,ORDINAL2:44,B1;
hence thesis by A17,A18,A19,ORDINAL1:19;
end;
A20: for b st b <> {} & b is limit_ordinal & for c st c in b holds R[c]
holds R[b]
proof
let b such that
A21: b <> {} & b is limit_ordinal and
for c st c in b holds a+^c in omega & c <> {} implies
phi.a in phi.(a+^c) and
A22: a+^b in omega & b <> {};
a+^b <> {} by A22,ORDINAL3:29; then
a+^b is limit_ordinal & {} in a+^b by A21,ORDINAL3:10,32;
hence thesis by A22;
end;
for c holds R[c] from ORDINAL2:sch 1(A15,A16,A20);
hence thesis by A4,A13,A14;
end;
deffunc phi(Ordinal) = phi($1);
consider fi being Ordinal-Sequence such that
A23: dom fi = sup phi & for a st a in sup phi holds fi.a = phi(a)
from ORDINAL2:sch 3;
succ a() in rng phi & sup rng phi = sup phi
by A4,A5,Lm1,FUNCT_1:def 5; then
A24: sup phi <> {} & sup phi is limit_ordinal
by A4,A12,ORDINAL4:16,ORDINAL2:27; then
A25: phi(sup phi) is_limes_of fi by A2,A23;
fi is increasing
proof
let a,b;
assume
A26: a in b & b in dom fi; then
fi.a = phi(a) & fi.b = phi(b) by A23,ORDINAL1:19;
hence thesis by A1,A26;
end; then
A27: sup fi = lim fi by A23,A24,ORDINAL4:8
.= phi(sup phi) by A25,ORDINAL2:def 14;
ZZ: sup fi c= sup phi
proof
let x be set;
assume
A28: x in sup fi; then
reconsider A = x as Ordinal;
consider b such that
A29: b in rng fi & A c= b by A28,ORDINAL2:29;
consider y being set such that
A30: y in dom fi & b = fi.y by A29,FUNCT_1:def 5;
reconsider y as Ordinal by A30;
consider c such that
A31: c in rng phi & y c= c by A23,A30,ORDINAL2:29;
consider z being set such that
A32: z in dom phi & c = phi.z by A31,FUNCT_1:def 5;
reconsider z as Ordinal by A32;
succ z in omega by A4,A32,ORDINAL1:41; then
A33: phi.succ z = phi(c) & phi.succ z in rng phi & b = phi(y)
by A4,A6,A23,A30,A32,FUNCT_1:def 5;
y c< c iff y <> c & y c= c by XBOOLE_0:def 8; then
phi(y) in phi(c) or y = c by A1,A31,ORDINAL1:21; then
b c= phi(c) & phi(c) in sup phi by A33,ORDINAL1:def 2,ORDINAL2:27; then
b in sup phi by ORDINAL1:22;
hence thesis by A29,ORDINAL1:22;
end;
phi.0 in rng phi by A4,FUNCT_1:def 5; then
a() in phi.0 & phi.0 in sup phi by B1,ORDINAL2:27; then
a() in sup phi by ORDINAL1:19;
hence contradiction by A11,A27,ZZ,ORDINAL1:7;
end;
begin :: Epsilon numbers
definition
let a be ordinal number;
attr a is epsilon means:
EPSILON:
exp(omega,a) = a;
end;
theorem ThE0:
ex b st a in b & b is epsilon
proof
deffunc phi(Ordinal) = exp(omega, $1);
A1: for a,b st a in b holds phi(a) in phi(b) by ORDINAL4:24;
A2: now let a such that
B1: a is non empty limit_ordinal;
let phi being Ordinal-Sequence such that
B2: dom phi = a & for b st b in a holds phi.b = phi(b);
phi is non-decreasing
proof
let b,c; assume
B3: b in c & c in dom phi; then
phi.b = phi(b) & phi.c = phi(c) by B2,ORDINAL1:19; then
phi.b in phi.c by B3,A1;
hence thesis by ORDINAL1:def 2;
end; then
Union phi is_limes_of phi & phi(a) = lim phi by B1,B2,ThND,ORDINAL2:62;
hence phi(a) is_limes_of phi by ORDINAL2:def 14;
end;
consider b such that
A3: a in b & phi(b) = b from CriticalNumber3(A1,A2);
take b; thus a in b by A3;
thus exp(omega, b) = b by A3;
end;
registration
cluster epsilon (ordinal number);
existence
proof
ex a st 0 in a & a is epsilon by ThE0;
hence thesis;
end;
end;
definition
let a be Ordinal;
func first_epsilon_greater_than a -> epsilon Ordinal means:
FEGT:
a in it & for b being epsilon Ordinal st a in b holds it c= b;
existence
proof
defpred E[Ordinal] means a in $1 & $1 is epsilon;
A1: ex c st E[c] by ThE0;
consider c such that
A2: E[c] & for b st E[b] holds c c= b from ORDINAL1:sch 1(A1);
reconsider c as epsilon Ordinal by A2;
take c; thus thesis by A2;
end;
uniqueness
proof let b1,b2 be epsilon Ordinal such that
A1: a in b1 & for b being epsilon Ordinal st a in b holds b1 c= b and
A2: a in b2 & for b being epsilon Ordinal st a in b holds b2 c= b;
thus b1 c= b2 & b2 c= b1 by A1,A2;
end;
end;
theorem
a c= b implies first_epsilon_greater_than a c= first_epsilon_greater_than b
proof assume
A0: a c= b;
b in first_epsilon_greater_than b by FEGT; then
a in first_epsilon_greater_than b by A0,ORDINAL1:22;
hence thesis by FEGT;
end;
theorem
a in b & b in first_epsilon_greater_than a implies
first_epsilon_greater_than b = first_epsilon_greater_than a
proof assume
Z0: a in b & b in first_epsilon_greater_than a;
now let c be epsilon Ordinal;
assume b in c; then
a in c by Z0,ORDINAL1:19;
hence first_epsilon_greater_than a c= c by FEGT;
end;
hence first_epsilon_greater_than b = first_epsilon_greater_than a
by Z0,FEGT;
end;
theorem Th20:
first_epsilon_greater_than 0 = omega |^|^ omega
proof
deffunc phi(Ordinal) = exp(omega, $1);
A1: for a,b st a in b holds phi(a) in phi(b) by ORDINAL4:24;
A2: now let a such that
B1: a is non empty limit_ordinal;
let phi being Ordinal-Sequence such that
B2: dom phi = a & for b st b in a holds phi.b = phi(b);
phi is non-decreasing
proof
let b,c; assume
B3: b in c & c in dom phi; then
phi.b = phi(b) & phi.c = phi(c) by B2,ORDINAL1:19; then
phi.b in phi.c by B3,A1;
hence thesis by ORDINAL1:def 2;
end; then
Union phi is_limes_of phi & phi(a) = lim phi by B1,B2,ThND,ORDINAL2:62;
hence phi(a) is_limes_of phi by ORDINAL2:def 14;
end;
deffunc F(Ordinal,Ordinal) = phi($2);
deffunc G(Ordinal,Ordinal-Sequence) = lim $2;
consider f being Ordinal-Sequence such that
A4: dom f = omega and
A5: {} in omega implies f.{} = 1 and
A6: for a st succ a in omega holds f.(succ a) = F(a,f.a) and
for a st a in omega & a <> {} & a is limit_ordinal
holds f.a = G(a,f|a) from ORDINAL2:sch 11;
F1: dom f = omega & f.0 = 1 by A4,A5;
F2: now let a; assume a in omega; then
succ a in omega by ORDINAL1:41;
hence f.(succ a) = phi(f.a) by A6;
end;
A7: 1 c= Union f & phi(Union f) = Union f &
for b st 1 c= b & phi(b) = b holds Union f c= b
from CriticalNumber2(A1,A2,F1,F2);
Union f is epsilon
proof
thus phi(Union f) = Union f by A7;
end; then
reconsider e = Union f as epsilon Ordinal;
defpred I[Nat] means f.$1 = omega |^|^ $1;
I1: I[0] by F1,Th0;
I2: for n st I[n] holds I[n+1]
proof
let n such that
I3: I[n];
I4: n+1 = succ n & n in omega by NAT_1:39,ORDINAL1:def 13;
hence f.(n+1) = phi(f.n) by F2 .= omega |^|^ (n+1) by I3,I4,Th1;
end;
A8: for n holds I[n] from NAT_1:sch 2(I1,I2); then
for c st c in omega holds f.c = omega |^|^ c; then
A9: omega |^|^ omega = lim f by F1,Th2;
f is non-decreasing
proof
let a,b; assume
B1: a in b & b in dom f; then
reconsider n = a, m = b as Element of omega by F1,ORDINAL1:19;
a c= b by B1,ORDINAL1:def 2; then
omega |^|^ a c= omega |^|^ b by Th5; then
f.n c= omega |^|^ m by A8;
hence thesis by A8;
end; then
e is_limes_of f by F1,ThND; then
AA: omega |^|^ omega = e by A9,ORDINAL2:def 14;
B2: succ 0 = 1; then
0 in 1 by ORDINAL1:10; then
AB: 0 in e by A7;
now let b be epsilon Ordinal;
assume 0 in b; then
1 c= b & phi(b) = b by B2,EPSILON,ORDINAL1:33;
hence e c= b by A7;
end;
hence thesis by AA,AB,FEGT;
end;
theorem Th21:
for e being epsilon Ordinal holds omega in e
proof
let e be epsilon Ordinal;
A0: exp(omega, e) = e by EPSILON;
A1: exp(omega,0) = 1 & exp(omega,1) = omega & 1 in omega
by ORDINAL2:60,63; then
A2: e <> 0 & e <> 1 & succ 0 = 1 & succ 1 = 2 by A0; then
0 in e by ORDINAL3:10; then
1 c= e by A2,ORDINAL1:33; then
1 c< e by A2,XBOOLE_0:def 8; then
1 in e by ORDINAL1:21;
hence thesis by A0,A1,ORDINAL4:24;
end;
registration
cluster epsilon -> non empty limit_ordinal Ordinal;
coherence
proof
let e be Ordinal such that
A0: e is epsilon;
exp(omega,0) = 1 by ORDINAL2:60;
hence e is non empty by A0,EPSILON; then
0 in e & exp(omega, e) = e by A0,EPSILON,ORDINAL3:10;
hence thesis by Th002;
end;
end;
theorem Th22:
for e being epsilon Ordinal holds
exp(omega, exp(e, omega)) = exp(e, exp(e, omega))
proof
let e be epsilon Ordinal;
thus exp(omega, exp(e, omega))
= exp(omega, exp(e, 1+^omega)) by CARD_3:116
.= exp(omega, exp(e, omega)*^exp(e, 1)) by ORDINAL4:30
.= exp(omega, exp(e, omega)*^e) by ORDINAL2:63
.= exp(exp(omega, e), exp(e, omega)) by ORDINAL4:31
.= exp(e, exp(e, omega)) by EPSILON;
end;
theorem Th23:
for e being epsilon Ordinal st 0 in n holds
e |^|^ (n+2) = exp(omega, e |^|^ (n+1))
proof
let e be epsilon Ordinal such that
A0: 0 in n;
0 in e by ORDINAL3:10; then
omega in e & e c= e|^|^n by A0,Th6,Th21; then
A1: omega c= e|^|^n by ORDINAL1:def 2;
thus e |^|^ (n+2) = e|^|^(n+1+1)
.= e|^|^succ(n+1) by NAT_1:39
.= exp(e, e|^|^(n+1)) by Th1
.= exp(exp(omega, e), e|^|^(n+1)) by EPSILON
.= exp(omega, (e|^|^(n+1))*^e) by ORDINAL4:31
.= exp(omega, (e|^|^succ n)*^e) by NAT_1:39
.= exp(omega, exp(e, e|^|^n)*^e) by Th1
.= exp(omega, exp(e, e|^|^n)*^exp(e,1)) by ORDINAL2:63
.= exp(omega, exp(e, 1+^e|^|^n)) by ORDINAL4:30
.= exp(omega, exp(e, e|^|^n)) by A1,CARD_3:116
.= exp(omega, e|^|^succ n) by Th1
.= exp(omega, e |^|^ (n+1)) by NAT_1:39;
end;
theorem Th24:
for e being epsilon Ordinal holds
first_epsilon_greater_than e = e |^|^ omega
proof let e be epsilon Ordinal;
deffunc phi(Ordinal) = exp(omega, $1);
A1: for a,b st a in b holds phi(a) in phi(b) by ORDINAL4:24;
A2: now let a such that
B1: a is non empty limit_ordinal;
let phi being Ordinal-Sequence such that
B2: dom phi = a & for b st b in a holds phi.b = phi(b);
phi is non-decreasing
proof
let b,c; assume
B3: b in c & c in dom phi; then
phi.b = phi(b) & phi.c = phi(c) by B2,ORDINAL1:19; then
phi.b in phi.c by B3,ORDINAL4:24;
hence thesis by ORDINAL1:def 2;
end; then
Union phi is_limes_of phi & phi(a) = lim phi by B1,B2,ThND,ORDINAL2:62;
hence phi(a) is_limes_of phi by ORDINAL2:def 14;
end;
deffunc F(Ordinal,Ordinal) = phi($2);
deffunc G(Ordinal,Ordinal-Sequence) = lim $2;
consider f being Ordinal-Sequence such that
A4: dom f = omega and
A5: {} in omega implies f.{} = succ e and
A6: for a st succ a in omega holds f.(succ a) = F(a,f.a) and
for a st a in omega & a <> {} & a is limit_ordinal
holds f.a = G(a,f|a) from ORDINAL2:sch 11;
F1: dom f = omega & f.0 = succ e by A4,A5;
F2: now let a; assume a in omega; then
succ a in omega by ORDINAL1:41;
hence f.(succ a) = phi(f.a) by A6;
end;
A7: succ e c= Union f & phi(Union f) = Union f &
for b st succ e c= b & phi(b) = b holds Union f c= b
from CriticalNumber2(A1,A2,F1,F2);
Union f is epsilon
proof
thus phi(Union f) = Union f by A7;
end; then
reconsider e' = Union f as epsilon Ordinal;
now e in succ e by ORDINAL1:10;
hence e in e' by A7;
let b be epsilon Ordinal; assume e in b; then
succ e c= b & phi(b) = b by EPSILON,ORDINAL1:33;
hence e' c= b by A7;
end; then
A3: e' = first_epsilon_greater_than e by FEGT;
H0: succ 0 = 1 & succ 1 = 2 & succ 2 = 3; then
H1: f.1 = phi(succ e) by F1,A6 .= omega*^phi(e) by ORDINAL2:61
.= omega*^e by EPSILON; then
H2: f.2 = phi(omega*^e) by H0,A6 .= exp(phi(e), omega) by ORDINAL4:31
.= exp(e, omega) by EPSILON; then
H3: f.3 = phi(exp(e, omega)) by H0,A6 .= exp(e, exp(e, omega)) by Th22;
H4: e|^|^0 = 1 & e|^|^1 = e & e|^|^2 = exp(e, e) by Th0,Th3,Th3';
omega in e & 1 in omega by Th21; then
H5: 1 in e by ORDINAL1:19; then
exp(e,1) in exp(e, e) & exp(e,1) in exp(e, omega) by ORDINAL4:24; then
H6: e in exp(e, e) & e in exp(e, omega) by ORDINAL2:63;
defpred I[Nat] means e|^|^$1 in f.($1+1) & f.$1 in e|^|^($1+2);
e in exp(e,e) & exp(e,e) is limit_ordinal
by H4,H5,Th7,Th002,ORDINAL3:10; then
I1: I[0] by F1,H1,H4,ORDINAL1:41,ORDINAL3:35;
I2: for n st I[n] holds I[n+1]
proof
let n such that
I3: I[n];
I4: n+1 = succ n & n+1+1 = succ(n+1) & n in omega & n+1 in omega
by NAT_1:39,ORDINAL1:def 13; then
I5: f.(n+1) = phi(f.n) & f.(n+1+1) = phi(f.(n+1)) by F2;
thus e|^|^(n+1) in f.(n+1+1)
proof
per cases by NAT_1:23;
suppose n = 0;
hence thesis by H2,H4,H6;
end;
suppose n = 1;
hence thesis by H3,H4,H5,H6,ORDINAL4:24;
end;
suppose n >= 2; then
consider k being Nat such that
J1: n = 2+k by NAT_1:10;
0 in k+1 & k+2 = k+1+1 by NAT_1:45; then
phi(e|^|^(k+2)) = e|^|^(k+1+2) by Th23;
hence thesis by I5,J1,I3,ORDINAL4:24;
end;
end;
0 in n+1 & n+2 = n+1+1 by NAT_1:45; then
phi(e|^|^(n+2)) = e|^|^(n+1+2) by Th23; then
phi(f.n) in e|^|^(n+1+2) by I3,ORDINAL4:24;
hence f.(n+1) in e|^|^(n+1+2) by I4,F2;
end;
A8: for n holds I[n] from NAT_1:sch 2(I1,I2);
deffunc G(Ordinal) = e|^|^$1;
consider g being Ordinal-Sequence such that
G0: dom g = omega & for a st a in omega holds g.a = G(a) from ORDINAL2:sch 3;
A9: e |^|^ omega = lim g by G0,Th2;
1 in omega & omega in e by Th21; then
1 in e by ORDINAL1:19; then
g is increasing Ordinal-Sequence by G0,Th8; then
Union g is_limes_of g by G0,ThND; then
AA: e |^|^ omega = Union g by A9,ORDINAL2:def 14;
e' = Union g
proof
thus e' c= Union g
proof
let x be set; assume x in e'; then
consider a being set such that
C1: a in dom f & x in f.a by CARD_5:10;
reconsider a as Element of omega by A4,C1;
C2: a+2 in omega by ORDINAL1:def 13; then
f.a in e|^|^(a+2) & g.(a+2) = G(a+2) by A8,G0; then
f.a in Union g by G0,C2,CARD_5:10;
hence thesis by C1,ORDINAL1:19;
end;
let x be set; assume x in Union g; then
consider a being set such that
C1: a in dom g & x in g.a by CARD_5:10;
reconsider a as Element of omega by G0,C1;
a+1 in omega & e|^|^a in f.(a+1) & g.a = G(a)
by A8,G0,ORDINAL1:def 13; then
g.a in Union f by A4,CARD_5:10;
hence thesis by C1,ORDINAL1:19;
end;
hence thesis by A3,AA;
end;
definition
let a be Ordinal;
func epsilon_a -> Ordinal means:
:: equals omega |^|^ exp(omega, 1+^a); :: wg wikipedii, ale to nie prawda
EPSILON2:
ex phi being Ordinal-Sequence st it = last phi & dom phi = succ a &
phi.{} = omega|^|^omega &
(for b being Ordinal st succ b in succ a
holds phi.succ b = (phi.b)|^|^omega) &
for c being Ordinal st c in succ a & c <> {} & c is limit_ordinal
holds phi.c = lim(phi|c);
correctness
proof
deffunc C(Ordinal,Ordinal) = $2|^|^omega;
deffunc D(Ordinal,Ordinal-Sequence) = lim $2;
(ex F being Ordinal,fi being Ordinal-Sequence
st F = last fi & dom fi = succ a & fi.{} = omega|^|^omega &
(for c being Ordinal st succ c in succ a holds fi.succ c = C(c,fi.c)) &
for c being Ordinal st c in succ a & c <> {} & c is limit_ordinal
holds fi.c = D(c,fi|c) ) & for A1,A2 being Ordinal st
(ex fi being Ordinal-Sequence
st A1 = last fi & dom fi = succ a & fi.{} = omega|^|^omega &
(for C being Ordinal st succ C in succ a holds fi.succ C = C(C,fi.C)) &
for C being Ordinal st C in succ a & C <> {} & C is limit_ordinal
holds fi.C = D(C,fi|C) ) &
(ex fi being Ordinal-Sequence
st A2 = last fi & dom fi = succ a & fi.{} = omega|^|^omega &
(for C being Ordinal st succ C in succ a holds fi.succ C = C(C,fi.C)) &
for C being Ordinal st C in succ a & C <> {} & C is limit_ordinal
holds fi.C = D(C,fi|C) ) holds A1 = A2 from ORDINAL2:sch 13;
hence thesis;
end;
end;
theorem Th30:
epsilon_0 = omega |^|^ omega
proof
deffunc F(Ordinal) = epsilon_$1;
deffunc D(Ordinal,Ordinal-Sequence) = lim $2;
deffunc C(Ordinal,Ordinal) = $2|^|^omega;
A1: for b,c holds c = F(b) iff
ex fi being Ordinal-Sequence st c = last fi & dom fi = succ b &
fi.{} = omega|^|^omega &
(for c st succ c in succ b holds fi.succ c = C(c,fi.c)) &
for c st c in succ b & c <> {} & c is limit_ordinal
holds fi.c = D(c,fi|c) by EPSILON2;
thus F(0) = omega|^|^omega from ORDINAL2:sch 14(A1);
end;
theorem Th31:
epsilon_(succ a) = epsilon_a |^|^ omega
proof
deffunc F(Ordinal) = epsilon_$1;
deffunc D(Ordinal,Ordinal-Sequence) = lim $2;
deffunc C(Ordinal,Ordinal) = $2|^|^omega;
A1: for b,c holds c = F(b) iff
ex fi being Ordinal-Sequence st c = last fi & dom fi = succ b &
fi.{} = omega|^|^omega &
(for c st succ c in succ b holds fi.succ c = C(c,fi.c)) &
for c st c in succ b & c <> {} & c is limit_ordinal
holds fi.c = D(c,fi|c) by EPSILON2;
for b holds F(succ b) = C(b,F(b)) from ORDINAL2:sch 15(A1);
hence thesis;
end;
theorem Th32:
b <> {} & b is limit_ordinal implies
for phi being Ordinal-Sequence st dom phi = b &
for c st c in b holds phi.c = epsilon_c
holds epsilon_b = lim phi
proof
assume
A1: b <> {} & b is limit_ordinal;
deffunc F(Ordinal) = epsilon_$1;
deffunc D(Ordinal,Ordinal-Sequence) = lim $2;
deffunc C(Ordinal,Ordinal) = $2|^|^omega;
let fi being Ordinal-Sequence such that
A2: dom fi = b and
A3: for c st c in b holds fi.c = F(c);
A4: for b,c holds c = F(b) iff
ex fi being Ordinal-Sequence st c = last fi & dom fi = succ b &
fi.{} = omega|^|^omega &
(for c st succ c in succ b holds fi.succ c = C(c,fi.c)) &
for c st c in succ b & c <> {} & c is limit_ordinal
holds fi.c = D(c,fi|c) by EPSILON2;
thus F(b) = D(b,fi) from ORDINAL2:sch 16(A4,A1,A2,A3);
end;
theorem Th33:
a in b implies epsilon_a in epsilon_b
proof
defpred P[Ordinal] means 1 in epsilon_$1 &
for a,b st a in b & b c= $1 holds epsilon_a in epsilon_b;
omega in epsilon_0 by Th9,Th30; then
A0: P[0] by ORDINAL1:19;
A1: P[c] implies P[succ c]
proof assume
B1: P[c];
epsilon_succ c = (epsilon_c) |^|^ omega by Th31; then
B4: epsilon_c in epsilon_succ c by B1,Th9;
hence 1 in epsilon_succ c by B1,ORDINAL1:19;
let a,b; assume
B2: a in b & b c= succ c; then
a c= c by ORDINAL1:34; then
B3: b = succ c & (a = c or a c< c) or b c< succ c by B2,XBOOLE_0:def 8;
per cases by B3,ORDINAL1:21;
suppose b in succ c; then
b c= c by ORDINAL1:34;
hence thesis by B1,B2;
end;
suppose
B5: b = succ c & a in c; then
epsilon_a in epsilon_c by B1;
hence thesis by B4,B5,ORDINAL1:19;
end;
suppose
b = succ c & a = c;
hence thesis by B4;
end;
end;
A2: c <> {} & c is limit_ordinal & (for b st b in c holds P[b]) implies P[c]
proof assume that
C1: c <> {} & c is limit_ordinal and
C2: for b st b in c holds P[b];
deffunc F(Ordinal) = epsilon_$1;
consider f such that
C3: dom f = c & for b st b in c holds f.b = F(b) from ORDINAL2:sch 3;
f is increasing
proof let a,b; assume
C4: a in b & b in dom f; then
a in c by C3,ORDINAL1:19; then
f.a = F(a) & f.b = F(b) & P[b] by C2,C3,C4;
hence thesis by C4;
end; then
Union f is_limes_of f by C1,C3,ThND; then
C5: Union f = lim f by ORDINAL2:def 14 .= epsilon_c by C1,C3,Th32;
C6: 0 in c by C1,ORDINAL3:10; then
1 in epsilon_0 & f.0 = F(0) by C2,C3;
hence 1 in epsilon_c by C3,C5,C6,CARD_5:10;
let a,b; assume
C7: a in b & b c= c; then
C8: b = c or b c< c by XBOOLE_0:def 8;
per cases by C8,ORDINAL1:21;
suppose b in c;
hence epsilon_a in epsilon_b by C2,C7;
end;
suppose
C9: b = c;
succ a in c & a in succ a by C1,C7,ORDINAL1:10,41; then
D1: F(a) in F(succ a) & F(succ a) = f.succ a & f.succ a in rng f
by C2,C3,FUNCT_1:def 5; then
f.succ a c= Union f by ZFMISC_1:92;
hence thesis by C5,C9,D1;
end;
end;
P[c] from ORDINAL2:sch 1(A0,A1,A2);
hence thesis;
end;
theorem Th34:
for phi being Ordinal-Sequence st
for c st c in dom phi holds phi.c = epsilon_c
holds phi is increasing
proof let f; assume
A1: for c st c in dom f holds f.c = epsilon_c;
let a,b; assume
A2: a in b & b in dom f; then
f.a = epsilon_a & f.b = epsilon_b by A1,ORDINAL1:19;
hence thesis by A2,Th33;
end;
theorem Th35:
b <> {} & b is limit_ordinal implies
for phi being Ordinal-Sequence st dom phi = b &
for c st c in b holds phi.c = epsilon_c
holds epsilon_b = Union phi
proof assume
A0: b <> {} & b is limit_ordinal;
let f; assume
A1: dom f = b & for c st c in b holds f.c = epsilon_c; then
f is increasing Ordinal-Sequence by Th34; then
Union f is_limes_of f by A0,A1,ThND; then
Union f = lim f by ORDINAL2:def 14;
hence thesis by A0,A1,Th32;
end;
theorem Th38:
b is non empty limit_ordinal implies
(x in epsilon_b iff ex c st c in b & x in epsilon_c)
proof assume
Z0: b is non empty limit_ordinal;
deffunc F(Ordinal) = epsilon_$1;
consider f such that
Z1: dom f = b & for c st c in b holds f.c = F(c) from ORDINAL2:sch 3;
Z2: Union f = epsilon_b by Z0,Z1,Th35;
hereby assume x in epsilon_b; then
consider c being set such that
Z4: c in dom f & x in f.c by Z2,CARD_5:10;
reconsider c as Ordinal by Z4;
take c;
thus c in b by Z1,Z4;
thus x in epsilon_c by Z1,Z4;
end;
given c such that
A1: c in b & x in epsilon_c;
f.c = F(c) by Z1,A1;
hence x in epsilon_b by Z1,Z2,A1,CARD_5:10;
end;
theorem Th39:
a c= epsilon_a
proof
defpred P[Ordinal] means $1 c= epsilon_$1;
0 in omega & omega c= epsilon_0 by Th6,Th30; then
A0: P[0];
A1: P[b] implies P[succ b]
proof assume
Z0: P[b];
epsilon_b in epsilon_succ b by Th33,ORDINAL1:10; then
b in epsilon_succ b by Z0,ORDINAL1:22;
hence thesis by ORDINAL1:33;
end;
A2: c <> {} & c is limit_ordinal & (for b st b in c holds P[b]) implies P[c]
proof assume that
c <> {} & c is limit_ordinal and
Z1: for b st b in c holds P[b];
let x; assume
Z2: x in c; then
reconsider a = x as Ordinal;
P[a] & epsilon_a in epsilon_c by Z1,Z2,Th33;
hence thesis by ORDINAL1:22;
end;
P[b] from ORDINAL2:sch 1(A0,A1,A2);
hence thesis;
end;
theorem Th37:
for X being non empty set st
for x st x in X holds x is epsilon Ordinal &
ex e being epsilon Ordinal st x in e & e in X
holds union X is epsilon Ordinal
proof
let X be non empty set; assume
Z0: for x st x in X holds x is epsilon Ordinal &
ex e being epsilon Ordinal st x in e & e in X; then
for x st x in X holds x is Ordinal; then
reconsider a = union X as Ordinal by ORDINAL1:35;
now
let b; assume b in a; then
consider x such that
B1: b in x & x in X by TARSKI:def 4;
reconsider x as epsilon Ordinal by B1,Z0;
succ b in x by B1,ORDINAL1:41;
hence succ b in a by B1,TARSKI:def 4;
end; then
Z1: a is limit_ordinal by ORDINAL1:41;
set z = the Element of X;
ex e being epsilon Ordinal st z in e & e in X by Z0; then
Z2: a <> {} by TARSKI:def 4;
a is epsilon
proof
thus exp(omega,a) c= a
proof
let x; assume x in exp(omega,a); then
consider b such that
Z3: b in a & x in exp(omega,b) by Z1,Z2,Th005;
consider y being set such that
Z4: b in y & y in X by Z3,TARSKI:def 4;
reconsider y as epsilon Ordinal by Z0,Z4;
exp(omega,b) in exp(omega,y) by Z4,ORDINAL4:24; then
exp(omega,b) in y by EPSILON; then
x in y by Z3,ORDINAL1:19;
hence thesis by Z4,TARSKI:def 4;
end;
thus thesis by ORDINAL4:32;
end;
hence thesis;
end;
theorem Th36:
for X being non empty set st
(for x st x in X holds x is epsilon Ordinal) &
for a st a in X holds first_epsilon_greater_than a in X
holds union X is epsilon Ordinal
proof
let X be non empty set such that
Z0: for x st x in X holds x is epsilon Ordinal and
Z1: for a st a in X holds first_epsilon_greater_than a in X;
now
let x; assume
Z2: x in X;
hence x is epsilon Ordinal by Z0; then
reconsider a = x as Ordinal;
take e = first_epsilon_greater_than a;
thus x in e & e in X by Z1,Z2,FEGT;
end;
hence union X is epsilon Ordinal by Th37;
end;
registration
let a;
cluster epsilon_a -> epsilon;
coherence
proof
deffunc phi(Ordinal) = epsilon_$1;
defpred P[Ordinal] means phi($1) is epsilon;
A0: P[{}] by Th20,Th30;
A1: P[b] implies P[succ b]
proof
assume P[b]; then
first_epsilon_greater_than epsilon_b = (epsilon_b)|^|^omega by Th24
.= epsilon_(succ b) by Th31;
hence thesis;
end;
A2: b <> {} & b is limit_ordinal & (for c st c in b holds P[c]) implies P[b]
proof assume that
Z0: b <> {} & b is limit_ordinal and
Z1: for c st c in b holds P[c];
consider f such that
Z2: dom f = b & for c st c in b holds f.c = phi(c) from ORDINAL2:sch 3;
Z3: phi(b) = Union f by Z0,Z2,Th35;
set X = rng f;
0 in b by Z0,ORDINAL3:10; then f.0 in rng f by Z2,FUNCT_1:def 5; then
reconsider X as non empty set;
Z4: now let x; assume x in X; then
consider a being set such that
Z5: a in dom f & f.a = x by FUNCT_1:def 5;
reconsider a as Ordinal by Z5;
x = phi(a) by Z2,Z5;
hence x is epsilon Ordinal by Z1,Z2,Z5;
end;
now let x be Ordinal; assume
Z6: x in X; then
consider a being set such that
Z5: a in dom f & f.a = x by FUNCT_1:def 5;
reconsider a as Ordinal by Z5;
Z7: succ a in b by Z0,Z2,Z5,ORDINAL1:41;
reconsider e = x as epsilon Ordinal by Z4,Z6;
e = phi(a) by Z2,Z5; then
first_epsilon_greater_than e = phi(a)|^|^omega by Th24
.= phi(succ a) by Th31 .= f.succ a by Z2,Z7;
hence first_epsilon_greater_than x in X by Z2,Z7,FUNCT_1:def 5;
end;
hence P[b] by Z3,Z4,Th36;
end;
for a holds P[a] from ORDINAL2:sch 1(A0,A1,A2);
hence thesis;
end;
end;
theorem
a is epsilon implies ex b st a = epsilon_b
proof
defpred N[set] means ex b st $1 = epsilon_b;
defpred Q[Ordinal] means
for e being epsilon Ordinal st e in epsilon_$1 holds N[e];
A0: Q[{}]
proof
let e be epsilon Ordinal;
0 in e by ORDINAL3:10; then
first_epsilon_greater_than 0 c= e by FEGT; then
e in epsilon_0 implies e in e by Th20,Th30;
hence thesis;
end;
A1: Q[c] implies Q[succ c]
proof assume
Z0: Q[c];
let e be epsilon Ordinal such that
Z1: e in epsilon_succ c;
Z2: epsilon_succ c = (epsilon_c)|^|^omega by Th31
.= first_epsilon_greater_than epsilon_c by Th24;
per cases by ORDINAL1:24;
suppose e in epsilon_c;
hence N[e] by Z0;
end;
suppose e = epsilon_c;
hence N[e];
end;
suppose epsilon_c in e; then
epsilon_succ c c= e by Z2,FEGT; then
e in e by Z1;
hence N[e];
end;
end;
A2: b <> {} & b is limit_ordinal & (for c st c in b holds Q[c]) implies Q[b]
proof assume that
Y0: b <> {} & b is limit_ordinal and
Y1: for c st c in b holds Q[c];
let e be epsilon Ordinal; assume
e in epsilon_b; then
ex c st c in b & e in epsilon_c by Y0,Th38;
hence N[e] by Y1;
end;
AA: Q[b] from ORDINAL2:sch 1(A0,A1,A2);
a c= epsilon_a & epsilon_a in epsilon_succ a by Th33,Th39,ORDINAL1:10;
hence thesis by AA,ORDINAL1:22;
end;
begin :: Cantor Normal Form
definition
let A be finite Ordinal-Sequence; :: why finite?
func Sum^ A -> Ordinal means:
SUM:
ex f being Ordinal-Sequence st it = last f & dom f = succ dom A &
f.0 = 0 & for n being Nat st n in dom A holds f.(n+1) = f.n +^ A.n;
correctness
proof
deffunc C(Ordinal,Ordinal) = $2+^A.$1;
deffunc D(Ordinal,Ordinal-Sequence) = Union $2;
set b = dom A;
A0: (ex F being Ordinal,fi being Ordinal-Sequence
st F = last fi & dom fi = succ b & fi.{} = 0 &
(for c being Ordinal st succ c in succ b holds fi.succ c = C(c,fi.c)) &
for c being Ordinal st c in succ b & c <> {} & c is limit_ordinal
holds fi.c = D(c,fi|c) ) & for A1,A2 being Ordinal st
(ex fi being Ordinal-Sequence
st A1 = last fi & dom fi = succ b & fi.{} = 0 &
(for C being Ordinal st succ C in succ b holds fi.succ C = C(C,fi.C)) &
for C being Ordinal st C in succ b & C <> {} & C is limit_ordinal
holds fi.C = D(C,fi|C) ) &
(ex fi being Ordinal-Sequence
st A2 = last fi & dom fi = succ b & fi.{} = 0 &
(for C being Ordinal st succ C in succ b holds fi.succ C = C(C,fi.C)) &
for C being Ordinal st C in succ b & C <> {} & C is limit_ordinal
holds fi.C = D(C,fi|C) ) holds A1 = A2 from ORDINAL2:sch 13; then
consider a,f such that
A2: a = last f & dom f = succ b & f.0 = 0 &
(for c being Ordinal st succ c in succ b holds f.succ c = C(c,f.c)) &
for c being Ordinal st c in succ b & c <> {} & c is limit_ordinal
holds f.c = D(c,f|c);
hereby
take a,f; thus a = last f & dom f = succ b & f.0 = 0 by A2;
let n; assume n in dom A; then
succ n c= dom A by ORDINAL1:33; then
succ n in succ b & n+1 = succ n by ORDINAL1:34,NAT_1:39;
hence f.(n+1) = f.n +^ A.n by A2;
end;
let a1,a2 be Ordinal;
given f1 being Ordinal-Sequence such that
B1: a1 = last f1 & dom f1 = succ dom A &
f1.0 = 0 & for n being Nat st n in dom A holds f1.(n+1) = f1.n +^ A.n;
given f2 being Ordinal-Sequence such that
B2: a2 = last f2 & dom f2 = succ dom A &
f2.0 = 0 & for n being Nat st n in dom A holds f2.(n+1) = f2.n +^ A.n;
reconsider b as finite Ordinal;
A3: succ b in omega & b in omega by CARD_1:103;
B3: for c being Ordinal st succ c in succ b holds f1.succ c = C(c,f1.c)
proof
let c; assume succ c in succ b; then
Z0: c in b by ORDINAL3:5; then
reconsider n = c as Element of omega;
f1.(n+1) = C(n,f1.n) by B1,Z0;
hence thesis by NAT_1:39;
end;
B4: for c being Ordinal st c in succ b & c <> {} & c is limit_ordinal
holds f1.c = D(c,f1|c)
proof
let c be Ordinal;
assume
C0: c in succ b & c <> {} & c is limit_ordinal; then
0 in c by ORDINAL3:10; then
c in omega & omega c= c by C0,A3,ORDINAL1:19,def 12;
hence f1.c = D(c,f1|c);
end;
B5: for c being Ordinal st succ c in succ b holds f2.succ c = C(c,f2.c)
proof
let c; assume succ c in succ b; then
Z0: c in b by ORDINAL3:5; then
reconsider n = c as Element of omega;
f2.(n+1) = C(n,f2.n) by B2,Z0;
hence thesis by NAT_1:39;
end;
for c being Ordinal st c in succ b & c <> {} & c is limit_ordinal
holds f2.c = D(c,f2|c)
proof
let c be Ordinal;
assume
C0: c in succ b & c <> {} & c is limit_ordinal; then
0 in c by ORDINAL3:10; then
c in omega & omega c= c by C0,A3,ORDINAL1:19,def 12;
hence thesis;
end;
hence thesis by A0,B1,B2,B3,B4,B5;
end;
end;
theorem Th50:
Sum^ {} = 0
proof
ex f being Ordinal-Sequence st Sum^ {} = last f & dom f = succ dom {} &
f.0 = 0 & for n being Nat st n in dom {} holds f.(n+1) = f.n +^ {}.n
by SUM;
hence thesis by ORDINAL2:7;
end;
theorem Th51:
Sum^ <%a%> = a
proof
consider f being Ordinal-Sequence such that
A1: Sum^ <%a%> = last f & dom f = succ dom <%a%> & f.0 = 0 &
for n being Nat st n in dom <%a%> holds f.(n+1) = f.n +^ <%a%>.n by SUM;
A2: dom <%a%> = 1 & <%a%>.0 = a by AFINSQ_1:def 5;
0 in 1 by NAT_1:45; then
f.(0+1) = (0 qua Ordinal) +^ a by A1,A2 .= a by ORDINAL2:47;
hence thesis by A1,A2,ORDINAL2:7;
end;
theorem Th59:
for A being finite Ordinal-Sequence holds Sum^ (A^<%a%>) = (Sum^ A) +^ a
proof
let A be finite Ordinal-Sequence;
consider f being Ordinal-Sequence such that
A1: Sum^(A^<%a%>) = last f & dom f = succ dom(A^<%a%>) & f.0 = 0 &
for n being Nat st n in dom(A^<%a%>)
holds f.(n+1) = f.n+^(A^<%a%>).n by SUM;
consider g being Ordinal-Sequence such that
A2: Sum^ A = last g & dom g = succ dom A & g.0 = 0 &
for n being Nat st n in dom A holds g.(n+1) = g.n +^ A.n by SUM;
dom <%a%> = 1 by AFINSQ_1:def 5; then
A5: dom (A^<%a%>) = (dom A)+^1 & (dom A)+^1 = succ dom A
by ORDINAL2:48,ORDINAL4:def 1;
reconsider dA = dom A as Element of NAT by ORDINAL1:def 13;
A6: dom A in succ dom A by ORDINAL1:10;
defpred P[Nat] means $1 in succ dom A implies f.$1 = g.$1;
A3: P[0] by A1,A2;
A4: P[n] implies P[n+1]
proof assume that
B1: P[n] and
B2: n+1 in succ dom A;
n+1 = succ n by NAT_1:39; then
B3: n in dom A by B2,ORDINAL3:5; then
B4: n in succ dom A by A6,ORDINAL1:19; then
g.(n+1) = g.n +^ A.n & f.(n+1) = f.n+^(A^<%a%>).n by A1,A2,A5,B3;
hence thesis by B1,B3,B4,ORDINAL4:def 1;
end;
AA: P[n] from NAT_1:sch 2(A3,A4);
thus Sum^ (A^<%a%>) = f.((dom A)+^1) by A1,A5,ORDINAL2:7
.= f.(dA+1) by CARD_2:49
.= f.(dom A)+^(A^<%a%>).len A by A1,A5,A6
.= f.(dom A) +^ a by AFINSQ_1:40
.= g.(dom A) +^ a by A6,AA
.= (Sum^ A) +^ a by A2,ORDINAL2:7;
end;
theorem Th52:
for A being finite Ordinal-Sequence holds Sum^ (<%a%>^A) = a +^ Sum^ A
proof
defpred P[finite T-Sequence] means
for f being finite Ordinal-Sequence st f = $1
holds Sum^(<%a%>^f) = a +^ Sum^ f;
<%a%>^{} = <%a%> by AFINSQ_1:32; then
Sum^(<%a%>^{}) = a by Th51; then
A0: P[{}] by Th50,ORDINAL2:44;
A1: for f being finite T-Sequence, x st P[f] holds P[f^<%x%>]
proof
let f be finite T-Sequence;
let x; assume
A2: P[f];
let g be finite Ordinal-Sequence;
consider b such that
A3: rng g c= b by ORDINAL2:def 8;
assume
A4: g = f^<%x%>; then
rng g = (rng f)\/rng<%x%> by AFINSQ_1:29; then
A5: rng f c= b & rng <%x%> c= b by A3,XBOOLE_1:11; then
reconsider f' = f as finite Ordinal-Sequence by ORDINAL2:def 8;
rng <%x%> = {x} by AFINSQ_1:36; then
x in b by A5,ZFMISC_1:37; then
reconsider x as Ordinal;
thus Sum^(<%a%>^g) = Sum^ (<%a%>^f'^<%x%>) by A4,AFINSQ_1:30
.= Sum^ (<%a%>^f') +^ x by Th59
.= a +^ Sum^ f' +^ x by A2
.= a +^ (Sum^ f' +^ x) by ORDINAL3:33
.= a +^ Sum^ g by A4,Th59;
end;
for f being finite T-Sequence holds P[f] from AFINSQ_1:sch 3(A0,A1);
hence thesis;
end;
theorem Th53:
for A being finite Ordinal-Sequence holds A.0 c= Sum^ A
proof
let A be finite Ordinal-Sequence;
defpred P[finite T-Sequence] means
for A being finite Ordinal-Sequence st $1 = A holds A.0 c= Sum^ A;
dom {} = {}; then
{}.0 = 0 by FUNCT_1:def 4; then
A0: P[{}] by XBOOLE_1:2;
A1: for f being finite T-Sequence, x st P[f] holds P[f^<%x%>]
proof
let f be finite T-Sequence;
let x; assume
A2: P[f];
let g be finite Ordinal-Sequence;
consider b such that
A3: rng g c= b by ORDINAL2:def 8;
assume
A4: g = f^<%x%>; then
rng g = (rng f)\/rng<%x%> by AFINSQ_1:29; then
A5: rng f c= b & rng <%x%> c= b by A3,XBOOLE_1:11; then
reconsider f' = f as finite Ordinal-Sequence by ORDINAL2:def 8;
rng <%x%> = {x} by AFINSQ_1:36; then
x in b by A5,ZFMISC_1:37; then
reconsider x as Ordinal;
per cases;
suppose f = {}; then
g = <%x%> by A4,AFINSQ_1:32; then
g.0 = x & Sum^ g = x by Th51,AFINSQ_1:def 5;
hence g.0 c= Sum^ g;
end;
suppose f <> {}; then
0 in dom f' & Sum^ g = Sum^ f' +^ x by A4,Th59,ORDINAL3:10; then
g.0 = f'.0 & f'.0 c= Sum^ f' & Sum^ f' c= Sum^ g
by A2,A4,ORDINAL3:27,ORDINAL4:def 1;
hence g.0 c= Sum^ g by XBOOLE_1:1;
end;
end;
for f being finite T-Sequence holds P[f] from AFINSQ_1:sch 3(A0,A1);
hence A.0 c= Sum^ A;
end;
definition
let a;
attr a is Cantor-component means:
CC:
ex b,n st 0 in n & a = n*^exp(omega,b);
end;
registration
cluster Cantor-component -> non empty Ordinal;
coherence
proof
let a;
given b,n such that
A0: 0 in n & a = n*^exp(omega,b);
exp(omega,b) <> 0 by ORDINAL4:22;
hence thesis by A0,ORDINAL3:34;
end;
end;
registration
cluster Cantor-component Ordinal;
existence
proof
take a = 1*^exp(omega,1), b = 1, n = 1;
thus thesis by NAT_1:45;
end;
end;
definition
let a,b;
func b-exponent(a) -> Ordinal means:
EXP:
exp(b,it) c= a & for c st exp(b,c) c= a holds c c= it if 1 in b & 0 in a
otherwise it = 0;
existence
proof
hereby assume
A: 1 in b & 0 in a;
defpred P[Ordinal] means a c= exp(b,$1);
a c= exp(b,a) by A,ORDINAL4:32; then
A0: ex c st P[c];
consider c such that
A1: P[c] & for d st P[d] holds c c= d from ORDINAL1:sch 1(A0);
0 in 1 by NAT_1:45; then
A2: 0 in b by A,ORDINAL1:19;
per cases by A1,XBOOLE_0:def 8;
suppose
B1: a = exp(b,c);
take c; thus exp(b,c) c= a by B1;
let d; assume
B2: exp(b,d) c= a & d c/= c; then
c in d by ORDINAL1:26; then
a in exp(b,d) by A,B1,ORDINAL4:24; then
a in a by B2;
hence contradiction;
end;
suppose a c< exp(b,c); then
C1: a in exp(b,c) by ORDINAL1:21;
succ 0 c= a by A,ORDINAL1:33; then
1 in exp(b,c) & exp(b,0) = 1 by C1,ORDINAL1:22,ORDINAL2:60; then
C4: c <> 0;
now assume c is limit_ordinal; then
consider d such that
C2: d in c & a in exp(b,d) by C4,A2,C1,Th005;
P[d] by C2,ORDINAL1:def 2; then
c c= d by A1; then
d in d by C2;
hence contradiction;
end; then
consider d such that
C3: c = succ d by ORDINAL1:42;
take d;
thus exp(b,d) c= a
proof
assume exp(b,d) c/= a; then
a c= exp(b,d); then
c c= d by A1; then
d in d by C3,ORDINAL1:33;
hence thesis;
end;
let e; assume
B2: exp(b,e) c= a & e c/= d; then
d in e by ORDINAL1:26; then
c c= e by C3,ORDINAL1:33; then
exp(b,c) c= exp(b,e) by A,ORDINAL4:27; then
a in exp(b,e) by C1; then
a in a by B2;
hence contradiction;
end;
end;
thus thesis;
end;
uniqueness
proof
let d1,d2 be Ordinal;
hereby assume that 1 in b & 0 in a and
A1: exp(b,d1) c= a & for c st exp(b,c) c= a holds c c= d1 and
A2: exp(b,d2) c= a & for c st exp(b,c) c= a holds c c= d2;
thus d1 = d2 proof thus d1 c= d2 by A1,A2; thus thesis by A1,A2; end;
end;
thus thesis;
end;
consistency;
end;
theorem Th41:
a in exp(omega, succ(omega-exponent(a)))
proof per cases by ORDINAL3:10;
suppose
A0: 0 in a; assume
not thesis; then
exp(omega, succ(omega-exponent(a))) c= a by ORDINAL1:26; then
succ(omega-exponent(a)) c= omega-exponent(a) &
omega-exponent(a) in succ(omega-exponent(a)) by A0,EXP,ORDINAL1:10; then
omega-exponent(a) in omega-exponent(a);
hence contradiction;
end;
suppose
A1: a = 0; then
omega-exponent(a) = 0 by EXP; then
exp(omega, succ(omega-exponent(a))) = omega by ORDINAL2:63;
hence thesis by A1;
end;
end;
theorem Th42:
0 in n implies omega-exponent(n*^exp(omega,a)) = a
proof assume
Z0: 0 in n; then
succ 0 c= n by ORDINAL1:33; then
Z1: 1*^exp(omega,a) = exp(omega,a) & 1*^exp(omega,a) c= n*^exp(omega,a)
by ORDINAL2:56,58;
Z5: exp(omega,a) <> 0 by ORDINAL4:22; then
Z2: 1 in omega & 0 in n*^exp(omega,a) by ORDINAL3:10,Z0,ORDINAL3:34;
now let b; assume
Z3: exp(omega,b) c= n*^exp(omega,a) & b c/= a; then
a in b by ORDINAL1:26; then
succ a c= b by ORDINAL1:33; then
Z4: exp(omega, succ a) c= exp(omega, b) by ORDINAL4:27;
exp(omega, succ a) = omega*^exp(omega, a) by ORDINAL2:61; then
omega*^exp(omega, a) c= n*^exp(omega,a) by Z3,Z4,XBOOLE_1:1; then
omega c= n & n in omega by Z5,ORDINAL1:def 13,ORDINAL3:38;
hence contradiction;
end;
hence omega-exponent(n*^exp(omega,a)) = a by Z1,Z2,EXP;
end;
theorem Th43a:
0 in a & c = omega-exponent a implies a div^ exp(omega, c) in omega
proof assume
A0: 0 in a & c = omega-exponent a;
set n = a div^ exp(omega, c);
set b = a mod^ exp(omega, c);
exp(omega,c) <> 0 by ORDINAL4:22; then
consider d such that
A2: a = n*^exp(omega, c)+^d & d in exp(omega, c) by ORDINAL3:def 7;
assume not n in omega; then
omega*^exp(omega,c) c= n*^exp(omega,c) by ORDINAL2:58,ORDINAL1:26; then
exp(omega, succ c) c= n*^exp(omega,c) & n*^exp(omega,c) c= a
by A2,ORDINAL2:61,ORDINAL3:27; then
exp(omega, succ c) c= a by XBOOLE_1:1; then
succ c c= c & c in succ c by A0,EXP,ORDINAL1:10; then
c in c;
hence contradiction;
end;
theorem Th43b:
0 in a & c = omega-exponent a implies 0 in a div^ exp(omega, c)
proof assume
A0: 0 in a & c = omega-exponent a;
set n = a div^ exp(omega, c);
set b = a mod^ exp(omega, c);
exp(omega,c) <> 0 by ORDINAL4:22; then
consider d such that
A2: a = n*^exp(omega, c)+^d & d in exp(omega, c) by ORDINAL3:def 7;
assume not 0 in n; then
n = 0 by ORDINAL3:10; then
a = (0 qua Ordinal)+^d by A2,ORDINAL2:52 .= d by ORDINAL2:47; then
exp(omega, c) c= d by A0,EXP; then
d in d by A2;
hence contradiction;
end;
theorem Th43c:
0 in a & c = omega-exponent a implies a mod^ exp(omega, c) in exp(omega, c)
proof assume
0 in a & c = omega-exponent a;
set n = a div^ exp(omega, c);
set b = a mod^ exp(omega, c);
exp(omega,c) <> 0 by ORDINAL4:22; then
consider d such that
A2: a = n*^exp(omega, c)+^d & d in exp(omega, c) by ORDINAL3:def 7;
d = a -^ n*^exp(omega, c) by A2,ORDINAL3:65 .= b by ORDINAL3:def 8;
hence thesis by A2;
end;
theorem Th43:
0 in a implies
ex n,b st a = n*^exp(omega, omega-exponent(a))+^b & 0 in n &
b in exp(omega, omega-exponent(a))
proof assume
A0: 0 in a;
set c = omega-exponent a;
set n = a div^ exp(omega, c);
set b = a mod^ exp(omega, c);
n in omega by A0,Th43a; then
reconsider n as Nat;
take n,b;
thus a = n*^exp(omega, c)+^b by ORDINAL3:78;
thus 0 in n by A0,Th43b;
thus b in exp(omega, c) by A0,Th43c;
end;
theorem Th43d:
omega-exponent b in omega-exponent a implies b in a
proof assume
A1: omega-exponent b in omega-exponent a; then
succ(omega-exponent(b)) c= omega-exponent(a) by ORDINAL1:33; then
A3: exp(omega, succ(omega-exponent(b))) c= exp(omega, omega-exponent(a))
by ORDINAL4:27;
A4: 0 in a by A1,EXP;
b in exp(omega, succ(omega-exponent(b))) by Th41; then
b in exp(omega, omega-exponent(a)) &
exp(omega, omega-exponent(a)) c= a by A3,A4,EXP;
hence thesis;
end;
definition
let A be Ordinal-Sequence;
attr A is Cantor-normal-form means:
CNF:
(for a st a in dom A holds A.a is Cantor-component) &
for a,b st a in b & b in dom A holds
omega-exponent(A.b) in omega-exponent(A.a);
end;
registration
cluster empty -> Cantor-normal-form Ordinal-Sequence;
coherence
proof
let f; assume a0: f is empty;
thus for a st a in dom f holds f.a is Cantor-component by a0;
thus thesis by a0;
end;
:: cluster Cantor-normal-form -> non-empty Ordinal-Sequence;
cluster Cantor-normal-form -> decreasing Ordinal-Sequence;
coherence
proof
let f such that
for a st a in dom f holds f.a is Cantor-component and
A1: for a,b st a in b & b in dom f holds
omega-exponent(f.b) in omega-exponent(f.a);
let a,b; assume
a in b & b in dom f; then
omega-exponent(f.b) in omega-exponent(f.a) by A1;
hence thesis by Th43d;
end;
end;
reserve A,B,A1,A2 for Cantor-normal-form Ordinal-Sequence;
theorem
Sum^ A = 0 implies A = {}
proof assume
A0: Sum^ A = 0 & A <> {}; then
0 in dom A by ORDINAL3:10; then
reconsider a = A.0 as Cantor-component Ordinal by CNF;
0 in a & a c= Sum^ A by Th53,ORDINAL3:10;
hence thesis by A0;
end;
theorem Th44:
0 in n implies <%n*^exp(omega,b)%> is Cantor-normal-form
proof assume
A0: 0 in n;
set A = <%n*^exp(omega,b)%>;
A1: dom A = 1 & A.0 = n*^exp(omega,b) by AFINSQ_1:def 5;
hereby let a; assume a in dom A; then
a = 0 & 0 in 1 by A1,TARSKI:def 1,ORDINAL3:18;
hence A.a is Cantor-component by A0,A1,CC;
end;
let a,b; assume
A2: a in b;
assume b in dom A;
hence omega-exponent(A.b) in omega-exponent(A.a)
by A2,A1,TARSKI:def 1,ORDINAL3:18;
end;
registration
cluster non empty Cantor-normal-form Ordinal-Sequence;
existence
proof
take A = <%1*^exp(omega,1)%>;
thus A is non empty;
0 in 1 by NAT_1:45;
hence thesis by Th44;
end;
end;
theorem Th46:
for A,B being Ordinal-Sequence st A^B is Cantor-normal-form
holds A is Cantor-normal-form & B is Cantor-normal-form
proof
let A,B be Ordinal-Sequence;
set AB = A^B;
assume that
Z0: for a st a in dom (A^B) holds (A^B).a is Cantor-component and
Z1: for a,b st a in b & b in dom (A^B) holds
omega-exponent((A^B).b) in omega-exponent((A^B).a);
Z2: dom (A^B) = (dom A)+^(dom B) by ORDINAL4:def 1; then
Z3: dom A c= dom (A^B) by ORDINAL3:27;
thus A is Cantor-normal-form
proof
hereby let a; assume a in dom A; then
A.a = (A^B).a & a in dom (A^B) by Z3,ORDINAL4:def 1;
hence A.a is Cantor-component by Z0;
end;
let a,b; assume
Y1: a in b & b in dom A; then
a in dom A by ORDINAL1:19; then
A.a = AB.a & A.b = AB.b & b in dom AB by Z3,Y1,ORDINAL4:def 1;
hence omega-exponent(A.b) in omega-exponent(A.a) by Z1,Y1;
end;
hereby let a; assume a in dom B; then
B.a = AB.((dom A)+^a) & (dom A)+^a in dom AB
by Z2,ORDINAL3:20,ORDINAL4:def 1;
hence B.a is Cantor-component by Z0;
end;
let a,b; assume
Y1: a in b & b in dom B; then
a in dom B by ORDINAL1:19; then
B.a = AB.((dom A)+^a) & B.b = AB.((dom A)+^b) & (dom A)+^b in dom AB &
(dom A)+^a in (dom A)+^b by Z2,Y1,ORDINAL3:20,ORDINAL4:def 1;
hence omega-exponent(B.b) in omega-exponent(B.a) by Z1;
end;
theorem
A <> {} implies ex c being Cantor-component Ordinal, B st A = <%c%>^B
proof
assume A <> {}; then
consider n being Nat such that
A1: len A = n+1 by NAT_1:6;
reconsider n as Element of NAT by ORDINAL1:def 13;
n+1 = 1+^n by CARD_2:49; then
consider S1,S2 such that
A2: A = S1^S2 & dom S1 = 1 & dom S2 = n by A1,Th65;
reconsider S1,S2 as Ordinal-Sequence by A2,ThS2;
S1^S2 is Cantor-normal-form by A2; then
reconsider S1,S2 as Cantor-normal-form Ordinal-Sequence by Th46;
0 in 1 by NAT_1:45; then
reconsider c = S1.0 as Cantor-component Ordinal by A2,CNF;
take c, S2;
len S1 = 1 by A2;
hence thesis by A2,AFINSQ_1:38;
end;
theorem Th45:
for A being non empty Cantor-normal-form Ordinal-Sequence
for c being Cantor-component Ordinal
st omega-exponent(A.0) in omega-exponent(c)
holds <%c%>^A is Cantor-normal-form
proof
let A be non empty Cantor-normal-form Ordinal-Sequence;
let c be Cantor-component Ordinal such that
A0: omega-exponent(A.0) in omega-exponent(c);
set B = <%c%>^A;
A1: dom <%c%> = 1 & <%c%>.0 = c by AFINSQ_1:def 5; then
A2: dom B = 1 +^ dom A by ORDINAL4:def 1;
hereby let a;
assume
A3: a in dom B;
per cases by A2,A3,ORDINAL3:42;
suppose
A4: a in 1; then
a = 0 by ORDINAL3:18,TARSKI:def 1;
hence B.a is Cantor-component by A1,A4,ORDINAL4:def 1;
end;
suppose ex b st b in dom A & a = 1 +^b; then
consider b such that
A5: b in dom A & a = 1 +^b;
B.a = A.b by A1,A5,ORDINAL4:def 1;
hence B.a is Cantor-component by A5,CNF;
end;
end;
let a,b; assume
A6: a in b & b in dom B;
per cases;
suppose not a in 1; then
B1: 1 c= a by ORDINAL1:26; then
B2: 1 in b & a in dom B & (1+^dom A)-^1 = dom A
by A6,ORDINAL1:19,22,ORDINAL3:65; then
B3: b-^1 in dom A & a-^1 in dom A & a-^1 in b-^1
by B1,A2,A6,ORDINAL3:66;
b = 1+^(b-^1) & a = 1+^(a-^1) by B1,B2,ORDINAL3:60,def 6; then
B.a = A.(a-^1) & B.b = A.(b-^1) by A1,B3,ORDINAL4:def 1;
hence thesis by B3,CNF;
end;
suppose a in 1; then
C1: B.a = <%c%>.a & a = 0 by A1,TARSKI:def 1,ORDINAL3:18,ORDINAL4:def 1; then
C2: succ 0 c= b by A6,ORDINAL1:33; then
b-^1 in (1+^dom A)-^1 by A2,A6,ORDINAL3:66; then
C3: b-^1 in dom A & b = 1+^(b-^1) by C2,ORDINAL3:def 6,65; then
C4: B.b = A.(b-^1) by A1,ORDINAL4:def 1;
0 in dom A & (b-^1 = 0 or 0 in b-^1) by ORDINAL3:10; then
omega-exponent(A.0) = omega-exponent(A.(b-^1)) or
omega-exponent(A.(b-^1)) in omega-exponent(A.0) by C3,CNF;
hence thesis by A0,A1,C1,C4,ORDINAL1:19;
end;
end;
theorem
ex A being Cantor-normal-form Ordinal-Sequence st a = Sum^ A
proof
defpred P[Ordinal] means 0 in $1 implies
ex A being non empty Cantor-normal-form Ordinal-Sequence st $1 = Sum^ A;
A0: for a st for b st b in a holds P[b] holds P[a]
proof let a such that
Z0: for b st b in a holds P[b] and
Z1: 0 in a;
consider n,b such that
Z2: a = n*^exp(omega, omega-exponent(a))+^b & 0 in n &
b in exp(omega, omega-exponent(a)) by Z1,Th43;
reconsider s = n*^exp(omega, omega-exponent(a)) as
Cantor-component Ordinal by Z2,CC;
set c = omega-exponent(a);
exp(omega, c) c= a by Z1,EXP; then
Z3: P[b] by Z0,Z2;
per cases by ORDINAL3:10;
suppose
B1: b = 0;
reconsider A = <%n*^exp(omega, omega-exponent(a))%> as
non empty Cantor-normal-form Ordinal-Sequence by Z2,Th44;
take A;
thus a = n*^exp(omega, omega-exponent(a)) by Z2,B1,ORDINAL2:44
.= Sum^ A by Th51;
end;
suppose
0 in b; then
consider A being non empty Cantor-normal-form Ordinal-Sequence
such that
B3: b = Sum^ A by Z3;
B4: A.0 in exp(omega, omega-exponent(a)) by Z2,B3,ORDINAL1:22,Th53;
0 in dom A by ORDINAL3:10; then
A.0 is Cantor-component Ordinal by CNF; then
0 in A.0 by ORDINAL3:10; then
exp(omega, omega-exponent(A.0)) c= A.0 by EXP; then
exp(omega, omega-exponent(A.0)) in exp(omega, omega-exponent(a))
by B4,ORDINAL1:22; then
B5: omega-exponent(A.0) in omega-exponent(a) by Th006;
omega-exponent(s) = omega-exponent(a) by Z2,Th42; then
reconsider B = <%s%>^A as non empty Cantor-normal-form Ordinal-Sequence
by B5,Th45;
take B;
thus a = Sum^ B by Z2,B3,Th52;
end;
end;
A1: P[b] from ORDINAL1:sch 2(A0);
per cases by ORDINAL3:10;
suppose
Y0: a = 0;
reconsider A = {} as Cantor-normal-form Ordinal-Sequence;
take A;
thus thesis by Y0,Th50;
end;
suppose 0 in a; then
ex A being non empty Cantor-normal-form Ordinal-Sequence st a = Sum^ A
by A1;
hence thesis;
end;
end;