:: Epsilon Numbers and Cantor Normal Form
:: by Grzegorz Bancerek
::
:: Received October 20, 2009
:: Copyright (c) 2009-2026 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 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, ORDINAL1,
XCMPLX_0, NAT_1, XXREAL_0, NEWTON, ORDINAL2, AFINSQ_1, ORDINAL3,
ORDINAL4, CARD_1, CARD_3, NUMBERS;
constructors NEWTON, NAT_1, AFINSQ_1, ORDINAL3, CARD_3, NUMBERS;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, NAT_1, XREAL_0, ORDINAL2,
ORDINAL4, CARD_1, CARD_5, CARD_LAR, NEWTON, AFINSQ_1, FINSET_1;
requirements SUBSET, BOOLE, NUMERALS, ARITHM, REAL;
definitions TARSKI, XBOOLE_0, ORDINAL2, ORDINAL1;
equalities ORDINAL2, CARD_3, ORDINAL1;
expansions TARSKI, XBOOLE_0;
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, XREGULAR;
schemes NAT_1, ORDINAL1, ORDINAL2, AFINSQ_1;
begin :: Preliminaries
reserve
a,b,c,d,e for Ordinal,
m,n for Nat,
f for Ordinal-Sequence,
x for object;
theorem Th1:
a c= succ b implies a c= b or a = succ b by ORDINAL1:16,21;
registration
cluster omega -> limit_ordinal;
:: rezultat innych rejestracji, ale nalezy przeniesc do ORDINAL1
coherence;
cluster -> Ordinal-yielding for empty set;
coherence
proof let f be empty set;
take 0;
thus thesis;
end;
end;
registration
cluster non empty finite for Sequence;
existence
proof
take <%the set%>;
thus thesis;
end;
end;
registration
let f be Sequence;
let g be non empty Sequence;
cluster f^g -> non empty;
coherence
proof
(dom f)+^dom g <> 0 by ORDINAL3:26; 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:26; then
dom(g^f) <> 0 by ORDINAL4:def 1;
hence thesis;
end;
end;
reserve S,S1,S2 for Sequence;
theorem Th2:
dom S = a+^b implies ex S1,S2 st S = S1^S2 & dom S1 = a & dom S2 = b
proof assume
A1: dom S = a+^b;
set S1 = S|a;
A2: a c= a+^b by ORDINAL3:24; then
A3: dom S1 = a by A1,RELAT_1:62;
deffunc F(Ordinal) = S.(a+^$1);
consider S2 such that
A4: 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;
A5: dom S = dom s by A1,A3,A4,ORDINAL4:def 1;
now let x be object; assume
A6: x in dom S; then reconsider z = x as Ordinal;
per cases by A1,A6,ORDINAL3:38;
suppose
A7: z in a;
hence S.x = S1.z by FUNCT_1:49 .= s.x by A7,A3,ORDINAL4:def 1;
end;
suppose ex c st c in b & z = a+^c; then
consider c such that
A8: c in b & z = a+^c;
thus S.x = S2.c by A4,A8 .= s.x by A8,A3,A4,ORDINAL4:def 1;
end;
end;
hence thesis by A2,A4,A5,A1,FUNCT_1:2,RELAT_1:62;
end;
theorem Th3:
rng S1 c= rng(S1^S2) & rng S2 c= rng(S1^S2)
proof
set q = S1^S2;
A1: dom q = (dom S1)+^dom S2 by ORDINAL4:def 1; then
A2: dom S1 c= dom q by ORDINAL3:24;
thus rng S1 c= rng(S1^S2)
proof
let x be object; assume x in rng S1; then
consider z being object such that
A3: z in dom S1 & x = S1.z by FUNCT_1:def 3;
reconsider z as Ordinal by A3;
q.z = x & z in dom q by A3,A2,ORDINAL4:def 1;
hence thesis by FUNCT_1:def 3;
end;
let x be object; assume x in rng S2; then
consider z being object such that
A4: z in dom S2 & x = S2.z by FUNCT_1:def 3;
reconsider z as Ordinal by A4;
q.((dom S1)+^z) = x & (dom S1)+^z in dom q
by A1,A4,ORDINAL3:17,ORDINAL4:def 1;
hence thesis by FUNCT_1:def 3;
end;
theorem Th4:
S1^S2 is Ordinal-yielding implies
S1 is Ordinal-yielding & S2 is Ordinal-yielding
proof
given a such that
A1: rng (S1^S2) c= a;
thus S1 is Ordinal-yielding
proof
take a;
rng S1 c= rng(S1^S2) by Th3;
hence thesis by A1;
end;
take a;
rng S2 c= rng(S1^S2) by Th3;
hence thesis by A1;
end;
definition
let f be 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:
Def2:
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 for 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 for Ordinal-Sequence;
coherence
by ORDINAL1:def 2;
end;
theorem Th5:
for f being Sequence holds f is infinite iff omega c= dom f
proof
let f be Sequence;
f is infinite iff dom f is infinite by FINSET_1:10;
hence thesis by CARD_3:85;
end;
registration
cluster decreasing -> finite for Sequence;
coherence
proof
let f be 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 Th5; then
f.0 in X by FUNCT_1:def 6; then
consider x being set such that
A3: x in X & X misses x by XREGULAR:1;
consider a being object such that
A4: a in dom f & a in omega & x = f.a by A3,FUNCT_1:def 6;
reconsider a as Ordinal by A4;
A5: succ a in omega by A4,ORDINAL1:28; then
a in succ a & succ a in dom f by A2,ORDINAL1:6; then
f.succ a in x & f.succ a in X by A1,A4,A5,FUNCT_1:def 6;
hence thesis by A3,XBOOLE_0:3;
end;
cluster -> decreasing increasing for empty set;
coherence
proof
let e be empty set;
thus e is decreasing ;
let a; thus thesis;
end;
end;
registration
let a;
cluster <%a%> -> Ordinal-yielding;
coherence
proof
take succ a;
let x be object; assume x in rng <%a%>; then
x in {a} by AFINSQ_1:33; then
x = a by TARSKI:def 1;
hence thesis by ORDINAL1:6;
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 4;
hence for c,b st c in b & b in dom f holds f.b in f.c
by ORDINAL3:15,TARSKI:def 1;
let c,b; thus thesis by A1,ORDINAL3:15,TARSKI:def 1;
end;
end;
registration
cluster decreasing increasing non-decreasing non-increasing finite
non empty for Ordinal-Sequence;
existence
proof
set a = the Ordinal;
take <%a%>; thus thesis;
end;
end;
theorem Th6:
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
A1: dom f is non empty;
set a0 = the Element of dom f;
per cases;
case
A2: Union f = 0;
take a0; thus a0 in dom f by A1;
let c; assume a0 c= c & c in dom f; then
f.c in rng f by FUNCT_1:def 3;
hence f.c = 0 by A2,ORDERS_1:6;
end;
case Union f <> 0;
let b,c; assume
A3: b in Union f & Union f in c; then
consider x being object such that
A4: x in dom f & b in f.x by CARD_5:2;
reconsider x as Ordinal by A4;
take x; thus x in dom f by A4;
let E be Ordinal; assume
A5: x c= E & E in dom f; then
x = E or x c< E; then
x = E or x in E by ORDINAL1:11; then
f.x c= f.E by A5,Def2;
hence b in f.E by A4;
f.E in rng f by A5,FUNCT_1:def 3; then
f.E c= Union f by ZFMISC_1:74;
hence f.E in c by A3,ORDINAL1:12;
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:21; then
A1: exp(omega, succ a) c= exp(omega, b) by ORDINAL4:27;
A2: exp(omega, succ a) = omega*^exp(omega, a) by ORDINAL2:44;
n in omega by ORDINAL1:def 12; then
n*^exp(omega, a) in omega*^exp(omega, a) by ORDINAL3:19,ORDINAL4:22;
hence thesis by A1,A2;
end;
theorem Th8:
0 in a & (for b st b in dom f holds f.b = exp(a,b)) implies
f is non-decreasing
proof assume
A1: 0 in a & for b st b in dom f holds f.b = exp(a,b);
let b,d; assume
A2: b in d & d in dom f; then
b in dom f by ORDINAL1:10; then
b c= d & f.b = exp(a,b) & f.d = exp(a,d) by A1,A2,ORDINAL1:def 2;
hence thesis by A1,ORDINAL4:27;
end;
theorem Th9:
a is limit_ordinal & 0 in b implies exp(a,b) is limit_ordinal proof assume
A1: a is limit_ordinal & 0 in b;
per cases by ORDINAL3:8;
suppose a = 0;
hence thesis by A1,ORDINAL4:20;
end;
suppose
A2: 0 in a;
defpred P[Ordinal] means 0 in $1 implies exp(a,$1) is limit_ordinal;
A3: P[0];
A4: P[c] implies P[succ c]
proof
exp(a, succ c) = a*^exp(a,c) by ORDINAL2:44;
hence thesis by A1,ORDINAL3:40;
end;
A5: c <> 0 & c is limit_ordinal & (for b st b in c holds P[b]) implies P[c]
proof assume that
A6: c <> 0 & c is limit_ordinal and
A7: for b st b in c holds P[b];
deffunc F(Ordinal) = exp(a,$1);
consider f such that
A8: dom f = c & for b st b in c holds f.b = F(b) from ORDINAL2:sch 3;
A9: exp(a,c) = lim f by A6,A8,ORDINAL2:45;
f is non-decreasing by A2,A8,Th8; then
Union f is_limes_of f by A6,A8,Th6; then
A10: exp(a,c) = Union f by A9,ORDINAL2:def 10;
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 object such that
A11: b in dom f & d in f.b by A10,CARD_5:2;
reconsider b as Ordinal by A11;
A12: succ b in dom f by A6,A8,A11,ORDINAL1:28; then
A13: f.b = F(b) & f.succ b = F(succ b) & P[succ b] by A7,A8,A11;
F(b) c= F(succ b) by A2,ORDINAL3:1,ORDINAL4:27; then
succ d in f.succ b by A13,A11,ORDINAL1:28,ORDINAL3:8;
hence succ d in exp(a,c) by A10,A12,CARD_5:2;
end;
hence P[c] by ORDINAL1:28;
end;
P[c] from ORDINAL2:sch 1(A3,A4,A5);
hence thesis by A1;
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
A1: 1 in a & for b st b in dom f holds f.b = exp(a,b);
let b,d; assume
A2: b in d & d in dom f; then
f.b = exp(a,b) & f.d = exp(a,d) by A1,ORDINAL1:10;
hence thesis by A1,A2,ORDINAL4:24;
end;
theorem Th11:
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
A1: 0 in a & b is non empty limit_ordinal;
deffunc F(Ordinal) = exp(a,$1);
consider f such that
A2: dom f = b & for c st c in b holds f.c = F(c) from ORDINAL2:sch 3;
f is non-decreasing by A1,A2,Th8; then
Union f is_limes_of f by A1,A2,Th6; then
A3: Union f = lim f by ORDINAL2:def 10 .= exp(a,b) by A1,A2,ORDINAL2:45;
hereby assume x in exp(a,b); then
consider c being object such that
A4: c in dom f & x in f.c by A3,CARD_5:2;
reconsider c as Ordinal by A4;
take c;
thus c in b by A2,A4;
thus x in exp(a,c) by A2,A4;
end;
given c such that
A5: c in b & x in exp(a,c);
f.c = F(c) by A2,A5;
hence x in exp(a,b) by A2,A3,A5,CARD_5:2;
end;
theorem Th12:
0 in a & exp(a,b) in exp(a,c) implies b in c proof assume
A1: 0 in a & exp(a,b) in exp(a,c);
assume not b in c; then
exp(a,c) c= exp(a,b) by A1,ORDINAL1:16,ORDINAL4:27; then
exp(a,b) in exp(a,b) by A1;
hence thesis;
end;
begin :: Tetration (Knuth's arrow notation) of ordinals
definition
let a,b be Ordinal;
func a|^|^b -> Ordinal means:
Def4:
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.0 = 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 <> 0 & 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 = 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 <> 0 & 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 = 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 <> 0 & C is limit_ordinal
holds fi.C = D(C,fi|C) ) holds A1 = A2 from ORDINAL2:sch 13;
hence thesis;
end;
end;
theorem Th13:
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.0 = 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 <> 0 & c is limit_ordinal
holds fi.c = D(c,fi|c) by Def4;
thus F(0) = 1 from ORDINAL2:sch 14(A1);
end;
theorem Th14:
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.0 = 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 <> 0 & c is limit_ordinal
holds fi.c = D(c,fi|c) by Def4;
for b holds F(succ b) = C(b,F(b)) from ORDINAL2:sch 15(A1);
hence thesis;
end;
theorem Th15:
b <> 0 & 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 <> 0 & 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.0 = 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 <> 0 & c is limit_ordinal
holds fi.c = D(c,fi|c) by Def4;
thus F(b) = D(b,fi) from ORDINAL2:sch 16(A4,A1,A2,A3);
end;
theorem Th16:
a |^|^ 1 = a
proof
0+1 = succ 0;
hence a |^|^ 1 = exp(a, a|^|^0) by Th14 .= exp(a, 1) by Th13
.= a by ORDINAL2:46;
end;
theorem Th17:
1 |^|^ a = 1
proof
defpred P[Ordinal] means 1 |^|^ $1 = 1;
A1: P[0] by Th13;
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 Th14
.= 1 by ORDINAL2:46;
end;
A3: for A being Ordinal st A <> 0 & 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 <> 0 & 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,Th15;
A8: rng fi c= { 1 }
proof
let x being object;
assume x in rng fi; then
consider y being object such that
A9: y in dom fi & x = fi.y by FUNCT_1:def 3;
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;
set x = the 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 3;
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 9;
hence 1 |^|^ A = 1 by A7,ORDINAL2:def 10;
end;
for a holds P[a] from ORDINAL2:sch 1(A1,A2,A3);
hence thesis;
end;
theorem Th18:
a |^|^ 2 = exp(a, a)
proof
2 = succ 1;
hence a |^|^ 2 = exp(a, a|^|^1) by Th14 .= exp(a, a) by Th16;
end;
theorem
a |^|^ 3 = exp(a,exp(a, a))
proof
3 = succ 2;
hence a |^|^ 3 = exp(a, a|^|^2) by Th14 .= exp(a,exp(a, a)) by Th18;
end;
theorem
for n being Nat 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 Th13,Th16;
A2: now
let n be Nat; assume
A3: P[n];
thus P[n+1]
proof
thus
A4: 0 |^|^ (2*(n+1)) = 0 |^|^ Segm(2*n+1+1)
.= 0 |^|^ succ Segm(2*n+1) by NAT_1:38
.= exp(0, 0) by A3,Th14
.= 1 by ORDINAL2:43;
thus 0 |^|^ (2*(n+1)+1) = 0 |^|^ Segm(2*(n+1)+1)
.= 0 |^|^ succ Segm(2*(n+1)) by NAT_1:38
.= exp(0, 1) by A4,Th14 .= 0 by ORDINAL2:46;
end;
end;
thus for n being Nat holds P[n] from NAT_1:sch 2(A1,A2);
end;
theorem Th21:
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:21; then
A3: 1 c< c or 1 = c;
per cases by A3,ORDINAL1:11;
suppose c = 1; then
c |^|^ a = 1 & c |^|^ b = 1 by Th17;
hence thesis;
end;
suppose
A4: 1 in c;
defpred H[Ordinal] means
for a,b st a c= b & b c= $1 holds c |^|^ a c= c |^|^ b;
A5: H[0] proof let a,b;
assume
A6: a c= b & b c= 0; then
b = {};
hence thesis by A6;
end;
A7: now let d such that
A8: H[d];
c |^|^ (succ d) = exp(c, c |^|^ d) by Th14; then
A9: c |^|^ d c= c |^|^ (succ d) by A4,ORDINAL4:32;
thus H[succ d] proof let a,b such that
A10: a c= b & b c= succ d;
A11: a c= succ d by A10;
per cases by A10,A11,Th1;
suppose b c= d;
hence thesis by A8,A10;
end;
suppose b = succ d & a = succ d;
hence thesis;
end;
suppose
A12: b = succ d & a c= d; then
c |^|^ a c= c |^|^ d by A8;
hence thesis by A9,A12;
end;
end;
end;
A13: now let d such that
A14: d <> 0 & d is limit_ordinal and
A15: for e st e in d holds H[e];
deffunc E(Ordinal) = c|^|^$1;
consider f being Ordinal-Sequence such that
A16: 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
A17: a in b & b in dom f; then
a c= b & H[b] by A15,A16,ORDINAL1:def 2; then
c |^|^ a c= c |^|^ b & a in d & f.b = E(b) by A16,A17,ORDINAL1:12;
hence thesis by A16;
end; then
A18: Union f is_limes_of f by A14,A16,Th6;
c|^|^d = lim f by A14,A16,Th15; then
A19: c|^|^d = Union f by A18,ORDINAL2:def 10;
thus H[d]
proof
let a,b; assume
A20: a c= b & b c= d; then
A21: (b c< d or b = d) & (a c< b or a = b);
per cases by A21,ORDINAL1:11;
suppose b in d;
hence E(a) c= E(b) by A20,A15;
end;
suppose
A22: b = d & a in d; then
f.a in rng f & f.a = E(a) by A16,FUNCT_1:def 3;
hence E(a) c= E(b) by A19,A22,ZFMISC_1:74;
end;
suppose b = d & a = d;
hence E(a) c= E(b);
end;
end;
end;
for b holds H[b] from ORDINAL2:sch 1(A5,A7,A13);
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
A1: 0 in a and
A2: for b st b in dom f holds f.b = a|^|^b;
let b,c; assume
A3: 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 A1,A2,A3,Th21;
hence f.b c= f.c by A2,A3,ORDINAL1:10;
end;
theorem Th23:
0 in a & 0 in b implies a c= a |^|^ b proof assume
A1: 0 in a & 0 in b;
defpred J[Ordinal] means 0 in $1 implies a c= a |^|^ $1;
A2: J[0];
A3: now let b; assume
A4: J[b];
A5: a |^|^ succ b = exp(a, a |^|^ b) by Th14;
A6: succ 0 = 0+1;
thus J[succ b]
proof
per cases by ORDINAL3:8;
suppose 0 in b; then
1 c= a |^|^ b by A6,A1,A4,ORDINAL1:21; then
exp(a, 1) c= exp(a, a |^|^ b) by A1,ORDINAL4:27;
hence thesis by A5,ORDINAL2:46;
end;
suppose
b = 0; then
a |^|^ b = 1 by Th13;
hence thesis by A5,ORDINAL2:46;
end;
end;
end;
A7: now let c such that
A8: c <> 0 & 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
A9: 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
A10: e in b & b in dom phi; then
A11: phi.b = F(b) & e in c by A9,ORDINAL1:10; then
phi.e = F(e) & e c= b by A9,A10,ORDINAL1:def 2;
hence thesis by A1,A11,Th21;
end; then
A12: Union phi is_limes_of phi by A8,A9,Th6;
lim phi = F(c) by A8,A9,Th15; then
A13: F(c) = Union phi by A12,ORDINAL2:def 10;
thus J[c]
proof
assume 0 in c; then
succ 0 in c by A8,ORDINAL1:28; then
phi.1 in rng phi & phi.1 = F(1) & F(1) = a by A9,Th16,FUNCT_1:def 3;
hence thesis by A13,ZFMISC_1:74;
end;
end;
for b holds J[b] from ORDINAL2:sch 1(A2,A3,A7);
hence thesis by A1;
end;
theorem Th24:
1 in a & m < n implies a |^|^ m in a |^|^ n proof assume
A1: 1 in a & m < n; then m+1 <= n by NAT_1:13; then
consider k being Nat such that
A2: 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 Th13; then
A3: Q[0] by A1,Th16;
A4: now let n; assume
A5: Q[n];
succ Segm n = Segm(n+1) & succ Segm (n+1) = Segm(n+1+1) by NAT_1:38;
then
a|^|^(n+1) = exp(a, a|^|^n) & a|^|^((n+1)+1) = exp(a, a|^|^(n+1)) by Th14
;
hence Q[n+1] by A5,A1,ORDINAL4:24;
end;
A6: for n holds Q[n] from NAT_1:sch 2(A3,A4); then
A7: P[0];
A8: now let k be Nat; assume
A9: P[k];
a|^|^(m+1+k) in a|^|^((m+1+k)+1) by A6;
hence P[k+1] by A9,ORDINAL1:10;
end;
for k being Nat holds P[k] from NAT_1:sch 2(A7,A8);
hence thesis by A2;
end;
:: theorem :: false a |^|^ succ omega = a |^|^ omega for a > 0
:: 1 in c & a in b implies c |^|^ a in c |^|^ b
theorem Th25:
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
A1: 1 in a and
A2: dom f c= omega and
A3: for n being Ordinal st n in dom f holds f.n = a|^|^n;
let b,c; assume
A4: b in c & c in dom f; then
A5: b in dom f by ORDINAL1:10;
reconsider b,c as Element of omega by A2,A4,ORDINAL1:10;
b in Segm c by A4;
then f.b = a|^|^b & f.c = a|^|^c & b < c by A3,A4,A5,NAT_1:44;
hence thesis by A1,Th24;
end;
theorem Th26:
1 in a & 1 in b implies a in a |^|^ b proof assume
A1: 1 in a;
assume 1 in b; then
A2: succ 1 c= b by ORDINAL1:21;
0 in Segm 1 by NAT_1:44; then
0 in a by A1,ORDINAL1:10;
then a|^|^1 in a|^|^2 & a|^|^2 c= a|^|^b by A1,A2,Th21,Th24; then
a|^|^1 in a|^|^b;
hence a in a |^|^ b by Th16;
end;
theorem Th27:
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:43; then
A1: P[0] by NEWTON:4;
A2: now
let k be Nat such that
A3: P[k];
reconsider n9 = n, nk = n|^k as Element of NAT by ORDINAL1:def 12;
Segm(k+1) = succ Segm k by NAT_1:38; then
exp(n,k+1) = n *^ exp(n,k) by ORDINAL2:44 .= n9 * nk by A3,CARD_2:37;
hence P[k+1] by NEWTON:6;
end;
thus for k being Nat holds P[k] from NAT_1:sch 2(A1,A2);
end;
registration
let n,k be Nat;
identify exp(n,k) with n|^k;
compatibility by Th27;
end;
registration
let n,k be Nat;
cluster exp(n,k) -> natural;
coherence;
end;
registration
let n,k be Nat;
cluster n |^|^ k -> natural;
coherence
proof
defpred O[Nat] means n |^|^ $1 is natural;
A1: O[0] by Th13;
A2: now let k be Nat;
assume O[k]; then
reconsider nk = n|^|^k as Nat;
Segm(k+1) = succ Segm k by NAT_1:38; then
n|^|^(k+1) = exp(n, nk) by Th14;
hence O[k+1];
end;
for k being Nat holds O[k] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
end;
theorem Th28:
for n,k being Nat st n > 1 holds n |^|^ k > k
proof
let n,k be Nat such that
A1: n > 1;
defpred H[Nat] means n |^|^ $1 > $1;
A2: H[0] by Th13;
A3: now
let k be Nat such that
A4: H[k];
succ Segm k = Segm(k+1) by NAT_1:38; then
n |^|^ (k+1) = exp(n, n |^|^ k) by Th14 .= n |^ (n |^|^ k); then
A5: n |^|^ (k+1) > n |^ k by A1,A4,PEPIN:66;
n |^ k > k by A1,NAT_4:3; then
n |^ k >= k+1 by NAT_1:13;
hence H[k+1] by A5,XXREAL_0:2;
end;
for k being Nat holds H[k] from NAT_1:sch 2(A2,A3);
hence thesis;
end;
theorem
for n being Nat st n > 1 holds n |^|^ omega = omega
proof
let n be Nat such that
A1: n > 1;
deffunc F(Ordinal) = n |^|^ $1;
consider phi being Ordinal-Sequence such that
A2: dom phi = omega & for b st b in omega holds phi.b = F(b)
from ORDINAL2:sch 3;
A3: rng phi c= omega
proof
let x be object; assume x in rng phi; then
consider a being object such that
A4: a in dom phi & x = phi.a by FUNCT_1:def 3;
reconsider a as Element of omega by A2,A4;
x = n |^|^ a by A2,A4;
hence thesis by ORDINAL1:def 12;
end;
A5: n |^|^ omega = lim phi by A2,Th15;
now
thus {} <> omega;
let b,c such that
A6: b in omega & omega in c;
reconsider x = b as Element of omega by A6;
take D = n |^|^ x; thus D in dom phi by A2,ORDINAL1:def 12;
x < D by A1,Th28; then
A7: b in Segm D by NAT_1:44;
let E be Ordinal;
assume
A8: D c= E & E in dom phi; then
reconsider e = E as Element of omega by A2;
x in Segm e by A7,A8; then
x < e & e < n |^|^ e by A1,Th28,NAT_1:44; then
A9: x < n |^|^ e & phi.e = F(e) by A2,XXREAL_0:2;
phi.E in rng phi by A8,FUNCT_1:def 3;
then reconsider phiE = phi.E as Nat by A3;
b in Segm phiE by A9,NAT_1:44;
hence b in phi.E;
phi.E in rng phi by A8,FUNCT_1:def 3;
hence phi.E in c by A6,A3,ORDINAL1:10;
end; then
omega is_limes_of phi by ORDINAL2:def 9;
hence n |^|^ omega = omega by A5,ORDINAL2:def 10;
end;
theorem Th30:
1 in a implies a |^|^ omega is limit_ordinal proof assume
A1: 1 in a;
deffunc F(Ordinal) = a |^|^ $1;
consider phi being Ordinal-Sequence such that
A2: 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 A2,ORDINAL1:10;
b in Segm c by A3;
then b < c by NAT_1:44; then
phi.b = F(b) & F(b) in F(c) by A1,A2,Th24;
hence thesis by A2;
end; then
lim phi = sup phi & sup phi is limit_ordinal by A2,ORDINAL4:8,16;
hence thesis by A2,Th15;
end;
theorem Th31:
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:21; then
A1: 1 = a or 1 c< a;
per cases by A1,ORDINAL1:11;
suppose
A2: a = 1;
hence exp(a, a |^|^ omega) = 1 by ORDINAL2:46 .= a |^|^ omega by A2,Th17;
end;
suppose
A3: 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 Segm 1 by NAT_1:44; then
0 in a & 0 in omega by A3,ORDINAL1:10; then
A6: a c= a|^|^omega by Th23;
E is increasing Ordinal-Sequence by A3,A5,ORDINAL4:25; then
lim E = exp(a, a|^|^omega) & Union E is_limes_of E
by A5,A6,Th6,A3,Th30,ORDINAL2:45; then
A7: exp(a, a|^|^omega) = Union E by ORDINAL2:def 10;
T is increasing Ordinal-Sequence by A3,A4,Th25; then
lim T = a|^|^omega & Union T is_limes_of T by A4,Th15,Th6; then
A8: a|^|^omega = Union T by ORDINAL2:def 10;
thus exp(a, a |^|^ omega) c= a |^|^ omega
proof
let x be Ordinal; assume x in exp(a, a |^|^ omega); then
consider b being object such that
A9: b in dom E & x in E.b by A7,CARD_5:2;
consider c being object such that
A10: c in dom T & b in T.c by A5,A8,A9,CARD_5:2;
reconsider b as Ordinal by A9;
reconsider c as Element of omega by A4,A10;
A11: exp(a, b) in exp(a, T.c) by A3,A10,ORDINAL4:24;
A12: succ c in omega by ORDINAL1:def 12;
then E.b = E(b) & T.c = T(c) & T.succ c = T(succ c) by A9,A4,A5; then
E.b in T.(succ c) by A11,Th14; then
x in T.(succ c) by A9,ORDINAL1:10;
hence thesis by A4,A8,CARD_5:2,A12;
end;
thus a |^|^ omega c= exp(a, a |^|^ omega) by A3,ORDINAL4:32;
end;
end;
theorem
0 in a & omega c= b implies a |^|^ b = a |^|^ omega proof assume
A1: 0 in a;
assume omega c= b; then
A2: b = omega+^(b-^omega) by ORDINAL3:def 5;
defpred P[Ordinal] means a |^|^ (omega+^$1) = a |^|^ omega;
A3: P[0] by ORDINAL2:27;
A4: P[c] implies P[succ c]
proof
assume P[c]; then
A5: exp(a, a |^|^ (omega+^c)) = a |^|^ omega by A1,Th31;
thus a |^|^ (omega+^succ c) = a |^|^ succ (omega+^c) by ORDINAL2:28
.= a |^|^ omega by A5,Th14;
end;
A6: c <> 0 & c is limit_ordinal & (for b st b in c holds P[b]) implies P[c]
proof assume
A7: c <> 0 & c is limit_ordinal;
assume
A8: for b st b in c holds P[b];
deffunc F(Ordinal) = a |^|^ $1;
consider f such that
A9: 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 A7,ORDINAL3:26,29; then
A10: a|^|^(omega+^c) = lim f by A9,Th15;
now a c= a|^|^omega by A1,Th23;
hence a|^|^omega <> {} by A1;
let B,C be Ordinal;
assume
A11: B in a|^|^omega & a|^|^omega in C;
take D = omega;
omega+^({} qua Ordinal) = omega & {} in c
by A7,ORDINAL2:27,ORDINAL3:8;
hence D in dom f by A9,ORDINAL2:32;
let E be Ordinal;
assume
A12: D c= E & E in dom f; then
E-^D in (omega+^c)-^omega by A9,ORDINAL3:53; then
E-^D in c by ORDINAL3:52; then
P[E-^D] by A8; then
a|^|^omega = a|^|^E by A12,ORDINAL3:def 5;
hence B in f.E & f.E in C by A9,A11,A12;
end; then
a|^|^omega is_limes_of f by ORDINAL2:def 9;
hence P[c] by A10,ORDINAL2:def 10;
end;
P[c] from ORDINAL2:sch 1(A3,A4,A6);
hence a |^|^ b = a |^|^ omega by A2;
end;
begin
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
A3: dom f() = omega & f().0 = a() and
A4: for a st a in omega holds f().(succ a) = phi(f().a)
proof
A5: a() in rng f() by A3,FUNCT_1:def 3;
hence a() c= Union f() by ZFMISC_1:74;
set phi = f();
A6: now :: a c= phi(a)
defpred P[Ordinal] means not $1 c= phi($1);
assume
A7: ex a st P[a];
consider a such that
A8: P[a] and
A9: for b st P[b] holds a c= b from ORDINAL1:sch 1(A7);
phi(phi(a)) in phi(a) by A1,A8,ORDINAL1:16; then
not phi(a) c= phi(phi(a)) by ORDINAL1:5;
hence contradiction by A8,A9;
end; then
a() c= phi(a()); then
A10: a() c< phi(a()) or a() = phi(a());
per cases by A10,ORDINAL1:11;
suppose
A11: phi(a()) = a();
A12: 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();
A13: P[0] by A3;
A14: now let n be Nat; assume
A15: P[n];
A16: Segm(n+1) = succ Segm n by NAT_1:38;
n in omega by ORDINAL1:def 12; then
f().succ n = phi(a()) by A4,A15;
hence P[n+1] by A11,A16;
end;
for n being Nat holds P[n] from NAT_1:sch 2(A13,A14); then
P[a];
hence thesis;
end;
rng f() = {a()}
proof
thus rng f() c= {a()}
proof
let x be object; assume x in rng f(); then
consider a being object such that
A17: a in dom f() & x = f().a by FUNCT_1:def 3;
x = a() by A12,A17,A3;
hence thesis by TARSKI:def 1;
end;
thus thesis by A5,ZFMISC_1:31;
end; then
Union f() = a() by ZFMISC_1:25;
hence phi(Union f()) = Union f() &
for b st a() c= b & phi(b) = b holds Union f() c= b by A11;
end;
suppose
A18: a() in phi(a());
deffunc F(Ordinal,Ordinal) = phi($2);
deffunc G(Ordinal,Sequence) = {};
A19: now let a such that
A20: succ a in omega;
a in succ a by ORDINAL1:6;
hence phi.(succ a) = F(a,phi.a) by A4,A20,ORDINAL1:10;
end;
A21: 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;
A22: N[0] by A18,A3,A4;
A23: now
let n be Nat; assume
A24: N[n];
A25: Segm(n+1) = succ Segm n & Segm(n+1+1) = succ Segm(n+1) &
n+1 in omega & n+1+1 in omega by NAT_1:38; then
phi.(n+1) = phi(phi.n) & phi.(n+1+1) = phi(phi.(n+1)) by A19; then
phi.n c= phi.(n+1) & phi.(n+1) in phi.(n+1+1) by A1,A6,A24,A25;
hence N[n+1] by A24,XBOOLE_1:1,A25;
end;
for n being Nat holds N[n] from NAT_1:sch 2(A22,A23); then
N[a];
hence thesis;
end;
deffunc phi(Ordinal) = phi($1);
consider fi being Ordinal-Sequence such that
A26: 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 A3,A4; then
phi(a()) in rng phi by A3,FUNCT_1:def 3; then
A27: phi(a()) c= Union phi by ZFMISC_1:74;
now
let c; assume c in Union phi; then
consider x being object such that
A28: x in dom phi & c in phi.x by CARD_5:2;
reconsider x as Element of omega by A3,A28;
succ c c= phi.x & phi.x in phi.succ x by A21,A28,ORDINAL1:21; then
succ c in phi.succ x & succ x in omega by ORDINAL1:12,def 12;
hence succ c in Union phi by A3,CARD_5:2;
end; then
A29: Union phi is limit_ordinal by ORDINAL1:28; then
A30: phi(Union phi) is_limes_of fi by A2,A26,A27,A18;
fi is increasing
proof
let a,b;
assume
A31: a in b & b in dom fi; then
fi.a = phi(a) & fi.b = phi(b) by A26,ORDINAL1:10;
hence thesis by A1,A31;
end; then
A32: sup fi = lim fi by A26,A27,A29,A18,ORDINAL4:8
.= phi(Union phi) by A30,ORDINAL2:def 10;
thus phi(Union phi) c= Union phi
proof
let x be Ordinal;
assume
A33: x in phi(Union phi);
reconsider A = x as Ordinal;
consider b such that
A34: b in rng fi & A c= b by A32,A33,ORDINAL2:21;
consider y being object such that
A35: y in dom fi & b = fi.y by A34,FUNCT_1:def 3;
reconsider y as Ordinal by A35;
consider z being object such that
A36: z in dom phi & y in phi.z by A26,A35,CARD_5:2;
reconsider z as Ordinal by A36;
set c = phi.z;
succ z in omega by A3,A36,ORDINAL1:28; then
phi.succ z = phi(c) & phi.succ z in rng phi & b = phi(y)
by A3,A19,A26,A35,FUNCT_1:def 3;
then b in phi(c) & phi(c) c= Union phi by A1,A36,ZFMISC_1:74;
hence thesis by A34,ORDINAL1:12;
end;
thus Union f() c= phi(Union f()) by A6;
let b; assume
A37: a() c= b & phi(b) = b;
rng f() c= b
proof
let x be object; assume x in rng f(); then
consider a being object such that
A38: a in dom f() & x = f().a by FUNCT_1:def 3;
reconsider a as Element of omega by A3,A38;
defpred P[Nat] means f().$1 in b;
a() <> b by A18,A37; then
a() c< b by A37; then
A39: P[0] by A3,ORDINAL1:11;
A40: now let n be Nat; assume P[n]; then
phi(f().n) in b & n in omega by A1,A37,ORDINAL1:def 12; then
A41: f().succ n in b by A4;
Segm(n+1) = succ Segm n by NAT_1:38;
hence P[n+1] by A41;
end;
for n being Nat holds P[n] from NAT_1:sch 2(A39,A40); then
P[a];
hence thesis by A38;
end; then
Union f() c= union b & union b c= b by ORDINAL2:5,ZFMISC_1:77;
hence Union f() c= b;
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,Sequence) = {};
consider phi being Ordinal-Sequence such that
A4: dom phi = omega and
A5: 0 in omega implies phi.0 = 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 <> 0 & 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:16; then
not phi(a) c= phi(phi(a)) by ORDINAL1:5;
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);
hence a in phi(a) by ORDINAL1:11;
end;
A12
: 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;
A13: N[0] by A5,ORDINAL1:6;
A14: now
let n be Nat; assume
A15: N[n];
Segm(n+1) = succ Segm n & n+1 in omega by NAT_1:38; then
phi.(n+1) = phi(phi.n) by A6; then
phi.n in phi.(n+1) by A15,A11;
hence N[n+1] by A15,ORDINAL1:10;
end;
for n being Nat holds N[n] from NAT_1:sch 2(A13,A14); then
N[a];
hence thesis;
end;
A16:phi is increasing
proof
let a,b;
assume
A17: a in b & b in dom phi; then
A18: ex c st b = a+^c & c <> {} by ORDINAL3:28;
defpred R[Ordinal] means
a+^$1 in omega & $1 <> {} implies phi.a in phi.(a+^$1);
A19: R[0];
A20: for c st R[c] holds R[succ c]
proof
let c such that
A21: a+^c in omega & c <> {} implies phi.a in phi.(a+^c) and
A22: a+^succ c in omega & succ c <> {};
A23: a+^c in succ(a+^c) & a+^succ c = succ(a+^c) by ORDINAL1:6,ORDINAL2:28;
reconsider d = phi.(a+^c) as Ordinal;
a+^c in omega by A22,A23,ORDINAL1:10; then
phi.(a+^succ c) = phi(d) & d in phi(d) & a+^({} qua Ordinal) = a
by A6,A11,A22,A23,A12,ORDINAL2:27;
hence thesis by A21,A22,A23,ORDINAL1:10;
end;
A24: for b st b <> 0 & b is limit_ordinal & for c st c in b holds R[c]
holds R[b]
proof
let b such that
A25: b <> 0 & 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
A26: a+^b in omega & b <> {};
a+^b <> {} by A26,ORDINAL3:26; then
a+^b is limit_ordinal & {} in a+^b by A25,ORDINAL3:8,29;
hence thesis by A26;
end;
for c holds R[c] from ORDINAL2:sch 1(A19,A20,A24);
hence thesis by A4,A17,A18;
end;
deffunc phi(Ordinal) = phi($1);
consider fi being Ordinal-Sequence such that
A27: 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,FUNCT_1:def 3; then
A28: sup phi <> {} & sup phi is limit_ordinal
by A4,A16,ORDINAL2:19,ORDINAL4:16; then
A29: phi(sup phi) is_limes_of fi by A2,A27;
fi is increasing
proof
let a,b;
assume
A30: a in b & b in dom fi; then
fi.a = phi(a) & fi.b = phi(b) by A27,ORDINAL1:10;
hence thesis by A1,A30;
end; then
A31: sup fi = lim fi by A27,A28,ORDINAL4:8
.= phi(sup phi) by A29,ORDINAL2:def 10;
A32: sup fi c= sup phi
proof
let x be Ordinal;
assume
A33: x in sup fi;
reconsider A = x as Ordinal;
consider b such that
A34: b in rng fi & A c= b by A33,ORDINAL2:21;
consider y being object such that
A35: y in dom fi & b = fi.y by A34,FUNCT_1:def 3;
reconsider y as Ordinal by A35;
consider c such that
A36: c in rng phi & y c= c by A27,A35,ORDINAL2:21;
consider z being object such that
A37: z in dom phi & c = phi.z by A36,FUNCT_1:def 3;
reconsider z as Ordinal by A37;
succ z in omega by A4,A37,ORDINAL1:28; then
A38: phi.succ z = phi(c) & phi.succ z in rng phi & b = phi(y)
by A4,A6,A27,A35,A37,FUNCT_1:def 3;
y c< c iff y <> c & y c= c; then
phi(y) in phi(c) or y = c by A1,A36,ORDINAL1:11; then
b c= phi(c) & phi(c) in sup phi by A38,ORDINAL1:def 2,ORDINAL2:19; then
b in sup phi by ORDINAL1:12;
hence thesis by A34,ORDINAL1:12;
end;
phi.0 in rng phi by A4,FUNCT_1:def 3; then
a() in phi.0 & phi.0 in sup phi by A12,ORDINAL2:19; then
a() in sup phi by ORDINAL1:10;
hence contradiction by A11,A31,A32,ORDINAL1:5;
end;
begin :: Epsilon numbers
definition
let a be Ordinal;
attr a is epsilon means :Def5:
exp(omega,a) = a;
end;
theorem Th33:
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
A3: a is non empty limit_ordinal;
let phi being Ordinal-Sequence such that
A4: dom phi = a & for b st b in a holds phi.b = phi(b);
phi is non-decreasing
proof
let b,c; assume
A5: b in c & c in dom phi; then
phi.b = phi(b) & phi.c = phi(c) by A4,ORDINAL1:10; then
phi.b in phi.c by A5,ORDINAL4:24;
hence thesis by ORDINAL1:def 2;
end; then
Union phi is_limes_of phi & phi(a) = lim phi by A3,A4,Th6,ORDINAL2:45;
hence phi(a) is_limes_of phi by ORDINAL2:def 10;
end;
consider b such that
A6: a in b & phi(b) = b from CriticalNumber3(A1,A2);
take b; thus a in b by A6;
thus exp(omega, b) = b by A6;
end;
registration
cluster epsilon for Ordinal;
existence
proof
ex a st 0 in a & a is epsilon by Th33;
hence thesis;
end;
end;
definition
let a be Ordinal;
func first_epsilon_greater_than a -> epsilon Ordinal means:
Def6:
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 Th33;
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;
end;
theorem
a c= b implies first_epsilon_greater_than a c= first_epsilon_greater_than b
proof assume
A1: a c= b;
b in first_epsilon_greater_than b by Def6; then
a in first_epsilon_greater_than b by A1,ORDINAL1:12;
hence thesis by Def6;
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
A1: 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 A1,ORDINAL1:10;
hence first_epsilon_greater_than a c= c by Def6;
end;
hence first_epsilon_greater_than b = first_epsilon_greater_than a
by A1,Def6;
end;
theorem Th36:
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
A3: a is non empty limit_ordinal;
let phi being Ordinal-Sequence such that
A4: dom phi = a & for b st b in a holds phi.b = phi(b);
phi is non-decreasing
proof
let b,c; assume
A5: b in c & c in dom phi; then
phi.b = phi(b) & phi.c = phi(c) by A4,ORDINAL1:10; then
phi.b in phi.c by A5,ORDINAL4:24;
hence thesis by ORDINAL1:def 2;
end; then
Union phi is_limes_of phi & phi(a) = lim phi by A3,A4,Th6,ORDINAL2:45;
hence phi(a) is_limes_of phi by ORDINAL2:def 10;
end;
deffunc F(Ordinal,Ordinal) = phi($2);
deffunc G(Ordinal,Ordinal-Sequence) = lim $2;
consider f being Ordinal-Sequence such that
A6: dom f = omega and
A7: 0 in omega implies f.0 = 1 and
A8: for a st succ a in omega holds f.(succ a) = F(a,f.a) and
for a st a in omega & a <> 0 & a is limit_ordinal
holds f.a = G(a,f|a) from ORDINAL2:sch 11;
A9: dom f = omega & f.0 = 1 by A6,A7;
A10: for a st a in omega holds f.(succ a) = phi(f.a) by A8,ORDINAL1:28;
A11: 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,A9,A10);
Union f is epsilon
by A11; then
reconsider e = Union f as epsilon Ordinal;
defpred I[Nat] means f.$1 = omega |^|^ $1;
A12: I[0] by A7,Th13;
A13: for n st I[n] holds I[n+1]
proof
let n such that
A14: I[n];
A15: Segm(n+1) = succ Segm n & n in omega by NAT_1:38,ORDINAL1:def 12;
hence f.(n+1) = phi(f.n) by A10 .= omega |^|^ (n+1) by A14,A15,Th14;
end;
A16: for n holds I[n] from NAT_1:sch 2(A12,A13); then
for c st c in omega holds f.c = omega |^|^ c; then
A17: omega |^|^ omega = lim f by A6,Th15;
f is non-decreasing
proof
let a,b; assume
A18: a in b & b in dom f; then
reconsider n = a, m = b as Element of omega by A6,ORDINAL1:10;
a c= b by A18,ORDINAL1:def 2; then
omega |^|^ a c= omega |^|^ b by Th21; then
f.n c= omega |^|^ m by A16;
hence thesis by A16;
end; then
e is_limes_of f by A6,Th6; then
A19: omega |^|^ omega = e by A17,ORDINAL2:def 10;
A20: succ 0 = 1; then
A21: 0 in 1 by ORDINAL1:6;
now let b be epsilon Ordinal;
assume 0 in b; then
1 c= b & phi(b) = b by A20,Def5,ORDINAL1:21;
hence e c= b by A11;
end;
hence thesis by A19,A21,Def6,A11;
end;
theorem Th37:
for e being epsilon Ordinal holds omega in e
proof
let e be epsilon Ordinal;
A1: exp(omega, e) = e by Def5;
A2: exp(omega,0) = 1 & exp(omega,1) = omega & 1 in omega
by ORDINAL2:43,46; then
A3: e <> 0 & e <> 1 & succ 0 = 1 & succ 1 = 2 by Def5; then
0 in e by ORDINAL3:8; then
1 c= e by A3,ORDINAL1:21; then
1 c< e by A3; then
1 in e by ORDINAL1:11;
hence thesis by A1,A2,ORDINAL4:24;
end;
registration
cluster epsilon -> non empty limit_ordinal for Ordinal;
coherence
proof
let e be Ordinal such that
A1: e is epsilon;
exp(omega,0) = 1 by ORDINAL2:43;
hence e is non empty by A1; then
0 in e & exp(omega, e) = e by A1,ORDINAL3:8;
hence thesis by Th9;
end;
end;
theorem Th38:
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_2:74
.= exp(omega, exp(e, omega)*^exp(e, 1)) by ORDINAL4:30
.= exp(omega, exp(e, omega)*^e) by ORDINAL2:46
.= exp(exp(omega, e), exp(e, omega)) by ORDINAL4:31
.= exp(e, exp(e, omega)) by Def5;
end;
theorem Th39:
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
A1: 0 in n;
0 in e by ORDINAL3:8; then
omega in e & e c= e|^|^n by A1,Th23,Th37; then
A2: omega c= e|^|^n by ORDINAL1:def 2;
thus e |^|^ (n+2) = e|^|^Segm(n+1+1)
.= e|^|^succ Segm(n+1) by NAT_1:38
.= exp(e, e|^|^(n+1)) by Th14
.= exp(exp(omega, e), e|^|^(n+1)) by Def5
.= exp(omega, (e|^|^Segm(n+1))*^e) by ORDINAL4:31
.= exp(omega, (e|^|^succ Segm n)*^e) by NAT_1:38
.= exp(omega, exp(e, e|^|^n)*^e) by Th14
.= exp(omega, exp(e, e|^|^n)*^exp(e,1)) by ORDINAL2:46
.= exp(omega, exp(e, 1+^e|^|^n)) by ORDINAL4:30
.= exp(omega, exp(e, e|^|^n)) by A2,CARD_2:74
.= exp(omega, e|^|^succ Segm n) by Th14
.= exp(omega, e |^|^ Segm(n+1)) by NAT_1:38
.= exp(omega, e |^|^ (n+1));
end;
theorem Th40:
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
A3: a is non empty limit_ordinal;
let phi being Ordinal-Sequence such that
A4: dom phi = a & for b st b in a holds phi.b = phi(b);
phi is non-decreasing
proof
let b,c; assume
A5: b in c & c in dom phi; then
phi.b = phi(b) & phi.c = phi(c) by A4,ORDINAL1:10; then
phi.b in phi.c by A5,ORDINAL4:24;
hence thesis by ORDINAL1:def 2;
end; then
Union phi is_limes_of phi & phi(a) = lim phi by A3,A4,Th6,ORDINAL2:45;
hence phi(a) is_limes_of phi by ORDINAL2:def 10;
end;
deffunc F(Ordinal,Ordinal) = phi($2);
deffunc G(Ordinal,Ordinal-Sequence) = lim $2;
consider f being Ordinal-Sequence such that
A6: dom f = omega and
A7: 0 in omega implies f.0 = succ e and
A8: for a st succ a in omega holds f.(succ a) = F(a,f.a) and
for a st a in omega & a <> 0 & a is limit_ordinal
holds f.a = G(a,f|a) from ORDINAL2:sch 11;
A9: dom f = omega & f.0 = succ e by A6,A7;
A10: for a st a in omega holds f.(succ a) = phi(f.a) by A8,ORDINAL1:28;
A11: 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,A9,A10);
Union f is epsilon
by A11; then
reconsider e9 = Union f as epsilon Ordinal;
A12: now e in succ e by ORDINAL1:6;
hence e in e9 by A11;
let b be epsilon Ordinal; assume e in b; then
succ e c= b & phi(b) = b by Def5,ORDINAL1:21;
hence e9 c= b by A11;
end;
A13: succ 0 = 1 & succ 1 = 2 & succ 2 = 3; then
A14: f.1 = phi(succ e) by A7,A8 .= omega*^phi(e) by ORDINAL2:44
.= omega*^e by Def5; then
A15: f.2 = phi(omega*^e) by A13,A8 .= exp(phi(e), omega) by ORDINAL4:31
.= exp(e, omega) by Def5; then
A16: f.3 = phi(exp(e, omega)) by A13,A8 .= exp(e, exp(e, omega)) by Th38;
A17: e|^|^0 = 1 & e|^|^1 = e & e|^|^2 = exp(e, e) by Th13,Th16,Th18;
omega in e & 1 in omega by Th37; then
A18: 1 in e by ORDINAL1:10; then
exp(e,1) in exp(e, e) & exp(e,1) in exp(e, omega) by ORDINAL4:24; then
A19: e in exp(e, e) & e in exp(e, omega) by ORDINAL2:46;
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 A17,A18,Th24,Th9,ORDINAL3:8; then
A20: I[0] by A7,A14,A17,ORDINAL1:28,ORDINAL3:32;
A21: for n st I[n] holds I[n+1]
proof
let n such that
A22: I[n];
A23: Segm(n+1) = succ Segm n & Segm(n+1+1) = succ Segm(n+1) &
n in omega & n+1 in omega
by NAT_1:38,ORDINAL1:def 12; then
A24: f.(n+1) = phi(f.n) & f.(n+1+1) = phi(f.(n+1)) by A10;
thus e|^|^(n+1) in f.(n+1+1)
proof
per cases by NAT_1:23;
suppose n = 0;
hence thesis by A15,Th16,A19;
end;
suppose n = 1;
hence thesis by A16,A17,A18,A19,ORDINAL4:24;
end;
suppose n >= 2; then
consider k being Nat such that
A25: n = 2+k by NAT_1:10;
0 in Segm(k+1) & k+2 = k+1+1 by NAT_1:44; then
phi(e|^|^(k+2)) = e|^|^(k+1+2) by Th39;
hence thesis by A24,A25,A22,ORDINAL4:24;
end;
end;
0 in Segm(n+1) & n+2 = n+1+1 by NAT_1:44; then
phi(e|^|^(n+2)) = e|^|^(n+1+2) by Th39; then
phi(f.n) in e|^|^(n+1+2) by A22,ORDINAL4:24;
hence f.(n+1) in e|^|^(n+1+2) by A23,A10;
end;
A26: for n holds I[n] from NAT_1:sch 2(A20,A21);
deffunc G(Ordinal) = e|^|^$1;
consider g being Ordinal-Sequence such that
A27: dom g = omega & for a st a in omega holds g.a = G(a) from ORDINAL2:sch 3;
A28: e |^|^ omega = lim g by A27,Th15;
1 in omega & omega in e by Th37; then
1 in e by ORDINAL1:10; then
g is increasing Ordinal-Sequence by A27,Th25; then
Union g is_limes_of g by A27,Th6; then
A29: e |^|^ omega = Union g by A28,ORDINAL2:def 10;
e9 = Union g
proof
thus e9 c= Union g
proof
let x be Ordinal; assume x in e9; then
consider a being object such that
A30: a in dom f & x in f.a by CARD_5:2;
reconsider a as Element of omega by A6,A30;
f.a in e|^|^(a+2) & g.(a+2) = G(a+2) by A26,A27; then
f.a in Union g by A27,CARD_5:2;
hence thesis by A30,ORDINAL1:10;
end;
let x be Ordinal; assume x in Union g; then
consider a being object such that
A31: a in dom g & x in g.a by CARD_5:2;
reconsider a as Element of omega by A27,A31;
a+1 in omega & e|^|^a in f.(a+1) & g.a = G(a) by A26,A27; then
g.a in Union f by A6,CARD_5:2;
hence thesis by A31,ORDINAL1:10;
end;
hence thesis by A12,A29,Def6;
end;
definition
let a be Ordinal;
func epsilon_a -> Ordinal means:
:: equals omega |^|^ exp(omega, 1+^a); :: wg wikipedii, ale to nie prawda
Def7:
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.0 = 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 <> 0 & 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.0 = 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 <> 0 & 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.0 = 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 <> 0 & C is limit_ordinal
holds fi.C = D(C,fi|C) ) holds A1 = A2 from ORDINAL2:sch 13;
hence thesis;
end;
end;
theorem Th41:
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.0 = 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 <> 0 & c is limit_ordinal
holds fi.c = D(c,fi|c) by Def7;
thus F(0) = omega|^|^omega from ORDINAL2:sch 14(A1);
end;
theorem Th42:
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.0 = 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 <> 0 & c is limit_ordinal
holds fi.c = D(c,fi|c) by Def7;
for b holds F(succ b) = C(b,F(b)) from ORDINAL2:sch 15(A1);
hence thesis;
end;
theorem Th43:
b <> 0 & 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 <> 0 & 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.0 = 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 <> 0 & c is limit_ordinal
holds fi.c = D(c,fi|c) by Def7;
thus F(b) = D(b,fi) from ORDINAL2:sch 16(A4,A1,A2,A3);
end;
theorem Th44:
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 Th26,Th41; then
A1: P[0] by ORDINAL1:10;
A2: P[c] implies P[succ c] proof assume
A3: P[c];
A4: epsilon_succ c = (epsilon_c) |^|^ omega by Th42; then
A5: epsilon_c in epsilon_succ c by A3,Th26;
hence 1 in epsilon_succ c by A3,ORDINAL1:10;
let a,b; assume
A6: a in b & b c= succ c; then
a c= c by ORDINAL1:22; then
A7: b = succ c & (a = c or a c< c) or b c< succ c by A6;
per cases by A7,ORDINAL1:11;
suppose b in succ c; then
b c= c by ORDINAL1:22;
hence thesis by A3,A6;
end;
suppose
A8: b = succ c & a in c; then
epsilon_a in epsilon_c by A3;
hence thesis by A5,A8,ORDINAL1:10;
end;
suppose
b = succ c & a = c;
hence thesis by A3,A4,Th26;
end;
end;
A9: c <> 0 & c is limit_ordinal & (for b st b in c holds P[b]) implies P[c]
proof assume that
A10: c <> 0 & c is limit_ordinal and
A11: for b st b in c holds P[b];
deffunc F(Ordinal) = epsilon_$1;
consider f such that
A12: 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
A13: a in b & b in dom f; then
a in c by A12,ORDINAL1:10; then
f.a = F(a) & f.b = F(b) & P[b] by A11,A12,A13;
hence thesis by A13;
end; then
Union f is_limes_of f by A10,A12,Th6; then
A14: Union f = lim f by ORDINAL2:def 10 .= epsilon_c by A10,A12,Th43;
A15: 0 in c by A10,ORDINAL3:8; then
1 in epsilon_0 & f.0 = F(0) by A11,A12;
hence 1 in epsilon_c by A12,A14,A15,CARD_5:2;
let a,b; assume
A16: a in b & b c= c; then
A17: b = c or b c< c;
per cases by A17,ORDINAL1:11;
suppose b in c;
hence epsilon_a in epsilon_b by A11,A16;
end;
suppose
A18: b = c;
succ a in c & a in succ a by A10,A16,ORDINAL1:6,28; then
A19: F(a) in F(succ a) & F(succ a) = f.succ a & f.succ a in rng f
by A11,A12,FUNCT_1:def 3; then
f.succ a c= Union f by ZFMISC_1:74;
hence thesis by A14,A18,A19;
end;
end;
P[c] from ORDINAL2:sch 1(A1,A2,A9);
hence thesis;
end;
theorem Th45:
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:10;
hence thesis by A2,Th44;
end;
theorem Th46:
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
A1: b <> {} & b is limit_ordinal;
let f; assume
A2: dom f = b & for c st c in b holds f.c = epsilon_c; then
f is increasing Ordinal-Sequence by Th45; then
Union f is_limes_of f by A1,A2,Th6; then
Union f = lim f by ORDINAL2:def 10;
hence thesis by A1,A2,Th43;
end;
theorem Th47:
b is non empty limit_ordinal implies
(x in epsilon_b iff ex c st c in b & x in epsilon_c)
proof assume
A1: b is non empty limit_ordinal;
deffunc F(Ordinal) = epsilon_$1;
consider f such that
A2: dom f = b & for c st c in b holds f.c = F(c) from ORDINAL2:sch 3;
A3: Union f = epsilon_b by A1,A2,Th46;
hereby assume x in epsilon_b; then
consider c being object such that
A4: c in dom f & x in f.c by A3,CARD_5:2;
reconsider c as Ordinal by A4;
take c;
thus c in b by A2,A4;
thus x in epsilon_c by A2,A4;
end;
given c such that
A5: c in b & x in epsilon_c;
f.c = F(c) by A2,A5;
hence x in epsilon_b by A2,A3,A5,CARD_5:2;
end;
theorem Th48:
a c= epsilon_a
proof
defpred P[Ordinal] means $1 c= epsilon_$1;
A1: P[0];
A2: P[b] implies P[succ b] proof assume
A3: P[b];
epsilon_b in epsilon_succ b by Th44,ORDINAL1:6; then
b in epsilon_succ b by A3,ORDINAL1:12;
hence thesis by ORDINAL1:21;
end;
A4: c <> 0 & c is limit_ordinal & (for b st b in c holds P[b]) implies P[c]
proof assume that
c <> 0 & c is limit_ordinal and
A5: for b st b in c holds P[b];
let x be Ordinal; assume
A6: x in c;
reconsider a = x as Ordinal;
P[a] & epsilon_a in epsilon_c by A5,A6,Th44;
hence thesis by ORDINAL1:12;
end;
P[b] from ORDINAL2:sch 1(A1,A2,A4);
hence thesis;
end;
theorem Th49:
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
A1: 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 epsilon-transitive epsilon-connected set
by ORDINAL1:23;
now
let b; assume b in a; then
consider x being set such that
A2: b in x & x in X by TARSKI:def 4;
reconsider x as epsilon Ordinal by A2,A1;
succ b in x by A2,ORDINAL1:28;
hence succ b in a by A2,TARSKI:def 4;
end; then
A3: a is limit_ordinal by ORDINAL1:28;
set z = the Element of X;
ex e being epsilon Ordinal st z in e & e in X by A1; then
A4: a <> {} by TARSKI:def 4;
a is epsilon
proof
thus exp(omega,a) c= a
proof
let x be Ordinal; assume x in exp(omega,a); then
consider b such that
A5: b in a & x in exp(omega,b) by A3,A4,Th11;
consider y being set such that
A6: b in y & y in X by A5,TARSKI:def 4;
reconsider y as epsilon Ordinal by A1,A6;
exp(omega,b) in exp(omega,y) by A6,ORDINAL4:24; then
exp(omega,b) in y by Def5; then
x in y by A5,ORDINAL1:10;
hence thesis by A6,TARSKI:def 4;
end;
thus thesis by ORDINAL4:32;
end;
hence thesis;
end;
theorem Th50:
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
A1: for x st x in X holds x is epsilon Ordinal and
A2: for a st a in X holds first_epsilon_greater_than a in X;
now
let x; assume
A3: x in X;
hence x is epsilon Ordinal by A1;
reconsider a = x as Ordinal by A1,A3;
take e = first_epsilon_greater_than a;
thus x in e & e in X by A2,A3,Def6;
end;
hence union X is epsilon Ordinal by Th49;
end;
registration
let a;
cluster epsilon_a -> epsilon;
coherence
proof
deffunc phi(Ordinal) = epsilon_$1;
defpred P[Ordinal] means phi($1) is epsilon;
A1: P[0] by Th36,Th41;
A2: P[b] implies P[succ b]
proof
assume P[b]; then
first_epsilon_greater_than epsilon_b = (epsilon_b)|^|^omega by Th40
.= epsilon_(succ b) by Th42;
hence thesis;
end;
A3: b <> 0 & b is limit_ordinal & (for c st c in b holds P[c]) implies P[b]
proof assume that
A4: b <> 0 & b is limit_ordinal and
A5: for c st c in b holds P[c];
consider f such that
A6: dom f = b & for c st c in b holds f.c = phi(c) from ORDINAL2:sch 3;
A7: phi(b) = Union f by A4,A6,Th46;
set X = rng f;
0 in b by A4,ORDINAL3:8; then f.0 in rng f by A6,FUNCT_1:def 3; then
reconsider X as non empty set;
A8: now let x; assume x in X; then
consider a being object such that
A9: a in dom f & f.a = x by FUNCT_1:def 3;
reconsider a as Ordinal by A9;
x = phi(a) by A6,A9;
hence x is epsilon Ordinal by A5,A6,A9;
end;
now let x be Ordinal; assume
A10: x in X; then
consider a being object such that
A11: a in dom f & f.a = x by FUNCT_1:def 3;
reconsider a as Ordinal by A11;
A12: succ a in b by A4,A6,A11,ORDINAL1:28;
reconsider e = x as epsilon Ordinal by A8,A10;
e = phi(a) by A6,A11; then
first_epsilon_greater_than e = phi(a)|^|^omega by Th40
.= phi(succ a) by Th42 .= f.succ a by A6,A12;
hence first_epsilon_greater_than x in X by A6,A12,FUNCT_1:def 3;
end;
hence P[b] by A7,A8,Th50;
end;
for a holds P[a] from ORDINAL2:sch 1(A1,A2,A3);
hence thesis;
end;
end;
::$N The ordinal indexing of epsilon numbers
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];
A1: Q[0]
proof
let e be epsilon Ordinal;
0 in e by ORDINAL3:8; then
first_epsilon_greater_than 0 c= e by Def6; then
e in epsilon_0 implies e in e by Th36,Th41;
hence thesis;
end;
A2: Q[c] implies Q[succ c] proof assume
A3: Q[c];
let e be epsilon Ordinal such that
A4: e in epsilon_succ c;
A5: epsilon_succ c = (epsilon_c)|^|^omega by Th42
.= first_epsilon_greater_than epsilon_c by Th40;
per cases by ORDINAL1:14;
suppose e in epsilon_c;
hence N[e] by A3;
end;
suppose e = epsilon_c;
hence N[e];
end;
suppose epsilon_c in e; then
epsilon_succ c c= e by A5,Def6; then
e in e by A4;
hence N[e];
end;
end;
A6: b <> 0 & b is limit_ordinal & (for c st c in b holds Q[c]) implies Q[b]
proof assume that
A7: b <> 0 & b is limit_ordinal and
A8: 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 A7,Th47;
hence N[e] by A8;
end;
A9: Q[b] from ORDINAL2:sch 1(A1,A2,A6);
a c= epsilon_a & epsilon_a in epsilon_succ a by Th44,Th48,ORDINAL1:6;
hence thesis by A9,ORDINAL1:12;
end;
begin :: Cantor Normal Form
definition
let A be finite Ordinal-Sequence; :: why finite?
func Sum^ A -> Ordinal means:
Def8:
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;
A1: (ex F being Ordinal,fi being Ordinal-Sequence
st F = last fi & dom fi = succ b & fi.0 = 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 <> 0 & 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 = 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 <> 0 & 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 = 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 <> 0 & 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:21; then
succ n in succ b & Segm(n+1) = succ Segm n by NAT_1:38,ORDINAL1:22;
hence f.(n+1) = f.n +^ A.n by A2;
end;
let a1,a2 be Ordinal;
given f1 being Ordinal-Sequence such that
A3: 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
A4: 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;
A5: 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
A6: c in b by ORDINAL3:3; then
reconsider n = c as Element of omega;
A7: Segm(n+1) = succ Segm n by NAT_1:38;
f1.(n+1) = C(n,f1.n) by A3,A6;
hence thesis by A7;
end;
A8: for c being Ordinal st c in succ b & c <> {} & c is limit_ordinal
holds f1.c = D(c,f1|c)
proof
A9: succ b in omega by ORDINAL1:def 12;
let c be Ordinal;
assume
A10: c in succ b & c <> {} & c is limit_ordinal; then
0 in c by ORDINAL3:8; then
c in omega & omega c= c by A10,ORDINAL1:10,def 11,A9;
hence f1.c = D(c,f1|c);
end;
A11: 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
A12: c in b by ORDINAL3:3; then
reconsider n = c as Element of omega;
A13: Segm(n+1) = succ Segm n by NAT_1:38;
f2.(n+1) = C(n,f2.n) by A4,A12;
hence thesis by A13;
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;
A14: succ b in omega by ORDINAL1:def 12;
assume
A15: c in succ b & c <> {} & c is limit_ordinal; then
0 in c by ORDINAL3:8; then
c in omega & omega c= c by A15,ORDINAL1:10,def 11,A14;
hence thesis;
end;
hence thesis by A1,A3,A4,A5,A8,A11;
end;
end;
theorem Th52:
Sum^ {} = 0
proof
reconsider A = {} as finite Ordinal-Sequence;
consider f being Ordinal-Sequence such that
A1: Sum^ A = last f and
A2: dom f = succ dom A and
A3: f.0 = 0 and
for n being Nat st n in dom A holds f.(n+1) = f.n +^ A.n by Def8;
dom f = succ 0 implies last f = f.0 by ORDINAL2:6;
hence Sum^ {} = 0 by A1,A2,A3;
end;
theorem Th53:
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 Def8;
A2: dom <%a%> = 1 & <%a%>.0 = a by AFINSQ_1:def 4;
0 in Segm 1 by NAT_1:44; then
f.(0+1) = (0 qua Ordinal) +^ a by A1,A2 .= a by ORDINAL2:30;
hence thesis by A1,A2,ORDINAL2:6;
end;
theorem Th54:
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 Def8;
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 Def8;
dom <%a%> = 1 by AFINSQ_1:def 4; then
A3: dom (A^<%a%>) = (dom A)+^1 & (dom A)+^1 = succ dom A
by ORDINAL2:31,ORDINAL4:def 1;
reconsider dA = dom A as Element of NAT by ORDINAL1:def 12;
A4: dom A in succ dom A by ORDINAL1:6;
defpred P[Nat] means $1 in succ dom A implies f.$1 = g.$1;
A5: P[0] by A1,A2;
A6: P[n] implies P[n+1] proof assume that
A7: P[n] and
A8: n+1 in succ dom A;
Segm(n+1) = succ Segm n by NAT_1:38; then
A9: n in dom A by A8,ORDINAL3:3; then
n in succ dom A by A4,ORDINAL1:10; then
g.(n+1) = g.n +^ A.n & f.(n+1) = f.n+^(A^<%a%>).n by A1,A2,A3,A9;
hence thesis by A7,A9,A4,ORDINAL1:10,ORDINAL4:def 1;
end;
A10: P[n] from NAT_1:sch 2(A5,A6);
thus Sum^ (A^<%a%>) = f.((dom A)+^1) by A1,A3,ORDINAL2:6
.= f.(dA+1) by CARD_2:36
.= f.(dom A)+^(A^<%a%>).len A by A1,A3,ORDINAL1:6
.= f.(dom A) +^ a by AFINSQ_1:36
.= g.(dom A) +^ a by A10,ORDINAL1:6
.= (Sum^ A) +^ a by A2,ORDINAL2:6;
end;
theorem Th55:
for A being finite Ordinal-Sequence holds Sum^ (<%a%>^A) = a +^ Sum^ A
proof
defpred P[finite Sequence] means
for f being finite Ordinal-Sequence st f = $1
holds Sum^(<%a%>^f) = a +^ Sum^ f;
Sum^(<%a%>^{}) = a by Th53; then
A1: P[{}] by Th52,ORDINAL2:27;
A2: for f being finite Sequence, x being object st P[f] holds P[f^<%x%>]
proof
let f be finite Sequence;
let x be object; assume
A3: P[f];
let g be finite Ordinal-Sequence;
consider b such that
A4: rng g c= b by ORDINAL2:def 4;
assume
A5: g = f^<%x%>; then
rng g = (rng f)\/rng<%x%> by AFINSQ_1:26; then
A6: rng f c= b & rng <%x%> c= b by A4,XBOOLE_1:11; then
reconsider f9 = f as finite Ordinal-Sequence by ORDINAL2:def 4;
rng <%x%> = {x} by AFINSQ_1:33; then
x in b by A6,ZFMISC_1:31; then
reconsider x as Ordinal;
thus Sum^(<%a%>^g) = Sum^ (<%a%>^f9^<%x%>) by A5,AFINSQ_1:27
.= Sum^ (<%a%>^f9) +^ x by Th54
.= a +^ Sum^ f9 +^ x by A3
.= a +^ (Sum^ f9 +^ x) by ORDINAL3:30
.= a +^ Sum^ g by A5,Th54;
end;
for f being finite Sequence holds P[f] from AFINSQ_1:sch 3(A1,A2);
hence thesis;
end;
theorem Th56:
for A being finite Ordinal-Sequence holds A.0 c= Sum^ A
proof
let A be finite Ordinal-Sequence;
defpred P[finite Sequence] means
for A being finite Ordinal-Sequence st $1 = A holds A.0 c= Sum^ A;
A1: P[{}];
A2: for f being finite Sequence, x being object st P[f] holds P[f^<%x%>]
proof
let f be finite Sequence;
let x be object; assume
A3: P[f];
let g be finite Ordinal-Sequence;
consider b such that
A4: rng g c= b by ORDINAL2:def 4;
assume
A5: g = f^<%x%>; then
rng g = (rng f)\/rng<%x%> by AFINSQ_1:26; then
A6: rng f c= b & rng <%x%> c= b by A4,XBOOLE_1:11; then
reconsider f9 = f as finite Ordinal-Sequence by ORDINAL2:def 4;
rng <%x%> = {x} by AFINSQ_1:33; then
x in b by A6,ZFMISC_1:31; then
reconsider x as Ordinal;
per cases;
suppose f = {}; then
g = {}^<%x%> by A5;
then g = <%x%>;
then g.0 = x & Sum^ g = x by Th53;
hence g.0 c= Sum^ g;
end;
suppose f <> {}; then
0 in dom f9 & Sum^ g = Sum^ f9 +^ x by A5,Th54,ORDINAL3:8; then
g.0 = f9.0 & f9.0 c= Sum^ f9 & Sum^ f9 c= Sum^ g
by A3,A5,ORDINAL3:24,ORDINAL4:def 1;
hence g.0 c= Sum^ g;
end;
end;
for f being finite Sequence holds P[f] from AFINSQ_1:sch 3(A1,A2);
hence A.0 c= Sum^ A;
end;
definition
let a;
attr a is Cantor-component means :Def9:
ex b,n st 0 in Segm n & a = n*^exp(omega,b);
end;
registration
cluster Cantor-component -> non empty for Ordinal;
coherence
proof
let a;
given b,n such that
A1: 0 in Segm n & a = n*^exp(omega,b);
exp(omega,b) <> 0 by ORDINAL4:22;
hence thesis by A1,ORDINAL3:31;
end;
end;
registration
cluster Cantor-component for Ordinal;
existence
proof
take 1*^exp(omega,1), 1, 1;
thus thesis by NAT_1:44;
end;
end;
definition
let a,b;
func b-exponent(a) -> Ordinal means :Def10:
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
A1: 1 in b & 0 in a;
defpred P[Ordinal] means a c= exp(b,$1);
a c= exp(b,a) by A1,ORDINAL4:32; then
A2: ex c st P[c];
consider c such that
A3: P[c] & for d st P[d] holds c c= d from ORDINAL1:sch 1(A2);
0 in Segm 1 by NAT_1:44; then
A4: 0 in b by A1,ORDINAL1:10;
per cases by A3;
suppose
A5: a = exp(b,c);
take c; thus exp(b,c) c= a by A5;
let d; assume
A6: exp(b,d) c= a & d c/= c; then
c in d by ORDINAL1:16; then
a in exp(b,d) by A1,A5,ORDINAL4:24; then
a in a by A6;
hence contradiction;
end;
suppose
A7: a c< exp(b,c); then
A8: a in exp(b,c) by ORDINAL1:11;
succ 0 c= a by A1,ORDINAL1:21; then
1 in exp(b,c) & exp(b,0) = 1 by A7,ORDINAL1:11,12,ORDINAL2:43; then
A9: c <> 0;
now assume c is limit_ordinal; then
consider d such that
A10: d in c & a in exp(b,d) by A9,A4,A8,Th11;
P[d] by A10,ORDINAL1:def 2; then
c c= d by A3; then
d in d by A10;
hence contradiction;
end; then
consider d such that
A11: c = succ d by ORDINAL1:29;
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 A3; then
d in d by A11,ORDINAL1:21;
hence thesis;
end;
let e; assume
A12: exp(b,e) c= a & e c/= d; then
d in e by ORDINAL1:16; then
c c= e by A11,ORDINAL1:21; then
exp(b,c) c= exp(b,e) by A1,ORDINAL4:27; then
a in exp(b,e) by A8; then
a in a by A12;
hence contradiction;
end;
end;
thus thesis;
end;
uniqueness;
consistency;
end;
Lm1: 0 in Segm 1 by NAT_1:44;
theorem Th57:
1 in b implies a in exp(b, succ(b-exponent(a))) proof assume
A1: 1 in b;
per cases by ORDINAL3:8;
suppose
A2: 0 in a; assume not thesis; then
exp(b, succ(b-exponent(a))) c= a by ORDINAL1:16; then
succ(b-exponent(a)) c= b-exponent(a) &
b-exponent(a) in succ(b-exponent(a)) by A1,A2,Def10,ORDINAL1:6; then
b-exponent(a) in b-exponent(a);
hence contradiction;
end;
suppose
A3: a = 0; then
b-exponent(a) = 0 by Def10; then
exp(b, succ(b-exponent(a))) = b by ORDINAL2:46;
hence thesis by A1,A3,Lm1,ORDINAL1:10;
end;
end;
registration
let a, b be Ordinal;
cluster <% a,b %> -> Ordinal-yielding;
coherence
proof
<% a,b %> = <% a %> ^ <% b %> by AFINSQ_1:def 5;
hence thesis;
end;
let c be Ordinal;
cluster <% a,b,c %> -> Ordinal-yielding;
coherence
proof
<% a,b,c %> = <% a %> ^ <% b %> ^ <% c %> by AFINSQ_1:def 6;
hence thesis;
end;
end;
::: into ORDINAL3 ?
registration
let a be non empty Ordinal, b be Ordinal;
cluster a +^ b -> non empty;
coherence by ORDINAL3:26;
cluster b +^ a -> non empty;
coherence by ORDINAL3:26;
end;
::: into ORDINAL3 ?
registration
let a, b be non empty Ordinal;
cluster b *^ a -> non empty;
coherence by ORDINAL3:31;
end;
::: into ORDINAL4 ?
registration
let A be empty Ordinal, B be non empty Ordinal;
cluster exp(A,B) -> empty;
coherence by ORDINAL4:20;
end;
::: into ORDINAL4 ?
registration
let A be Ordinal, B be empty Ordinal;
cluster exp(A,B) -> non empty;
coherence by ORDINAL2:43;
end;
::: into ORDINAL4 ?
registration
let A be non empty Ordinal, B be Ordinal;
cluster exp(A,B) -> non empty;
coherence by ORDINAL4:22;
end;
theorem Th58:
for a, b, c being Ordinal
holds 0 in c & c in b implies b -exponent(c*^exp(b,a)) = a
proof
let a, b, c be Ordinal; assume
A1: 0 in c & c in b; then
A2: succ 0 c= c by ORDINAL1:21; then
A3: 1*^exp(b,a) = exp(b,a) & 1*^exp(b,a) c= c*^exp(b,a) by ORDINAL2:39,41;
A4: 1 in b & 0 in c*^exp(b,a) by A2,A1,ORDINAL1:12,ORDINAL3:8;
now let d be Ordinal; assume
A5: exp(b,d) c= c*^exp(b,a) & d c/= a; then
succ a c= d by ORDINAL1:16, ORDINAL1:21; then
A6: exp(b, succ a) c= exp(b, d) by A1,ORDINAL4:27;
exp(b, succ a) = b*^exp(b, a) by ORDINAL2:44; then
b*^exp(b, a) c= c*^exp(b,a) by A5,A6; then
b c= c by ORDINAL3:35; then
c in c by A1;
hence contradiction;
end;
hence b-exponent(c*^exp(b,a)) = a by A3,A4,Def10;
end;
theorem Th59:
0 in a & 1 in b & c = b-exponent a implies a div^ exp(b, c) in b proof assume
A1: 0 in a & 1 in b & c = b-exponent a;
set n = a div^ exp(b, c);
exp(b,c) <> 0 by A1; then
consider d such that
A2: a = n*^exp(b, c)+^d & d in exp(b, c) by ORDINAL3:def 6;
assume not n in b; then
b*^exp(b,c) c= n*^exp(b,c) by ORDINAL1:16,ORDINAL2:41; then
exp(b, succ c) c= n*^exp(b,c) & n*^exp(b,c) c= a
by A2,ORDINAL2:44,ORDINAL3:24; then
exp(b, succ c) c= a; then
succ c c= c & c in succ c by A1,Def10,ORDINAL1:6; then
c in c;
hence contradiction;
end;
theorem Th60:
0 in a & 1 in b & c = b-exponent a implies 0 in a div^ exp(b, c) proof assume
A1: 0 in a & 1 in b & c = b-exponent a;
set n = a div^ exp(b, c);
exp(b,c) <> 0 by A1; then
consider d such that
A2: a = n*^exp(b, c)+^d & d in exp(b, c) by ORDINAL3:def 6;
assume not 0 in n; then
n = 0 by ORDINAL3:8; then
a = (0 qua Ordinal)+^d by A2,ORDINAL2:35 .= d by ORDINAL2:30; then
exp(b, c) c= d by A1,Def10; then
d in d by A2;
hence contradiction;
end;
theorem Th61:
b <> 0 implies a mod^ exp(b, c) in exp(b, c) proof assume that
A1: b <> 0;
set n = a div^ exp(b, c);
exp(b,c) <> 0 by A1; then
consider d such that
A2: a = n*^exp(b, c)+^d & d in exp(b, c) by ORDINAL3:def 6;
d = a -^ n*^exp(b, c) by A2,ORDINAL3:52
.= a mod^ exp(b,c) by ORDINAL3:def 7;
hence thesis by A2;
end;
theorem Th62:
0 in a implies
ex n,c st a = n*^exp(omega, omega-exponent(a))+^c & 0 in Segm n &
c in exp(omega, omega-exponent(a))
proof assume
A1: 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 A1,Th59; then
reconsider n as Nat;
take n,b;
thus a = n*^exp(omega, c)+^b by ORDINAL3:65;
thus 0 in Segm n by A1,Th60;
thus b in exp(omega, c) by Th61;
end;
theorem Th63:
1 in c & c-exponent b in c-exponent a implies b in a proof assume
A1: 1 in c & c-exponent b in c-exponent a; then
succ(c-exponent(b)) c= c-exponent(a) by ORDINAL1:21; then
A2: exp(c, succ(c-exponent(b))) c= exp(c, c-exponent(a)) by A1,ORDINAL4:27;
A3: 0 in a by A1,Def10;
b in exp(c, succ(c-exponent(b))) by A1,Th57; then
b in exp(c, c-exponent(a)) & exp(c, c-exponent(a)) c= a by A1,A2,A3,Def10;
hence thesis;
end;
definition
let A be Ordinal-Sequence;
attr A is Cantor-normal-form means :Def11:
(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 for Ordinal-Sequence;
coherence;
cluster Cantor-normal-form -> non-empty for Ordinal-Sequence;
coherence
proof
let A be Ordinal-Sequence;
assume A1: A is Cantor-normal-form;
now
let x be object;
assume x in dom A;
then A.x is Cantor-component by A1;
hence A.x is non empty;
end;
hence thesis by FUNCT_1:def 9;
end;
cluster Cantor-normal-form -> decreasing for 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 Th63;
end;
end;
reserve A,B for Cantor-normal-form Ordinal-Sequence;
theorem
Sum^ A = 0 implies A = {} proof assume
A1: Sum^ A = 0 & A <> {}; then
0 in dom A by ORDINAL3:8; then
reconsider a = A.0 as Cantor-component Ordinal by Def11;
0 in a & a c= Sum^ A by Th56,ORDINAL3:8;
hence thesis by A1;
end;
theorem Th65:
0 in Segm n implies <%n*^exp(omega,b)%> is Cantor-normal-form
proof assume
A1: 0 in Segm n;
set A = <%n*^exp(omega,b)%>;
A2: dom A = Segm 1 & A.0 = n*^exp(omega,b) by AFINSQ_1:def 4;
hereby let a; assume a in dom A; then
a = 0 & 0 in Segm 1 by A2,ORDINAL3:15,TARSKI:def 1;
hence A.a is Cantor-component by A1;
end;
let a,b; assume
A3: a in b;
assume b in dom A;
hence omega-exponent(A.b) in omega-exponent(A.a)
by A3,A2,ORDINAL3:15,TARSKI:def 1;
end;
registration
cluster non empty Cantor-normal-form for Ordinal-Sequence;
existence
proof
take A = <%1*^exp(omega,1)%>;
thus A is non empty;
0 in Segm 1 by NAT_1:44;
hence thesis by Th65;
end;
end;
theorem Th66:
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
A1: for a st a in dom (A^B) holds (A^B).a is Cantor-component and
A2: for a,b st a in b & b in dom (A^B) holds
omega-exponent((A^B).b) in omega-exponent((A^B).a);
A3: dom (A^B) = (dom A)+^(dom B) by ORDINAL4:def 1; then
A4: dom A c= dom (A^B) by ORDINAL3:24;
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 A4,ORDINAL4:def 1;
hence A.a is Cantor-component by A1;
end;
let a,b; assume
A5: a in b & b in dom A; then
a in dom A by ORDINAL1:10; then
A.a = AB.a & A.b = AB.b & b in dom AB by A4,A5,ORDINAL4:def 1;
hence omega-exponent(A.b) in omega-exponent(A.a) by A2,A5;
end;
hereby let a; assume a in dom B; then
B.a = AB.((dom A)+^a) & (dom A)+^a in dom AB
by A3,ORDINAL3:17,ORDINAL4:def 1;
hence B.a is Cantor-component by A1;
end;
let a,b; assume
A6: a in b & b in dom B; then
a in dom B by ORDINAL1:10; 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 A3,A6,ORDINAL3:17,ORDINAL4:def 1;
hence omega-exponent(B.b) in omega-exponent(B.a) by A2;
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 12;
n+1 = 1+^n by CARD_2:36; then
consider S1,S2 such that
A2: A = S1^S2 & dom S1 = 1 & dom S2 = n by A1,Th2;
reconsider S1,S2 as Ordinal-Sequence by A2,Th4;
S1^S2 is Cantor-normal-form by A2; then
reconsider S1,S2 as Cantor-normal-form Ordinal-Sequence by Th66;
0 in Segm 1 by NAT_1:44; then
reconsider c = S1.0 as Cantor-component Ordinal by A2,Def11;
take c, S2;
len S1 = 1 by A2;
hence thesis by A2,AFINSQ_1:34;
end;
theorem Th68:
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
A1: omega-exponent(A.0) in omega-exponent(c);
set B = <%c%>^A;
A2: dom <%c%> = 1 & <%c%>.0 = c by AFINSQ_1:def 4; then
A3: dom B = 1 +^ dom A by ORDINAL4:def 1;
hereby let a;
assume
A4: a in dom B;
per cases by A3,A4,ORDINAL3:38;
suppose
A5: a in 1; then
a = 0 by ORDINAL3:15,TARSKI:def 1;
hence B.a is Cantor-component by A2,A5,ORDINAL4:def 1;
end;
suppose ex b st b in dom A & a = 1 +^b; then
consider b such that
A6: b in dom A & a = 1 +^b;
B.a = A.b by A2,A6,ORDINAL4:def 1;
hence B.a is Cantor-component by A6,Def11;
end;
end;
let a,b; assume
A7: a in b & b in dom B;
per cases;
suppose not a in 1; then
A8: 1 c= a by ORDINAL1:16; then
A9: 1 in b & a in dom B & (1+^dom A)-^1 = dom A
by A7,ORDINAL1:10,12,ORDINAL3:52; then
A10: b-^1 in dom A & a-^1 in dom A & a-^1 in b-^1 by A8,A3,A7,ORDINAL3:53;
b = 1+^(b-^1) & a = 1+^(a-^1) by A8,A9,ORDINAL3:51,def 5; then
B.a = A.(a-^1) & B.b = A.(b-^1) by A2,A10,ORDINAL4:def 1;
hence thesis by A10,Def11;
end;
suppose a in 1; then
A11: B.a = <%c%>.a & a = 0 by A2,ORDINAL3:15,ORDINAL4:def 1,TARSKI:def 1;
then
A12: succ 0 c= b by A7,ORDINAL1:21; then
b-^1 in (1+^dom A)-^1 by A3,A7,ORDINAL3:53; then
A13: b-^1 in dom A & b = 1+^(b-^1) by A12,ORDINAL3:52,def 5; then
A14: B.b = A.(b-^1) by A2,ORDINAL4:def 1;
0 in dom A & (b-^1 = 0 or 0 in b-^1) by ORDINAL3:8; then
omega-exponent(A.0) = omega-exponent(A.(b-^1)) or
omega-exponent(A.(b-^1)) in omega-exponent(A.0) by A13,Def11;
hence thesis by A1,A11,A14,ORDINAL1:10;
end;
end;
::$N Existence of Cantor Normal Form for ordinal numbers
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;
A1: for a st for b st b in a holds P[b] holds P[a] proof let a such that
A2: for b st b in a holds P[b] and
A3: 0 in a;
consider n,b such that
A4: a = n*^exp(omega, omega-exponent(a))+^b & 0 in Segm n &
b in exp(omega, omega-exponent(a)) by A3,Th62;
reconsider s = n*^exp(omega, omega-exponent(a)) as
Cantor-component Ordinal by A4,Def9;
set c = omega-exponent(a);
A5: exp(omega, c) c= a by A3,Def10;
per cases by ORDINAL3:8;
suppose
A6: b = 0;
reconsider A = <%n*^exp(omega, omega-exponent(a))%> as
non empty Cantor-normal-form Ordinal-Sequence by A4,Th65;
take A;
thus a = n*^exp(omega, omega-exponent(a)) by A4,A6,ORDINAL2:27
.= Sum^ A by Th53;
end;
suppose
0 in b; then
consider A being non empty Cantor-normal-form Ordinal-Sequence
such that
A7: b = Sum^ A by A5,A2,A4;
A8: A.0 in exp(omega, omega-exponent(a)) by A4,A7,Th56,ORDINAL1:12;
0 in dom A by ORDINAL3:8; then
A.0 is Cantor-component Ordinal by Def11; then
0 in A.0 by ORDINAL3:8; then
exp(omega, omega-exponent(A.0)) c= A.0 by Def10; then
A9: exp(omega, omega-exponent(A.0)) in exp(omega, omega-exponent(a))
by A8,ORDINAL1:12;
n in omega by ORDINAL1:def 12; then
omega-exponent(s) = omega-exponent(a) by A4,Th58; then
reconsider B = <%s%>^A as non empty Cantor-normal-form Ordinal-Sequence
by A9,Th68,Th12;
take B;
thus a = Sum^ B by A4,A7,Th55;
end;
end;
A10: P[b] from ORDINAL1:sch 2(A1);
per cases by ORDINAL3:8;
suppose
A11: a = 0;
reconsider A = {} as Cantor-normal-form Ordinal-Sequence;
take A;
thus thesis by A11,Th52;
end;
suppose 0 in a; then
ex A being non empty Cantor-normal-form Ordinal-Sequence st a = Sum^ A
by A10;
hence thesis;
end;
end;