:: by Grzegorz Bancerek

::

:: Received October 20, 2009

:: Copyright (c) 2009-2012 Association of Mizar Users

begin

registration

coherence

omega is limit_ordinal ;

coherence

for b_{1} being empty set holds b_{1} is Ordinal-yielding

end;
omega is limit_ordinal ;

coherence

for b

proof end;

registration
end;

registration

let f be T-Sequence;

let g be non empty T-Sequence;

coherence

not f ^ g is empty

not g ^ f is empty

end;
let g be non empty T-Sequence;

coherence

not f ^ g is empty

proof end;

coherence not g ^ f is empty

proof 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 )

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 Th4: :: ORDINAL5:4

for S1, S2 being T-Sequence st S1 ^ S2 is Ordinal-yielding holds

( S1 is Ordinal-yielding & S2 is Ordinal-yielding )

( S1 is Ordinal-yielding & S2 is Ordinal-yielding )

proof end;

definition

let f be T-Sequence;

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

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;

for a, b being ordinal number st a in b & b in dom f holds

f . a c= f . b;

:: 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 );

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

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

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

for b_{1} being Ordinal-Sequence st b_{1} is increasing holds

b_{1} is non-decreasing

for b_{1} being Ordinal-Sequence st b_{1} is decreasing holds

b_{1} is non-increasing
end;

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

coherence for b

b

proof end;

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

coherence for b

b

proof end;

registration

coherence

for b_{1} being T-Sequence st b_{1} is decreasing holds

b_{1} is finite

for b_{1} being empty set holds

( b_{1} is decreasing & b_{1} is increasing )

end;
for b

b

proof end;

coherence for b

( b

proof end;

registration
end;

registration

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

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

existence ex b

( 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

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 :: 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

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) ) )

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;

begin

definition

let a, b be Ordinal;

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

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

existence

ex b

( b

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

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

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

proof 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) ) ) );

for a, b, b

( b

( b

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

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 :: 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

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

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;

registration
end;

registration
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 } :

CriticalNumber2{ F

( 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 ) )

providedUnion F

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))

F

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

F

A3: ( dom F

A4: for a being ordinal number st a in omega holds

F

proof end;

scheme :: ORDINAL5:sch 2

CriticalNumber3{ F_{1}() -> Ordinal, F_{2}( Ordinal) -> Ordinal } :

provided

CriticalNumber3{ F

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

F

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

F

proof end;

begin

definition
end;

:: deftheorem Def5 defines epsilon ORDINAL5:def 5 :

for a being ordinal number holds

( a is epsilon iff exp (omega,a) = a );

for a being ordinal number holds

( a is epsilon iff exp (omega,a) = a );

definition

let a be Ordinal;

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 ) )

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}

end;
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 ( a in it & ( for b being epsilon Ordinal st a in b holds

it c= b ) );

ex b

( a in b

b

proof end;

uniqueness for b

b

b

b

proof 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 ) ) );

for a being Ordinal

for b

( b

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

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

first_epsilon_greater_than b = first_epsilon_greater_than a

proof end;

registration

coherence

for b_{1} being Ordinal st b_{1} is epsilon holds

( not b_{1} is empty & b_{1} is limit_ordinal )

end;
for b

( not b

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)))

for e being epsilon Ordinal st 0 in n holds

e |^|^ (n + 2) = exp (omega,(e |^|^ (n + 1)))

proof end;

definition

let a be Ordinal;

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

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

existence

ex b

( b

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

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

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

proof 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) ) ) );

for a, b

( b

( b

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

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

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

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 ) )

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

( 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

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;

begin

definition

let A be finite Ordinal-Sequence;

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

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

existence

ex b

( b

f . (n + 1) = (f . n) +^ (A . n) ) );

uniqueness

for b

( b

f . (n + 1) = (f . n) +^ (A . n) ) ) & ex f being Ordinal-Sequence st

( b

f . (n + 1) = (f . n) +^ (A . n) ) ) holds

b

proof 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) ) ) );

for A being finite Ordinal-Sequence

for b

( b

( b

f . (n + 1) = (f . n) +^ (A . n) ) ) );

theorem Th54: :: ORDINAL5:54

for a being ordinal number

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

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)

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

proof 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)) ) );

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

definition

let a, b be ordinal number ;

( ( 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 ) )

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} ) )

for b_{1} being Ordinal holds verum
;

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

( ( 1 in b & 0 in a implies ex b

( exp (b,b

c c= b

proof end;

uniqueness for b

( ( 1 in b & 0 in a & exp (b,b

c c= b

c c= b

proof end;

consistency for b

:: 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 ) ) );

for a, b being ordinal number

for b

( ( 1 in b & 0 in a implies ( b

c c= b

Lm2: 0 in 1

by NAT_1:44;

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

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

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))

0 in a div^ (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)) )

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;

:: 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) ) ) );

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

for b_{1} being Ordinal-Sequence st b_{1} is empty holds

b_{1} is Cantor-normal-form

for b_{1} being Ordinal-Sequence st b_{1} is Cantor-normal-form holds

b_{1} is decreasing
end;

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

coherence for b

b

proof end;

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

coherence for b

b

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

for n being Nat st 0 in n holds

<%(n *^ (exp (omega,b)))%> is Cantor-normal-form

proof end;

registration

ex b_{1} being Ordinal-Sequence st

( not b_{1} is empty & b_{1} is Cantor-normal-form )
end;

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

existence ex b

( not b

proof 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 )

( 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

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

for c being Cantor-component Ordinal st omega -exponent (A . 0) in omega -exponent c holds

<%c%> ^ A is Cantor-normal-form

proof end;

:: 1 in c & a in b implies c |^|^ a in c |^|^ b