:: Epsilon Numbers and Cantor Normal Form
:: by Grzegorz Bancerek
::
:: Received October 20, 2009
:: Copyright (c) 2009-2012 Association of Mizar Users
begin
theorem
Th1
:
:: ORDINAL5:1
for
a
,
b
being
ordinal
number
holds
( not
a
c=
succ
b
or
a
c=
b
or
a
=
succ
b
)
proof
end;
registration
cluster
NAT
->
limit_ordinal
;
coherence
omega
is
limit_ordinal
;
cluster
empty
->
empty
Ordinal-yielding
for
set
;
coherence
for
b
1
being
empty
set
holds
b
1
is
Ordinal-yielding
proof
end;
end;
registration
cluster
Relation-like
Function-like
non
empty
T-Sequence-like
finite
for
set
;
existence
ex
b
1
being
T-Sequence
st
( not
b
1
is
empty
&
b
1
is
finite
)
proof
end;
end;
registration
let
f
be
T-Sequence
;
let
g
be non
empty
T-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
number
for
S
being
T-Sequence
st
dom
S
=
a
+^
b
holds
ex
S1
,
S2
being
T-Sequence
st
(
S
=
S1
^
S2
&
dom
S1
=
a
&
dom
S2
=
b
)
proof
end;
theorem
Th3
:
:: ORDINAL5:3
for
S1
,
S2
being
T-Sequence
holds
(
rng
S1
c=
rng
(
S1
^
S2
)
&
rng
S2
c=
rng
(
S1
^
S2
)
)
proof
end;
theorem
Th4
:
:: ORDINAL5:4
for
S1
,
S2
being
T-Sequence
st
S1
^
S2
is
Ordinal-yielding
holds
(
S1
is
Ordinal-yielding
&
S2
is
Ordinal-yielding
)
proof
end;
definition
let
f
be
T-Sequence
;
attr
f
is
decreasing
means
:: ORDINAL5:def 1
for
a
,
b
being
ordinal
number
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
number
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
number
st
a
in
b
&
b
in
dom
f
holds
f
.
b
c=
f
.
a
;
end;
::
deftheorem
defines
decreasing
ORDINAL5:def 1 :
for
f
being
T-Sequence
holds
(
f
is
decreasing
iff for
a
,
b
being
ordinal
number
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
T-Sequence
holds
(
f
is
non-decreasing
iff for
a
,
b
being
ordinal
number
st
a
in
b
&
b
in
dom
f
holds
f
.
a
c=
f
.
b
);
::
deftheorem
defines
non-increasing
ORDINAL5:def 3 :
for
f
being
T-Sequence
holds
(
f
is
non-increasing
iff for
a
,
b
being
ordinal
number
st
a
in
b
&
b
in
dom
f
holds
f
.
b
c=
f
.
a
);
registration
cluster
Relation-like
Function-like
T-Sequence-like
Ordinal-yielding
increasing
->
non-decreasing
for
set
;
coherence
for
b
1
being
Ordinal-Sequence
st
b
1
is
increasing
holds
b
1
is
non-decreasing
proof
end;
cluster
Relation-like
Function-like
T-Sequence-like
Ordinal-yielding
decreasing
->
non-increasing
for
set
;
coherence
for
b
1
being
Ordinal-Sequence
st
b
1
is
decreasing
holds
b
1
is
non-increasing
proof
end;
end;
theorem
Th5
:
:: ORDINAL5:5
for
f
being
T-Sequence
holds
(
f
is
infinite
iff
omega
c=
dom
f
)
proof
end;
registration
cluster
Relation-like
Function-like
T-Sequence-like
decreasing
->
finite
for
set
;
coherence
for
b
1
being
T-Sequence
st
b
1
is
decreasing
holds
b
1
is
finite
proof
end;
cluster
empty
->
empty
increasing
decreasing
for
set
;
coherence
for
b
1
being
empty
set
holds
(
b
1
is
decreasing
&
b
1
is
increasing
)
proof
end;
end;
registration
let
a
be
ordinal
number
;
cluster
<%
a
%>
->
Ordinal-yielding
;
coherence
<%
a
%>
is
Ordinal-yielding
proof
end;
end;
registration
let
a
be
ordinal
number
;
cluster
<%
a
%>
->
increasing
decreasing
;
coherence
(
<%
a
%>
is
decreasing
&
<%
a
%>
is
increasing
)
proof
end;
end;
registration
cluster
Relation-like
Function-like
non
empty
T-Sequence-like
finite
Ordinal-yielding
increasing
decreasing
non-decreasing
non-increasing
for
set
;
existence
ex
b
1
being
Ordinal-Sequence
st
(
b
1
is
decreasing
&
b
1
is
increasing
&
b
1
is
non-decreasing
&
b
1
is
non-increasing
&
b
1
is
finite
& not
b
1
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
number
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
number
for
f
being
Ordinal-Sequence
st
0
in
a
& ( for
b
being
ordinal
number
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
number
st
a
is
limit_ordinal
&
0
in
b
holds
exp
(
a
,
b
) is
limit_ordinal
proof
end;
theorem
:: ORDINAL5:10
for
a
being
ordinal
number
for
f
being
Ordinal-Sequence
st 1
in
a
& ( for
b
being
ordinal
number
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
number
for
x
being
set
st
0
in
a
& not
b
is
empty
&
b
is
limit_ordinal
holds
(
x
in
exp
(
a
,
b
) iff ex
c
being
ordinal
number
st
(
c
in
b
&
x
in
exp
(
a
,
c
) ) )
proof
end;
theorem
Th12
:
:: ORDINAL5:12
for
a
,
b
,
c
being
ordinal
number
st
0
in
a
&
exp
(
a
,
b
)
in
exp
(
a
,
c
) holds
b
in
c
proof
end;
begin
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
1
being
Ordinal
ex
phi
being
Ordinal-Sequence
st
(
b
1
=
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
1
,
b
2
being
Ordinal
st ex
phi
being
Ordinal-Sequence
st
(
b
1
=
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
2
=
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
1
=
b
2
;
proof
end;
end;
::
deftheorem
Def4
defines
|^|^
ORDINAL5:def 4 :
for
a
,
b
,
b
3
being
Ordinal
holds
(
b
3
=
a
|^|^
b
iff ex
phi
being
Ordinal-Sequence
st
(
b
3
=
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
number
holds
a
|^|^
0
=
1
proof
end;
theorem
Th14
:
:: ORDINAL5:14
for
a
,
b
being
ordinal
number
holds
a
|^|^
(
succ
b
)
=
exp
(
a
,
(
a
|^|^
b
)
)
proof
end;
theorem
Th15
:
:: ORDINAL5:15
for
b
,
a
being
ordinal
number
st
b
<>
{}
&
b
is
limit_ordinal
holds
for
phi
being
Ordinal-Sequence
st
dom
phi
=
b
& ( for
c
being
ordinal
number
st
c
in
b
holds
phi
.
c
=
a
|^|^
c
) holds
a
|^|^
b
=
lim
phi
proof
end;
theorem
Th16
:
:: ORDINAL5:16
for
a
being
ordinal
number
holds
a
|^|^
1
=
a
proof
end;
theorem
Th17
:
:: ORDINAL5:17
for
a
being
ordinal
number
holds 1
|^|^
a
=
1
proof
end;
theorem
Th18
:
:: ORDINAL5:18
for
a
being
ordinal
number
holds
a
|^|^
2
=
exp
(
a
,
a
)
proof
end;
theorem
:: ORDINAL5:19
for
a
being
ordinal
number
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
number
st
a
c=
b
&
0
in
c
holds
c
|^|^
a
c=
c
|^|^
b
proof
end;
theorem
:: ORDINAL5:22
for
a
being
ordinal
number
for
f
being
Ordinal-Sequence
st
0
in
a
& ( for
b
being
ordinal
number
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
number
st
0
in
a
&
0
in
b
holds
a
c=
a
|^|^
b
proof
end;
theorem
Th24
:
:: ORDINAL5:24
for
a
being
ordinal
number
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
number
for
f
being
Ordinal-Sequence
st 1
in
a
&
dom
f
c=
omega
& ( for
b
being
ordinal
number
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
number
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
number
st 1
in
a
holds
a
|^|^
omega
is
limit_ordinal
proof
end;
theorem
Th31
:
:: ORDINAL5:31
for
a
being
ordinal
number
st
0
in
a
holds
exp
(
a
,
(
a
|^|^
omega
)
)
=
a
|^|^
omega
proof
end;
theorem
:: ORDINAL5:32
for
a
,
b
being
ordinal
number
st
0
in
a
&
omega
c=
b
holds
a
|^|^
b
=
a
|^|^
omega
proof
end;
begin
Lm1
:
{}
in
omega
by
ORDINAL1:def 11
;
scheme
:: ORDINAL5:sch 1
CriticalNumber2
{
F
1
()
->
Ordinal
,
F
2
()
->
Ordinal-Sequence
,
F
3
(
Ordinal
)
->
Ordinal
} :
(
F
1
()
c=
Union
F
2
() &
F
3
(
(
Union
F
2
()
)
)
=
Union
F
2
() & ( for
b
being
ordinal
number
st
F
1
()
c=
b
&
F
3
(
b
)
=
b
holds
Union
F
2
()
c=
b
) )
provided
A1
: for
a
,
b
being
ordinal
number
st
a
in
b
holds
F
3
(
a
)
in
F
3
(
b
)
and
A2
: for
a
being
ordinal
number
st not
a
is
empty
&
a
is
limit_ordinal
holds
for
phi
being
Ordinal-Sequence
st
dom
phi
=
a
& ( for
b
being
ordinal
number
st
b
in
a
holds
phi
.
b
=
F
3
(
b
) ) holds
F
3
(
a
)
is_limes_of
phi
and
A3
: (
dom
F
2
()
=
omega
&
F
2
()
.
0
=
F
1
() )
and
A4
: for
a
being
ordinal
number
st
a
in
omega
holds
F
2
()
.
(
succ
a
)
=
F
3
(
(
F
2
()
.
a
)
)
proof
end;
scheme
:: ORDINAL5:sch 2
CriticalNumber3
{
F
1
()
->
Ordinal
,
F
2
(
Ordinal
)
->
Ordinal
} :
ex
a
being
ordinal
number
st
(
F
1
()
in
a
&
F
2
(
a
)
=
a
)
provided
A1
: for
a
,
b
being
ordinal
number
st
a
in
b
holds
F
2
(
a
)
in
F
2
(
b
)
and
A2
: for
a
being
ordinal
number
st not
a
is
empty
&
a
is
limit_ordinal
holds
for
phi
being
Ordinal-Sequence
st
dom
phi
=
a
& ( for
b
being
ordinal
number
st
b
in
a
holds
phi
.
b
=
F
2
(
b
) ) holds
F
2
(
a
)
is_limes_of
phi
proof
end;
begin
definition
let
a
be
ordinal
number
;
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
number
holds
(
a
is
epsilon
iff
exp
(
omega
,
a
)
=
a
);
theorem
Th33
:
:: ORDINAL5:33
for
a
being
ordinal
number
ex
b
being
ordinal
number
st
(
a
in
b
&
b
is
epsilon
)
proof
end;
registration
cluster
epsilon-transitive
epsilon-connected
ordinal
epsilon
for
set
;
existence
ex
b
1
being
ordinal
number
st
b
1
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
1
being
epsilon
Ordinal
st
(
a
in
b
1
& ( for
b
being
epsilon
Ordinal
st
a
in
b
holds
b
1
c=
b
) )
proof
end;
uniqueness
for
b
1
,
b
2
being
epsilon
Ordinal
st
a
in
b
1
& ( for
b
being
epsilon
Ordinal
st
a
in
b
holds
b
1
c=
b
) &
a
in
b
2
& ( for
b
being
epsilon
Ordinal
st
a
in
b
holds
b
2
c=
b
) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def6
defines
first_epsilon_greater_than
ORDINAL5:def 6 :
for
a
being
Ordinal
for
b
2
being
epsilon
Ordinal
holds
(
b
2
=
first_epsilon_greater_than
a
iff (
a
in
b
2
& ( for
b
being
epsilon
Ordinal
st
a
in
b
holds
b
2
c=
b
) ) );
theorem
:: ORDINAL5:34
for
a
,
b
being
ordinal
number
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
number
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
1
being
Ordinal
st
b
1
is
epsilon
holds
( not
b
1
is
empty
&
b
1
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
1
being
Ordinal
ex
phi
being
Ordinal-Sequence
st
(
b
1
=
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
1
,
b
2
being
Ordinal
st ex
phi
being
Ordinal-Sequence
st
(
b
1
=
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
2
=
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
1
=
b
2
;
proof
end;
end;
::
deftheorem
Def7
defines
epsilon_
ORDINAL5:def 7 :
for
a
,
b
2
being
Ordinal
holds
(
b
2
=
epsilon_
a
iff ex
phi
being
Ordinal-Sequence
st
(
b
2
=
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
number
holds
epsilon_
(
succ
a
)
=
(
epsilon_
a
)
|^|^
omega
proof
end;
theorem
Th43
:
:: ORDINAL5:43
for
b
being
ordinal
number
st
b
<>
{}
&
b
is
limit_ordinal
holds
for
phi
being
Ordinal-Sequence
st
dom
phi
=
b
& ( for
c
being
ordinal
number
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
number
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
number
st
c
in
dom
phi
holds
phi
.
c
=
epsilon_
c
) holds
phi
is
increasing
proof
end;
theorem
Th46
:
:: ORDINAL5:46
for
b
being
ordinal
number
st
b
<>
{}
&
b
is
limit_ordinal
holds
for
phi
being
Ordinal-Sequence
st
dom
phi
=
b
& ( for
c
being
ordinal
number
st
c
in
b
holds
phi
.
c
=
epsilon_
c
) holds
epsilon_
b
=
Union
phi
proof
end;
theorem
Th47
:
:: ORDINAL5:47
for
b
being
ordinal
number
for
x
being
set
st not
b
is
empty
&
b
is
limit_ordinal
holds
(
x
in
epsilon_
b
iff ex
c
being
ordinal
number
st
(
c
in
b
&
x
in
epsilon_
c
) )
proof
end;
theorem
Th48
:
:: ORDINAL5:48
for
a
being
ordinal
number
holds
a
c=
epsilon_
a
proof
end;
theorem
Th49
:
:: ORDINAL5:49
for
X
being non
empty
set
st ( for
x
being
set
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
set
st
x
in
X
holds
x
is
epsilon
Ordinal
) & ( for
a
being
ordinal
number
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
number
;
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
number
st
a
is
epsilon
holds
ex
b
being
ordinal
number
st
a
=
epsilon_
b
proof
end;
begin
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
1
being
Ordinal
ex
f
being
Ordinal-Sequence
st
(
b
1
=
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
1
,
b
2
being
Ordinal
st ex
f
being
Ordinal-Sequence
st
(
b
1
=
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
2
=
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
1
=
b
2
;
proof
end;
end;
::
deftheorem
Def8
defines
Sum^
ORDINAL5:def 8 :
for
A
being
finite
Ordinal-Sequence
for
b
2
being
Ordinal
holds
(
b
2
=
Sum^
A
iff ex
f
being
Ordinal-Sequence
st
(
b
2
=
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
number
holds
Sum^
<%
a
%>
=
a
proof
end;
theorem
Th54
:
:: ORDINAL5:54
for
a
being
ordinal
number
for
A
being
finite
Ordinal-Sequence
holds
Sum^
(
A
^
<%
a
%>
)
=
(
Sum^
A
)
+^
a
proof
end;
theorem
Th55
:
:: ORDINAL5:55
for
a
being
ordinal
number
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
number
;
attr
a
is
Cantor-component
means
:
Def9
:
:: ORDINAL5:def 9
ex
b
being
ordinal
number
ex
n
being
Nat
st
(
0
in
n
&
a
=
n
*^
(
exp
(
omega
,
b
)
)
);
end;
::
deftheorem
Def9
defines
Cantor-component
ORDINAL5:def 9 :
for
a
being
ordinal
number
holds
(
a
is
Cantor-component
iff ex
b
being
ordinal
number
ex
n
being
Nat
st
(
0
in
n
&
a
=
n
*^
(
exp
(
omega
,
b
)
)
) );
registration
cluster
ordinal
Cantor-component
->
non
empty
for
set
;
coherence
for
b
1
being
Ordinal
st
b
1
is
Cantor-component
holds
not
b
1
is
empty
proof
end;
end;
registration
cluster
epsilon-transitive
epsilon-connected
ordinal
Cantor-component
for
set
;
existence
ex
b
1
being
Ordinal
st
b
1
is
Cantor-component
proof
end;
end;
definition
let
a
,
b
be
ordinal
number
;
func
b
-exponent
a
->
Ordinal
means
:
Def10
:
:: ORDINAL5:def 10
(
exp
(
b
,
it
)
c=
a
& ( for
c
being
ordinal
number
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
1
being
Ordinal
st
(
exp
(
b
,
b
1
)
c=
a
& ( for
c
being
ordinal
number
st
exp
(
b
,
c
)
c=
a
holds
c
c=
b
1
) ) ) & ( ( not 1
in
b
or not
0
in
a
) implies ex
b
1
being
Ordinal
st
b
1
=
0
) )
proof
end;
uniqueness
for
b
1
,
b
2
being
Ordinal
holds
( ( 1
in
b
&
0
in
a
&
exp
(
b
,
b
1
)
c=
a
& ( for
c
being
ordinal
number
st
exp
(
b
,
c
)
c=
a
holds
c
c=
b
1
) &
exp
(
b
,
b
2
)
c=
a
& ( for
c
being
ordinal
number
st
exp
(
b
,
c
)
c=
a
holds
c
c=
b
2
) implies
b
1
=
b
2
) & ( ( not 1
in
b
or not
0
in
a
) &
b
1
=
0
&
b
2
=
0
implies
b
1
=
b
2
) )
proof
end;
consistency
for
b
1
being
Ordinal
holds verum
;
end;
::
deftheorem
Def10
defines
-exponent
ORDINAL5:def 10 :
for
a
,
b
being
ordinal
number
for
b
3
being
Ordinal
holds
( ( 1
in
b
&
0
in
a
implies (
b
3
=
b
-exponent
a
iff (
exp
(
b
,
b
3
)
c=
a
& ( for
c
being
ordinal
number
st
exp
(
b
,
c
)
c=
a
holds
c
c=
b
3
) ) ) ) & ( ( not 1
in
b
or not
0
in
a
) implies (
b
3
=
b
-exponent
a
iff
b
3
=
0
) ) );
Lm2
:
0
in
1
by
NAT_1:44
;
theorem
Th57
:
:: ORDINAL5:57
for
b
,
a
being
ordinal
number
st 1
in
b
holds
a
in
exp
(
b
,
(
succ
(
b
-exponent
a
)
)
)
proof
end;
theorem
Th58
:
:: ORDINAL5:58
for
b
,
a
being
ordinal
number
for
n
being
Nat
st
0
in
n
&
n
in
b
holds
b
-exponent
(
n
*^
(
exp
(
b
,
a
)
)
)
=
a
proof
end;
theorem
Th59
:
:: ORDINAL5:59
for
a
,
b
,
c
being
ordinal
number
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
number
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
b
,
a
,
c
being
ordinal
number
st
b
<>
0
holds
a
mod^
(
exp
(
b
,
c
)
)
in
exp
(
b
,
c
)
proof
end;
theorem
Th62
:
:: ORDINAL5:62
for
a
being
ordinal
number
st
0
in
a
holds
ex
n
being
Nat
ex
c
being
ordinal
number
st
(
a
=
(
n
*^
(
exp
(
omega
,
(
omega
-exponent
a
)
)
)
)
+^
c
&
0
in
n
&
c
in
exp
(
omega
,
(
omega
-exponent
a
)
) )
proof
end;
theorem
Th63
:
:: ORDINAL5:63
for
c
,
b
,
a
being
ordinal
number
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
number
st
a
in
dom
A
holds
A
.
a
is
Cantor-component
) & ( for
a
,
b
being
ordinal
number
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
number
st
a
in
dom
A
holds
A
.
a
is
Cantor-component
) & ( for
a
,
b
being
ordinal
number
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
T-Sequence-like
Ordinal-yielding
->
Cantor-normal-form
for
set
;
coherence
for
b
1
being
Ordinal-Sequence
st
b
1
is
empty
holds
b
1
is
Cantor-normal-form
proof
end;
cluster
Relation-like
Function-like
T-Sequence-like
Ordinal-yielding
Cantor-normal-form
->
decreasing
for
set
;
coherence
for
b
1
being
Ordinal-Sequence
st
b
1
is
Cantor-normal-form
holds
b
1
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
number
for
n
being
Nat
st
0
in
n
holds
<%
(
n
*^
(
exp
(
omega
,
b
)
)
)
%>
is
Cantor-normal-form
proof
end;
registration
cluster
Relation-like
Function-like
non
empty
T-Sequence-like
Ordinal-yielding
Cantor-normal-form
for
set
;
existence
ex
b
1
being
Ordinal-Sequence
st
( not
b
1
is
empty
&
b
1
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
number
ex
A
being
Cantor-normal-form
Ordinal-Sequence
st
a
=
Sum^
A
proof
end;
:: 1 in c & a in b implies c |^|^ a in c |^|^ b