:: Epsilon Numbers and Cantor Normal Form
:: by Grzegorz Bancerek
::
:: Received October 20, 2009
:: Copyright (c) 2009-2021 Association of Mizar Users

theorem Th1: :: ORDINAL5:1

for a, b being Ordinal holds
( not a c= succ b or a c= b or a = succ b ) by ORDINAL1:16, ORDINAL1:21;

registration

cluster omega -> limit_ordinal ;

coherence
omega is limit_ordinal ;

cluster empty -> empty Ordinal-yielding for set ;

coherence
for b₁ being empty set holds b₁ is Ordinal-yielding

proof end;

end;

registration

cluster Relation-like Function-like non empty Sequence-like finite for set ;

existence
ex b₁ being Sequence st
( not b₁ is empty & b₁ is finite )

proof end;

end;

registration

let f be Sequence;
let g be non empty Sequence;

cluster f ^ g -> non empty ;

coherence
not f ^ g is empty

proof end;

cluster g ^ f -> non empty ;

coherence
not g ^ f is empty

proof end;

end;

theorem Th2: :: ORDINAL5:2

for a, b being Ordinal
for S being Sequence st dom S = a +^ b holds
ex S1, S2 being Sequence st
( S = S1 ^ S2 & dom S1 = a & dom S2 = b )

proof end;

theorem Th3: :: ORDINAL5:3

for S1, S2 being Sequence holds
( rng S1 c= rng (S1 ^ S2) & rng S2 c= rng (S1 ^ S2) )

proof end;

theorem Th4: :: ORDINAL5:4

for S1, S2 being Sequence st S1 ^ S2 is Ordinal-yielding holds
( S1 is Ordinal-yielding & S2 is Ordinal-yielding )

proof end;

definition

let f be Sequence;

attr f is decreasing means :: ORDINAL5:def 1
for a, b being Ordinal st a in b & b in dom f holds
f . b in f . a;

attr f is non-decreasing means :Def2: :: ORDINAL5:def 2
for a, b being Ordinal st a in b & b in dom f holds
f . a c= f . b;

attr f is non-increasing means :: ORDINAL5:def 3
for a, b being Ordinal st a in b & b in dom f holds
f . b c= f . a;

end;

:: deftheorem defines decreasing ORDINAL5:def 1 :
for f being Sequence holds
( f is decreasing iff for a, b being Ordinal st a in b & b in dom f holds
f . b in f . a );

:: deftheorem Def2 defines non-decreasing ORDINAL5:def 2 :
for f being Sequence holds
( f is non-decreasing iff for a, b being Ordinal st a in b & b in dom f holds
f . a c= f . b );

:: deftheorem defines non-increasing ORDINAL5:def 3 :
for f being Sequence holds
( f is non-increasing iff for a, b being Ordinal st a in b & b in dom f holds
f . b c= f . a );

registration

cluster Relation-like Function-like Sequence-like Ordinal-yielding increasing -> non-decreasing for set ;

coherence
for b₁ being Ordinal-Sequence st b₁ is increasing holds
b₁ is non-decreasing

proof end;

cluster Relation-like Function-like Sequence-like Ordinal-yielding decreasing -> non-increasing for set ;

coherence
for b₁ being Ordinal-Sequence st b₁ is decreasing holds
b₁ is non-increasing by ORDINAL1:def 2;

end;

theorem Th5: :: ORDINAL5:5

for f being Sequence holds
( f is infinite iff omega c= dom f )

proof end;

registration

cluster Relation-like Function-like Sequence-like decreasing -> finite for set ;

coherence
for b₁ being Sequence st b₁ is decreasing holds
b₁ is finite

proof end;

cluster empty -> empty increasing decreasing for set ;

coherence
for b₁ being empty set holds
( b₁ is decreasing & b₁ is increasing )

proof end;

end;

registration

let a be Ordinal;

cluster <%a%> -> Ordinal-yielding ;

coherence
<%a%> is Ordinal-yielding

proof end;

end;

registration

let a be Ordinal;

cluster <%a%> -> increasing decreasing ;

coherence
( <%a%> is decreasing & <%a%> is increasing )

proof end;

end;

registration

cluster Relation-like Function-like non empty Sequence-like finite Ordinal-yielding increasing decreasing non-decreasing non-increasing for set ;

existence
ex b₁ being Ordinal-Sequence st
( b₁ is decreasing & b₁ is increasing & b₁ is non-decreasing & b₁ is non-increasing & b₁ is finite & not b₁ is empty )

proof end;

end;

theorem Th6: :: ORDINAL5:6

for f being non-decreasing Ordinal-Sequence st not dom f is empty holds
Union f is_limes_of f

proof end;

theorem :: ORDINAL5:7

for a, b being Ordinal
for n being Nat st a in b holds
n *^ (exp (omega,a)) in exp (omega,b)

proof end;

theorem Th8: :: ORDINAL5:8

for a being Ordinal
for f being Ordinal-Sequence st 0 in a & ( for b being Ordinal st b in dom f holds
f . b = exp (a,b) ) holds
f is non-decreasing

proof end;

theorem Th9: :: ORDINAL5:9

for a, b being Ordinal st a is limit_ordinal & 0 in b holds
exp (a,b) is limit_ordinal

proof end;

theorem :: ORDINAL5:10

for a being Ordinal
for f being Ordinal-Sequence st 1 in a & ( for b being Ordinal st b in dom f holds
f . b = exp (a,b) ) holds
f is increasing

proof end;

theorem Th11: :: ORDINAL5:11

for a, b being Ordinal
for x being object st 0 in a & not b is empty & b is limit_ordinal holds
( x in exp (a,b) iff ex c being Ordinal st
( c in b & x in exp (a,c) ) )

proof end;

theorem Th12: :: ORDINAL5:12

for a, b, c being Ordinal st 0 in a & exp (a,b) in exp (a,c) holds
b in c

proof end;

definition

let a, b be Ordinal;

func a |^|^ b -> Ordinal means :Def4: :: ORDINAL5:def 4
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
existence
ex b₁ being Ordinal ex phi being Ordinal-Sequence st
( b₁ = 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) ) );
uniqueness
for b₁, b₂ being Ordinal st ex phi being Ordinal-Sequence st
( b₁ = 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) ) ) & ex phi being Ordinal-Sequence st
( b₂ = 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) ) ) holds
b₁ = b₂;

proof end;

end;

:: deftheorem Def4 defines |^|^ ORDINAL5:def 4 :
for a, b, b₃ being Ordinal holds
( b₃ = a |^|^ b iff ex phi being Ordinal-Sequence st
( b₃ = 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) ) ) );

theorem Th13: :: ORDINAL5:13

for a being Ordinal holds a |^|^ 0 = 1

proof end;

theorem Th14: :: ORDINAL5:14

for a, b being Ordinal holds a |^|^ (succ b) = exp (a,(a |^|^ b))

proof end;

theorem Th15: :: ORDINAL5:15

for a, b being Ordinal st b <> 0 & b is limit_ordinal holds
for phi being Ordinal-Sequence st dom phi = b & ( for c being Ordinal st c in b holds
phi . c = a |^|^ c ) holds
a |^|^ b = lim phi

proof end;

theorem Th16: :: ORDINAL5:16

for a being Ordinal holds a |^|^ 1 = a

proof end;

theorem Th17: :: ORDINAL5:17

for a being Ordinal holds 1 |^|^ a = 1

proof end;

theorem Th18: :: ORDINAL5:18

for a being Ordinal holds a |^|^ 2 = exp (a,a)

proof end;

theorem :: ORDINAL5:19

for a being Ordinal holds a |^|^ 3 = exp (a,(exp (a,a)))

proof end;

theorem :: ORDINAL5:20

for n being Nat holds
( 0 |^|^ (2 * n) = 1 & 0 |^|^ ((2 * n) + 1) = 0 )

proof end;

theorem Th21: :: ORDINAL5:21

for a, b, c being Ordinal st a c= b & 0 in c holds
c |^|^ a c= c |^|^ b

proof end;

theorem :: ORDINAL5:22

for a being Ordinal
for f being Ordinal-Sequence st 0 in a & ( for b being Ordinal st b in dom f holds
f . b = a |^|^ b ) holds
f is non-decreasing

proof end;

theorem Th23: :: ORDINAL5:23

for a, b being Ordinal st 0 in a & 0 in b holds
a c= a |^|^ b

proof end;

theorem Th24: :: ORDINAL5:24

for a being Ordinal
for m, n being Nat st 1 in a & m < n holds
a |^|^ m in a |^|^ n

proof 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: :: ORDINAL5:25

for a being Ordinal
for f being Ordinal-Sequence st 1 in a & dom f c= omega & ( for b being Ordinal st b in dom f holds
f . b = a |^|^ b ) holds
f is increasing

proof end;

theorem Th26: :: ORDINAL5:26

for a, b being Ordinal st 1 in a & 1 in b holds
a in a |^|^ b

proof end;

theorem Th27: :: ORDINAL5:27

for n, k being Nat holds exp (n,k) = n |^ k

proof end;

registration

let n, k be Nat;

cluster exp (n,k) -> natural ;

coherence
exp (n,k) is natural

proof end;

end;

registration

let n, k be Nat;

cluster n |^|^ k -> natural ;

coherence
n |^|^ k is natural

proof end;

end;

theorem Th28: :: ORDINAL5:28

for n, k being Nat st n > 1 holds
n |^|^ k > k

proof end;

theorem :: ORDINAL5:29

for n being Nat st n > 1 holds
n |^|^ omega = omega

proof end;

theorem Th30: :: ORDINAL5:30

for a being Ordinal st 1 in a holds
a |^|^ omega is limit_ordinal

proof end;

theorem Th31: :: ORDINAL5:31

for a being Ordinal st 0 in a holds
exp (a,(a |^|^ omega)) = a |^|^ omega

proof end;

theorem :: ORDINAL5:32

for a, b being Ordinal st 0 in a & omega c= b holds
a |^|^ b = a |^|^ omega

proof end;

scheme :: ORDINAL5:sch 1
CriticalNumber2{ F₁() -> Ordinal, F₂() -> Ordinal-Sequence, F₃( Ordinal) -> Ordinal } :

( F₁() c= Union F₂() & F₃((Union F₂())) = Union F₂() & ( for b being Ordinal st F₁() c= b & F₃(b) = b holds
Union F₂() c= b ) )

provided

A1: for a, b being Ordinal st a in b holds
F₃(a) in F₃(b) and
A2: for a being Ordinal st not a is empty & a is limit_ordinal holds
for phi being Ordinal-Sequence st dom phi = a & ( for b being Ordinal st b in a holds
phi . b = F₃(b) ) holds
F₃(a) is_limes_of phi and
A3: ( dom F₂() = omega & F₂() . 0 = F₁() ) and
A4: for a being Ordinal st a in omega holds
F₂() . (succ a) = F₃((F₂() . a))

proof end;

scheme :: ORDINAL5:sch 2
CriticalNumber3{ F₁() -> Ordinal, F₂( Ordinal) -> Ordinal } :

ex a being Ordinal st
( F₁() in a & F₂(a) = a )

provided

A1: for a, b being Ordinal st a in b holds
F₂(a) in F₂(b) and
A2: for a being Ordinal st not a is empty & a is limit_ordinal holds
for phi being Ordinal-Sequence st dom phi = a & ( for b being Ordinal st b in a holds
phi . b = F₂(b) ) holds
F₂(a) is_limes_of phi

proof end;

definition

let a be Ordinal;

attr a is epsilon means :Def5: :: ORDINAL5:def 5
exp (omega,a) = a;

end;

:: deftheorem Def5 defines epsilon ORDINAL5:def 5 :
for a being Ordinal holds
( a is epsilon iff exp (omega,a) = a );

theorem Th33: :: ORDINAL5:33

for a being Ordinal ex b being Ordinal st
( a in b & b is epsilon )

proof end;

registration

cluster epsilon-transitive epsilon-connected ordinal epsilon for set ;

existence
ex b₁ being Ordinal st b₁ is epsilon

proof end;

end;

definition

let a be Ordinal;

func first_epsilon_greater_than a -> epsilon Ordinal means :Def6: :: ORDINAL5:def 6
( a in it & ( for b being epsilon Ordinal st a in b holds
it c= b ) );

existence
ex b₁ being epsilon Ordinal st
( a in b₁ & ( for b being epsilon Ordinal st a in b holds
b₁ c= b ) )

proof end;

uniqueness
for b₁, b₂ being epsilon Ordinal st a in b₁ & ( for b being epsilon Ordinal st a in b holds
b₁ c= b ) & a in b₂ & ( for b being epsilon Ordinal st a in b holds
b₂ c= b ) holds
b₁ = b₂ ;

end;

:: deftheorem Def6 defines first_epsilon_greater_than ORDINAL5:def 6 :
for a being Ordinal
for b₂ being epsilon Ordinal holds
( b₂ = first_epsilon_greater_than a iff ( a in b₂ & ( for b being epsilon Ordinal st a in b holds
b₂ c= b ) ) );

theorem :: ORDINAL5:34

for a, b being Ordinal st a c= b holds
first_epsilon_greater_than a c= first_epsilon_greater_than b

proof end;

theorem :: ORDINAL5:35

for a, b being Ordinal st a in b & b in first_epsilon_greater_than a holds
first_epsilon_greater_than b = first_epsilon_greater_than a

proof end;

theorem Th36: :: ORDINAL5:36

first_epsilon_greater_than 0 = omega |^|^ omega

proof end;

theorem Th37: :: ORDINAL5:37

for e being epsilon Ordinal holds omega in e

proof end;

registration

cluster ordinal epsilon -> non empty limit_ordinal for set ;

coherence
for b₁ being Ordinal st b₁ is epsilon holds
( not b₁ is empty & b₁ is limit_ordinal )

proof end;

end;

theorem Th38: :: ORDINAL5:38

for e being epsilon Ordinal holds exp (omega,(exp (e,omega))) = exp (e,(exp (e,omega)))

proof end;

theorem Th39: :: ORDINAL5:39

for n being Nat
for e being epsilon Ordinal st 0 in n holds
e |^|^ (n + 2) = exp (omega,(e |^|^ (n + 1)))

proof end;

theorem Th40: :: ORDINAL5:40

for e being epsilon Ordinal holds first_epsilon_greater_than e = e |^|^ omega

proof end;

definition

let a be Ordinal;

:: equals omega |^|^ exp(omega, 1+^a); :: wg wikipedii, ale to nie prawda

func epsilon_ a -> Ordinal means :Def7: :: ORDINAL5:def 7
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
existence
ex b₁ being Ordinal ex phi being Ordinal-Sequence st
( b₁ = 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) ) );
uniqueness
for b₁, b₂ being Ordinal st ex phi being Ordinal-Sequence st
( b₁ = 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) ) ) & ex phi being Ordinal-Sequence st
( b₂ = 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) ) ) holds
b₁ = b₂;

proof end;

end;

:: deftheorem Def7 defines epsilon_ ORDINAL5:def 7 :
for a, b₂ being Ordinal holds
( b₂ = epsilon_ a iff ex phi being Ordinal-Sequence st
( b₂ = 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) ) ) );

theorem Th41: :: ORDINAL5:41

epsilon_ 0 = omega |^|^ omega

proof end;

theorem Th42: :: ORDINAL5:42

for a being Ordinal holds epsilon_ (succ a) = (epsilon_ a) |^|^ omega

proof end;

theorem Th43: :: ORDINAL5:43

for b being Ordinal st b <> 0 & b is limit_ordinal holds
for phi being Ordinal-Sequence st dom phi = b & ( for c being Ordinal st c in b holds
phi . c = epsilon_ c ) holds
epsilon_ b = lim phi

proof end;

theorem Th44: :: ORDINAL5:44

for a, b being Ordinal st a in b holds
epsilon_ a in epsilon_ b

proof end;

theorem Th45: :: ORDINAL5:45

for phi being Ordinal-Sequence st ( for c being Ordinal st c in dom phi holds
phi . c = epsilon_ c ) holds
phi is increasing

proof end;

theorem Th46: :: ORDINAL5:46

for b being Ordinal st b <> {} & b is limit_ordinal holds
for phi being Ordinal-Sequence st dom phi = b & ( for c being Ordinal st c in b holds
phi . c = epsilon_ c ) holds
epsilon_ b = Union phi

proof end;

theorem Th47: :: ORDINAL5:47

for b being Ordinal
for x being object st not b is empty & b is limit_ordinal holds
( x in epsilon_ b iff ex c being Ordinal st
( c in b & x in epsilon_ c ) )

proof end;

theorem Th48: :: ORDINAL5:48

for a being Ordinal holds a c= epsilon_ a

proof end;

theorem Th49: :: ORDINAL5:49

for X being non empty set st ( for x being object 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 end;

theorem Th50: :: ORDINAL5:50

for X being non empty set st ( for x being object st x in X holds
x is epsilon Ordinal ) & ( for a being Ordinal st a in X holds
first_epsilon_greater_than a in X ) holds
union X is epsilon Ordinal

proof end;

registration

let a be Ordinal;

cluster epsilon_ a -> epsilon ;

coherence
epsilon_ a is epsilon

proof end;

end;

:: The ordinal indexing of epsilon numbers

theorem :: ORDINAL5:51

for a being Ordinal st a is epsilon holds
ex b being Ordinal st a = epsilon_ b

proof end;

definition

let A be finite Ordinal-Sequence;

func Sum^ A -> Ordinal means :Def8: :: ORDINAL5:def 8
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
existence
ex b₁ being Ordinal ex f being Ordinal-Sequence st
( b₁ = 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) ) );
uniqueness
for b₁, b₂ being Ordinal st ex f being Ordinal-Sequence st
( b₁ = 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) ) ) & ex f being Ordinal-Sequence st
( b₂ = 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) ) ) holds
b₁ = b₂;

proof end;

end;

:: deftheorem Def8 defines Sum^ ORDINAL5:def 8 :
for A being finite Ordinal-Sequence
for b₂ being Ordinal holds
( b₂ = Sum^ A iff ex f being Ordinal-Sequence st
( b₂ = 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) ) ) );

theorem Th52: :: ORDINAL5:52

Sum^ {} = 0

proof end;

theorem Th53: :: ORDINAL5:53

for a being Ordinal holds Sum^ <%a%> = a

proof end;

theorem Th54: :: ORDINAL5:54

for a being Ordinal
for A being finite Ordinal-Sequence holds Sum^ (A ^ <%a%>) = (Sum^ A) +^ a

proof end;

theorem Th55: :: ORDINAL5:55

for a being Ordinal
for A being finite Ordinal-Sequence holds Sum^ (<%a%> ^ A) = a +^ (Sum^ A)

proof end;

theorem Th56: :: ORDINAL5:56

for A being finite Ordinal-Sequence holds A . 0 c= Sum^ A

proof end;

definition

let a be Ordinal;

attr a is Cantor-component means :Def9: :: ORDINAL5:def 9
ex b being Ordinal ex n being Nat st
( 0 in Segm n & a = n *^ (exp (omega,b)) );

end;

:: deftheorem Def9 defines Cantor-component ORDINAL5:def 9 :
for a being Ordinal holds
( a is Cantor-component iff ex b being Ordinal ex n being Nat st
( 0 in Segm n & a = n *^ (exp (omega,b)) ) );

registration

cluster ordinal Cantor-component -> non empty for set ;

coherence
for b₁ being Ordinal st b₁ is Cantor-component holds
not b₁ is empty

proof end;

end;

registration

cluster epsilon-transitive epsilon-connected ordinal Cantor-component for set ;

existence
ex b₁ being Ordinal st b₁ is Cantor-component

proof end;

end;

definition

let a, b be Ordinal;

func b -exponent a -> Ordinal means :Def10: :: ORDINAL5:def 10
( exp (b,it) c= a & ( for c being Ordinal st exp (b,c) c= a holds
c c= it ) ) if ( 1 in b & 0 in a )
otherwise it = 0 ;

existence
( ( 1 in b & 0 in a implies ex b₁ being Ordinal st
( exp (b,b₁) c= a & ( for c being Ordinal st exp (b,c) c= a holds
c c= b₁ ) ) ) & ( ( not 1 in b or not 0 in a ) implies ex b₁ being Ordinal st b₁ = 0 ) )

proof end;

uniqueness
for b₁, b₂ being Ordinal holds
( ( 1 in b & 0 in a & exp (b,b₁) c= a & ( for c being Ordinal st exp (b,c) c= a holds
c c= b₁ ) & exp (b,b₂) c= a & ( for c being Ordinal st exp (b,c) c= a holds
c c= b₂ ) implies b₁ = b₂ ) & ( ( not 1 in b or not 0 in a ) & b₁ = 0 & b₂ = 0 implies b₁ = b₂ ) ) ;
consistency
for b₁ being Ordinal holds verum ;

end;

:: deftheorem Def10 defines -exponent ORDINAL5:def 10 :
for a, b, b₃ being Ordinal holds
( ( 1 in b & 0 in a implies ( b₃ = b -exponent a iff ( exp (b,b₃) c= a & ( for c being Ordinal st exp (b,c) c= a holds
c c= b₃ ) ) ) ) & ( ( not 1 in b or not 0 in a ) implies ( b₃ = b -exponent a iff b₃ = 0 ) ) );

Lm1: 0 in Segm 1
by NAT_1:44;

theorem Th57: :: ORDINAL5:57

for a, b being Ordinal st 1 in b holds
a in exp (b,(succ (b -exponent a)))

proof end;

registration

let a, b be Ordinal;

cluster <%a,b%> -> Ordinal-yielding ;

coherence
<%a,b%> is Ordinal-yielding

proof end;

let c be Ordinal;

cluster <%a,b,c%> -> Ordinal-yielding ;

coherence
<%a,b,c%> is Ordinal-yielding

proof end;

end;

::: into ORDINAL3 ?

registration

let a be non empty Ordinal;
let b be Ordinal;

cluster a +^ b -> non empty ;

coherence
not a +^ b is empty by ORDINAL3:26;

cluster b +^ a -> non empty ;

coherence
not b +^ a is empty by ORDINAL3:26;

end;

::: into ORDINAL3 ?

registration

let a, b be non empty Ordinal;

cluster b *^ a -> non empty ;

coherence
not b *^ a is empty by ORDINAL3:31;

end;

::: into ORDINAL4 ?

registration

let A be empty Ordinal;
let B be non empty Ordinal;

cluster exp (A,B) -> empty ;

coherence
exp (A,B) is empty by ORDINAL4:20;

end;

::: into ORDINAL4 ?

registration

let A be Ordinal;
let B be empty Ordinal;

cluster exp (A,B) -> non empty ;

coherence
not exp (A,B) is empty by ORDINAL2:43;

end;

::: into ORDINAL4 ?

registration

let A be non empty Ordinal;
let B be Ordinal;

cluster exp (A,B) -> non empty ;

coherence
not exp (A,B) is empty by ORDINAL4:22;

end;

theorem Th58: :: ORDINAL5:58

for a, b, c being Ordinal st 0 in c & c in b holds
b -exponent (c *^ (exp (b,a))) = a

proof end;

theorem Th59: :: ORDINAL5:59

for a, b, c being Ordinal st 0 in a & 1 in b & c = b -exponent a holds
a div^ (exp (b,c)) in b

proof end;

theorem Th60: :: ORDINAL5:60

for a, b, c being Ordinal st 0 in a & 1 in b & c = b -exponent a holds
0 in a div^ (exp (b,c))

proof end;

theorem Th61: :: ORDINAL5:61

for a, b, c being Ordinal st b <> 0 holds
a mod^ (exp (b,c)) in exp (b,c)

proof end;

theorem Th62: :: ORDINAL5:62

for a being Ordinal st 0 in a holds
ex n being Nat ex c being Ordinal st
( a = (n *^ (exp (omega,(omega -exponent a)))) +^ c & 0 in Segm n & c in exp (omega,(omega -exponent a)) )

proof end;

theorem Th63: :: ORDINAL5:63

for a, b, c being Ordinal st 1 in c & c -exponent b in c -exponent a holds
b in a

proof end;

definition

let A be Ordinal-Sequence;

attr A is Cantor-normal-form means :Def11: :: ORDINAL5:def 11
( ( for a being Ordinal st a in dom A holds
A . a is Cantor-component ) & ( for a, b being Ordinal st a in b & b in dom A holds
omega -exponent (A . b) in omega -exponent (A . a) ) );

end;

:: deftheorem Def11 defines Cantor-normal-form ORDINAL5:def 11 :
for A being Ordinal-Sequence holds
( A is Cantor-normal-form iff ( ( for a being Ordinal st a in dom A holds
A . a is Cantor-component ) & ( for a, b being Ordinal st a in b & b in dom A holds
omega -exponent (A . b) in omega -exponent (A . a) ) ) );

registration

cluster Relation-like Function-like empty Sequence-like Ordinal-yielding -> Cantor-normal-form for set ;

coherence
for b₁ being Ordinal-Sequence st b₁ is empty holds
b₁ is Cantor-normal-form ;

cluster Relation-like Function-like Sequence-like Ordinal-yielding Cantor-normal-form -> non-empty for set ;

coherence
for b₁ being Ordinal-Sequence st b₁ is Cantor-normal-form holds
b₁ is non-empty

proof end;

cluster Relation-like Function-like Sequence-like Ordinal-yielding Cantor-normal-form -> decreasing for set ;

coherence
for b₁ being Ordinal-Sequence st b₁ is Cantor-normal-form holds
b₁ is decreasing

proof end;

end;

theorem :: ORDINAL5:64

for A being Cantor-normal-form Ordinal-Sequence st Sum^ A = 0 holds
A = {}

proof end;

theorem Th65: :: ORDINAL5:65

for b being Ordinal
for n being Nat st 0 in Segm n holds
<%(n *^ (exp (omega,b)))%> is Cantor-normal-form

proof end;

registration

cluster Relation-like Function-like non empty Sequence-like Ordinal-yielding Cantor-normal-form for set ;

existence
ex b₁ being Ordinal-Sequence st
( not b₁ is empty & b₁ is Cantor-normal-form )

proof end;

end;

theorem Th66: :: ORDINAL5:66

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 end;

theorem :: ORDINAL5:67

for A being Cantor-normal-form Ordinal-Sequence st A <> {} holds
ex c being Cantor-component Ordinal ex B being Cantor-normal-form Ordinal-Sequence st A = <%c%> ^ B

proof end;

theorem Th68: :: ORDINAL5:68

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 end;

:: Existence of Cantor Normal Form for ordinal numbers

theorem :: ORDINAL5:69

for a being Ordinal ex A being Cantor-normal-form Ordinal-Sequence st a = Sum^ A

proof end;