:: Sequences of Ordinal Numbers. Beginnings of Ordinal Arithmetics
:: by Grzegorz Bancerek
::
:: Received July 18, 1989
:: Copyright (c) 1990-2021 Association of Mizar Users


scheme :: ORDINAL2:sch 1
OrdinalInd{ P1[ Ordinal] } :
for A being Ordinal holds P1[A]
provided
A1: P1[ 0 ] and
A2: for A being Ordinal st P1[A] holds
P1[ succ A] and
A3: for A being Ordinal st A <> 0 & A is limit_ordinal & ( for B being Ordinal st B in A holds
P1[B] ) holds
P1[A]
proof end;

theorem Th1: :: ORDINAL2:1
for A, B being Ordinal holds
( A c= B iff succ A c= succ B )
proof end;

theorem Th2: :: ORDINAL2:2
for A being Ordinal holds union (succ A) = A
proof end;

theorem :: ORDINAL2:3
for A being Ordinal holds succ A c= bool A
proof end;

theorem :: ORDINAL2:4
0 is limit_ordinal by ZFMISC_1:2;

theorem Th5: :: ORDINAL2:5
for A being Ordinal holds union A c= A
proof end;

definition
let L be Sequence;
func last L -> set equals :: ORDINAL2:def 1
L . (union (dom L));
coherence
L . (union (dom L)) is set ;
end;

:: deftheorem defines last ORDINAL2:def 1 :
for L being Sequence holds last L = L . (union (dom L));

theorem :: ORDINAL2:6
for A being Ordinal
for L being Sequence st dom L = succ A holds
last L = L . A by Th2;

theorem :: ORDINAL2:7
for X being set holds On X c= X by ORDINAL1:def 9;

theorem Th8: :: ORDINAL2:8
for A being Ordinal holds On A = A
proof end;

theorem Th9: :: ORDINAL2:9
for X, Y being set st X c= Y holds
On X c= On Y
proof end;

theorem :: ORDINAL2:10
for X being set holds Lim X c= X by ORDINAL1:def 10;

theorem :: ORDINAL2:11
for X, Y being set st X c= Y holds
Lim X c= Lim Y
proof end;

theorem :: ORDINAL2:12
for X being set holds Lim X c= On X
proof end;

theorem Th13: :: ORDINAL2:13
for X being set st ( for x being object st x in X holds
x is Ordinal ) holds
meet X is Ordinal
proof end;

registration
cluster epsilon-transitive epsilon-connected ordinal limit_ordinal for set ;
existence
ex b1 being Ordinal st b1 is limit_ordinal
proof end;
end;

definition
let X be set ;
func inf X -> Ordinal equals :: ORDINAL2:def 2
 meet (On X);
coherence
meet (On X) is Ordinal
proof end;
func sup X -> Ordinal means :Def3: :: ORDINAL2:def 3
( On X c= it & ( for A being Ordinal st On X c= A holds
it c= A ) );
existence
ex b1 being Ordinal st
( On X c= b1 & ( for A being Ordinal st On X c= A holds
b1 c= A ) )
proof end;
uniqueness
for b1, b2 being Ordinal st On X c= b1 & ( for A being Ordinal st On X c= A holds
b1 c= A ) & On X c= b2 & ( for A being Ordinal st On X c= A holds
b2 c= A ) holds
b1 = b2 ;
end;

:: deftheorem defines inf ORDINAL2:def 2 :
for X being set holds inf X = meet (On X);

:: deftheorem Def3 defines sup ORDINAL2:def 3 :
for X being set
for b2 being Ordinal holds
( b2 = sup X iff ( On X c= b2 & ( for A being Ordinal st On X c= A holds
b2 c= A ) ) );

theorem :: ORDINAL2:14
for A being Ordinal
for X being set st A in X holds
inf X c= A
proof end;

theorem :: ORDINAL2:15
for D being Ordinal
for X being set st On X <> 0 & ( for A being Ordinal st A in X holds
D c= A ) holds
D c= inf X
proof end;

theorem :: ORDINAL2:16
for A being Ordinal
for X, Y being set st A in X & X c= Y holds
inf Y c= inf X
proof end;

theorem :: ORDINAL2:17
for A being Ordinal
for X being set st A in X holds
inf X in X
proof end;

theorem Th18: :: ORDINAL2:18
for A being Ordinal holds sup A = A
proof end;

theorem Th19: :: ORDINAL2:19
for A being Ordinal
for X being set st A in X holds
A in sup X
proof end;

theorem Th20: :: ORDINAL2:20
for D being Ordinal
for X being set st ( for A being Ordinal st A in X holds
A in D ) holds
sup X c= D
proof end;

theorem :: ORDINAL2:21
for A being Ordinal
for X being set st A in sup X holds
ex B being Ordinal st
( B in X & A c= B )
proof end;

theorem :: ORDINAL2:22
for X, Y being set st X c= Y holds
sup X c= sup Y
proof end;

theorem :: ORDINAL2:23
for A being Ordinal holds sup {A} = succ A
proof end;

theorem :: ORDINAL2:24
for X being set holds inf X c= sup X
proof end;

scheme :: ORDINAL2:sch 2
TSLambda{ F1() -> Ordinal, F2( Ordinal) -> set } :
ex L being Sequence st
( dom L = F1() & ( for A being Ordinal st A in F1() holds
L . A = F2(A) ) )
proof end;

definition
let f be Function;
attr f is Ordinal-yielding means :Def4: :: ORDINAL2:def 4
 ex A being Ordinal st rng f c= A;
end;

:: deftheorem Def4 defines Ordinal-yielding ORDINAL2:def 4 :
for f being Function holds
( f is Ordinal-yielding iff ex A being Ordinal st rng f c= A );

registration
cluster Relation-like Sequence-like Function-like Ordinal-yielding for set ;
existence
ex b1 being Sequence st b1 is Ordinal-yielding
proof end;
end;

definition
mode Ordinal-Sequence is Ordinal-yielding Sequence;
end;

registration
let A be Ordinal;
cluster Relation-like A -valued Sequence-like Function-like -> Ordinal-yielding for set ;
coherence
for b1 being Sequence of A holds b1 is Ordinal-yielding by RELAT_1:def 19;
end;

registration
let L be Ordinal-Sequence;
let A be Ordinal;
cluster L | A -> Ordinal-yielding ;
coherence
L | A is Ordinal-yielding
proof end;
end;

theorem Th25: :: ORDINAL2:25
for A being Ordinal
for fi being Ordinal-Sequence st A in dom fi holds
fi . A is Ordinal
proof end;

registration
let f be Ordinal-Sequence;
let a be object ;
cluster f . a -> ordinal ;
coherence
f . a is ordinal
proof end;
end;

scheme :: ORDINAL2:sch 3
OSLambda{ F1() -> Ordinal, F2( Ordinal) -> Ordinal } :
ex fi being Ordinal-Sequence st
( dom fi = F1() & ( for A being Ordinal st A in F1() holds
fi . A = F2(A) ) )
proof end;

scheme :: ORDINAL2:sch 4
TSUniq1{ F1() -> Ordinal, F2() -> object , F3( Ordinal, set ) -> object , F4( Ordinal, Sequence) -> object , F5() -> Sequence, F6() -> Sequence } :
F5() = F6()
provided
A1: dom F5() = F1() and
A2: ( 0 in F1() implies F5() . 0 = F2() ) and
A3: for A being Ordinal st succ A in F1() holds
F5() . (succ A) = F3(A,(F5() . A)) and
A4: for A being Ordinal st A in F1() & A <> 0 & A is limit_ordinal holds
F5() . A = F4(A,(F5() | A)) and
A5: dom F6() = F1() and
A6: ( 0 in F1() implies F6() . 0 = F2() ) and
A7: for A being Ordinal st succ A in F1() holds
F6() . (succ A) = F3(A,(F6() . A)) and
A8: for A being Ordinal st A in F1() & A <> 0 & A is limit_ordinal holds
F6() . A = F4(A,(F6() | A))
proof end;

scheme :: ORDINAL2:sch 5
TSExist1{ F1() -> Ordinal, F2() -> object , F3( Ordinal, set ) -> object , F4( Ordinal, Sequence) -> object } :
ex L being Sequence st
( dom L = F1() & ( 0 in F1() implies L . 0 = F2() ) & ( for A being Ordinal st succ A in F1() holds
L . (succ A) = F3(A,(L . A)) ) & ( for A being Ordinal st A in F1() & A <> 0 & A is limit_ordinal holds
L . A = F4(A,(L | A)) ) )
proof end;

scheme :: ORDINAL2:sch 6
TSResult{ F1() -> Sequence, F2( Ordinal) -> set , F3() -> Ordinal, F4() -> set , F5( Ordinal, set ) -> set , F6( Ordinal, Sequence) -> set } :
for A being Ordinal st A in dom F1() holds
F1() . A = F2(A)
provided
A1: for A being Ordinal
for x being object holds
( x = F2(A) iff ex L being Sequence st
( x = last L & dom L = succ A & L . 0 = F4() & ( for C being Ordinal st succ C in succ A holds
L . (succ C) = F5(C,(L . C)) ) & ( for C being Ordinal st C in succ A & C <> 0 & C is limit_ordinal holds
L . C = F6(C,(L | C)) ) ) ) and
A2: dom F1() = F3() and
A3: ( 0 in F3() implies F1() . 0 = F4() ) and
A4: for A being Ordinal st succ A in F3() holds
F1() . (succ A) = F5(A,(F1() . A)) and
A5: for A being Ordinal st A in F3() & A <> 0 & A is limit_ordinal holds
F1() . A = F6(A,(F1() | A))
proof end;

scheme :: ORDINAL2:sch 7
TSDef{ F1() -> Ordinal, F2() -> set , F3( Ordinal, set ) -> set , F4( Ordinal, Sequence) -> set } :
( ex x being object ex L being Sequence st
( x = last L & dom L = succ F1() & L . 0 = F2() & ( for C being Ordinal st succ C in succ F1() holds
L . (succ C) = F3(C,(L . C)) ) & ( for C being Ordinal st C in succ F1() & C <> 0 & C is limit_ordinal holds
L . C = F4(C,(L | C)) ) ) & ( for x1, x2 being set st ex L being Sequence st
( x1 = last L & dom L = succ F1() & L . 0 = F2() & ( for C being Ordinal st succ C in succ F1() holds
L . (succ C) = F3(C,(L . C)) ) & ( for C being Ordinal st C in succ F1() & C <> 0 & C is limit_ordinal holds
L . C = F4(C,(L | C)) ) ) & ex L being Sequence st
( x2 = last L & dom L = succ F1() & L . 0 = F2() & ( for C being Ordinal st succ C in succ F1() holds
L . (succ C) = F3(C,(L . C)) ) & ( for C being Ordinal st C in succ F1() & C <> 0 & C is limit_ordinal holds
L . C = F4(C,(L | C)) ) ) holds
x1 = x2 ) )
proof end;

scheme :: ORDINAL2:sch 8
TSResult0{ F1( Ordinal) -> set , F2() -> set , F3( Ordinal, set ) -> set , F4( Ordinal, Sequence) -> set } :
F1(0) = F2()
provided
A1: for A being Ordinal
for x being object holds
( x = F1(A) iff ex L being Sequence st
( x = last L & dom L = succ A & L . 0 = F2() & ( for C being Ordinal st succ C in succ A holds
L . (succ C) = F3(C,(L . C)) ) & ( for C being Ordinal st C in succ A & C <> 0 & C is limit_ordinal holds
L . C = F4(C,(L | C)) ) ) )
proof end;

scheme :: ORDINAL2:sch 9
TSResultS{ F1() -> set , F2( Ordinal, set ) -> set , F3( Ordinal, Sequence) -> set , F4( Ordinal) -> set } :
for A being Ordinal holds F4((succ A)) = F2(A,F4(A))
provided
A1: for A being Ordinal
for x being object holds
( x = F4(A) iff ex L being Sequence st
( x = last L & dom L = succ A & L . 0 = F1() & ( for C being Ordinal st succ C in succ A holds
L . (succ C) = F2(C,(L . C)) ) & ( for C being Ordinal st C in succ A & C <> 0 & C is limit_ordinal holds
L . C = F3(C,(L | C)) ) ) )
proof end;

scheme :: ORDINAL2:sch 10
TSResultL{ F1() -> Sequence, F2() -> Ordinal, F3( Ordinal) -> set , F4() -> set , F5( Ordinal, set ) -> set , F6( Ordinal, Sequence) -> set } :
F3(F2()) = F6(F2(),F1())
provided
A1: for A being Ordinal
for x being object holds
( x = F3(A) iff ex L being Sequence st
( x = last L & dom L = succ A & L . 0 = F4() & ( for C being Ordinal st succ C in succ A holds
L . (succ C) = F5(C,(L . C)) ) & ( for C being Ordinal st C in succ A & C <> 0 & C is limit_ordinal holds
L . C = F6(C,(L | C)) ) ) ) and
A2: ( F2() <> 0 & F2() is limit_ordinal ) and
A3: dom F1() = F2() and
A4: for A being Ordinal st A in F2() holds
F1() . A = F3(A)
proof end;

scheme :: ORDINAL2:sch 11
OSExist{ F1() -> Ordinal, F2() -> Ordinal, F3( Ordinal, Ordinal) -> Ordinal, F4( Ordinal, Sequence) -> Ordinal } :
ex fi being Ordinal-Sequence st
( dom fi = F1() & ( 0 in F1() implies fi . 0 = F2() ) & ( for A being Ordinal st succ A in F1() holds
fi . (succ A) = F3(A,(fi . A)) ) & ( for A being Ordinal st A in F1() & A <> 0 & A is limit_ordinal holds
fi . A = F4(A,(fi | A)) ) )
proof end;

scheme :: ORDINAL2:sch 12
OSResult{ F1() -> Ordinal-Sequence, F2( Ordinal) -> Ordinal, F3() -> Ordinal, F4() -> Ordinal, F5( Ordinal, Ordinal) -> Ordinal, F6( Ordinal, Sequence) -> Ordinal } :
for A being Ordinal st A in dom F1() holds
F1() . A = F2(A)
provided
A1: for A, B being Ordinal holds
( B = F2(A) iff ex fi being Ordinal-Sequence st
( B = last fi & dom fi = succ A & fi . 0 = F4() & ( for C being Ordinal st succ C in succ A holds
fi . (succ C) = F5(C,(fi . C)) ) & ( for C being Ordinal st C in succ A & C <> 0 & C is limit_ordinal holds
fi . C = F6(C,(fi | C)) ) ) ) and
A2: dom F1() = F3() and
A3: ( 0 in F3() implies F1() . 0 = F4() ) and
A4: for A being Ordinal st succ A in F3() holds
F1() . (succ A) = F5(A,(F1() . A)) and
A5: for A being Ordinal st A in F3() & A <> 0 & A is limit_ordinal holds
F1() . A = F6(A,(F1() | A))
proof end;

scheme :: ORDINAL2:sch 13
OSDef{ F1() -> Ordinal, F2() -> Ordinal, F3( Ordinal, Ordinal) -> Ordinal, F4( Ordinal, Sequence) -> Ordinal } :
( ex A being Ordinal ex fi being Ordinal-Sequence st
( A = last fi & dom fi = succ F1() & fi . 0 = F2() & ( for C being Ordinal st succ C in succ F1() holds
fi . (succ C) = F3(C,(fi . C)) ) & ( for C being Ordinal st C in succ F1() & C <> 0 & C is limit_ordinal holds
fi . C = F4(C,(fi | C)) ) ) & ( for A1, A2 being Ordinal st ex fi being Ordinal-Sequence st
( A1 = last fi & dom fi = succ F1() & fi . 0 = F2() & ( for C being Ordinal st succ C in succ F1() holds
fi . (succ C) = F3(C,(fi . C)) ) & ( for C being Ordinal st C in succ F1() & C <> 0 & C is limit_ordinal holds
fi . C = F4(C,(fi | C)) ) ) & ex fi being Ordinal-Sequence st
( A2 = last fi & dom fi = succ F1() & fi . 0 = F2() & ( for C being Ordinal st succ C in succ F1() holds
fi . (succ C) = F3(C,(fi . C)) ) & ( for C being Ordinal st C in succ F1() & C <> 0 & C is limit_ordinal holds
fi . C = F4(C,(fi | C)) ) ) holds
A1 = A2 ) )
proof end;

scheme :: ORDINAL2:sch 14
OSResult0{ F1( Ordinal) -> Ordinal, F2() -> Ordinal, F3( Ordinal, Ordinal) -> Ordinal, F4( Ordinal, Sequence) -> Ordinal } :
F1(0) = F2()
provided
A1: for A, B being Ordinal holds
( B = F1(A) iff ex fi being Ordinal-Sequence st
( B = last fi & dom fi = succ A & fi . 0 = F2() & ( for C being Ordinal st succ C in succ A holds
fi . (succ C) = F3(C,(fi . C)) ) & ( for C being Ordinal st C in succ A & C <> 0 & C is limit_ordinal holds
fi . C = F4(C,(fi | C)) ) ) )
proof end;

scheme :: ORDINAL2:sch 15
OSResultS{ F1() -> Ordinal, F2( Ordinal, Ordinal) -> Ordinal, F3( Ordinal, Sequence) -> Ordinal, F4( Ordinal) -> Ordinal } :
for A being Ordinal holds F4((succ A)) = F2(A,F4(A))
provided
A1: for A, B being Ordinal holds
( B = F4(A) iff ex fi being Ordinal-Sequence st
( B = last fi & dom fi = succ A & fi . 0 = F1() & ( for C being Ordinal st succ C in succ A holds
fi . (succ C) = F2(C,(fi . C)) ) & ( for C being Ordinal st C in succ A & C <> 0 & C is limit_ordinal holds
fi . C = F3(C,(fi | C)) ) ) )
proof end;

scheme :: ORDINAL2:sch 16
OSResultL{ F1() -> Ordinal-Sequence, F2() -> Ordinal, F3( Ordinal) -> Ordinal, F4() -> Ordinal, F5( Ordinal, Ordinal) -> Ordinal, F6( Ordinal, Sequence) -> Ordinal } :
F3(F2()) = F6(F2(),F1())
provided
A1: for A, B being Ordinal holds
( B = F3(A) iff ex fi being Ordinal-Sequence st
( B = last fi & dom fi = succ A & fi . 0 = F4() & ( for C being Ordinal st succ C in succ A holds
fi . (succ C) = F5(C,(fi . C)) ) & ( for C being Ordinal st C in succ A & C <> 0 & C is limit_ordinal holds
fi . C = F6(C,(fi | C)) ) ) ) and
A2: ( F2() <> 0 & F2() is limit_ordinal ) and
A3: dom F1() = F2() and
A4: for A being Ordinal st A in F2() holds
F1() . A = F3(A)
proof end;

definition
let L be Sequence;
func sup L -> Ordinal equals :: ORDINAL2:def 5
 sup (rng L);
correctness
coherence
sup (rng L) is Ordinal;
;
func inf L -> Ordinal equals :: ORDINAL2:def 6
 inf (rng L);
correctness
coherence
inf (rng L) is Ordinal;
;
end;

:: deftheorem defines sup ORDINAL2:def 5 :
for L being Sequence holds sup L = sup (rng L);

:: deftheorem defines inf ORDINAL2:def 6 :
for L being Sequence holds inf L = inf (rng L);

theorem :: ORDINAL2:26
for L being Sequence holds
( sup L = sup (rng L) & inf L = inf (rng L) ) ;

definition
let L be Sequence;
func lim_sup L -> Ordinal means :: ORDINAL2:def 7
 ex fi being Ordinal-Sequence st
( it = inf fi & dom fi = dom L & ( for A being Ordinal st A in dom L holds
fi . A = sup (rng (L | ((dom L) \ A))) ) );
existence
ex b1 being Ordinal ex fi being Ordinal-Sequence st
( b1 = inf fi & dom fi = dom L & ( for A being Ordinal st A in dom L holds
fi . A = sup (rng (L | ((dom L) \ A))) ) )
proof end;
uniqueness
for b1, b2 being Ordinal st ex fi being Ordinal-Sequence st
( b1 = inf fi & dom fi = dom L & ( for A being Ordinal st A in dom L holds
fi . A = sup (rng (L | ((dom L) \ A))) ) ) & ex fi being Ordinal-Sequence st
( b2 = inf fi & dom fi = dom L & ( for A being Ordinal st A in dom L holds
fi . A = sup (rng (L | ((dom L) \ A))) ) ) holds
b1 = b2
proof end;
func lim_inf L -> Ordinal means :: ORDINAL2:def 8
 ex fi being Ordinal-Sequence st
( it = sup fi & dom fi = dom L & ( for A being Ordinal st A in dom L holds
fi . A = inf (rng (L | ((dom L) \ A))) ) );
existence
ex b1 being Ordinal ex fi being Ordinal-Sequence st
( b1 = sup fi & dom fi = dom L & ( for A being Ordinal st A in dom L holds
fi . A = inf (rng (L | ((dom L) \ A))) ) )
proof end;
uniqueness
for b1, b2 being Ordinal st ex fi being Ordinal-Sequence st
( b1 = sup fi & dom fi = dom L & ( for A being Ordinal st A in dom L holds
fi . A = inf (rng (L | ((dom L) \ A))) ) ) & ex fi being Ordinal-Sequence st
( b2 = sup fi & dom fi = dom L & ( for A being Ordinal st A in dom L holds
fi . A = inf (rng (L | ((dom L) \ A))) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem defines lim_sup ORDINAL2:def 7 :
for L being Sequence
for b2 being Ordinal holds
( b2 = lim_sup L iff ex fi being Ordinal-Sequence st
( b2 = inf fi & dom fi = dom L & ( for A being Ordinal st A in dom L holds
fi . A = sup (rng (L | ((dom L) \ A))) ) ) );

:: deftheorem defines lim_inf ORDINAL2:def 8 :
for L being Sequence
for b2 being Ordinal holds
( b2 = lim_inf L iff ex fi being Ordinal-Sequence st
( b2 = sup fi & dom fi = dom L & ( for A being Ordinal st A in dom L holds
fi . A = inf (rng (L | ((dom L) \ A))) ) ) );

definition
let A be Ordinal;
let fi be Ordinal-Sequence;
pred A is_limes_of fi means :Def9: :: ORDINAL2:def 9
 ex B being Ordinal st
( B in dom fi & ( for C being Ordinal st B c= C & C in dom fi holds
fi . C = 0 ) ) if A = 0
otherwise for B, C being Ordinal st B in A & A in C holds
ex D being Ordinal st
( D in dom fi & ( for E being Ordinal st D c= E & E in dom fi holds
( B in fi . E & fi . E in C ) ) );
consistency
verum ;
end;

:: deftheorem Def9 defines is_limes_of ORDINAL2:def 9 :
for A being Ordinal
for fi being Ordinal-Sequence holds
( ( A = 0 implies ( A is_limes_of fi iff ex B being Ordinal st
( B in dom fi & ( for C being Ordinal st B c= C & C in dom fi holds
fi . C = 0 ) ) ) ) & ( not A = 0 implies ( A is_limes_of fi iff for B, C being Ordinal st B in A & A in C holds
ex D being Ordinal st
( D in dom fi & ( for E being Ordinal st D c= E & E in dom fi holds
( B in fi . E & fi . E in C ) ) ) ) ) );

definition
let fi be Ordinal-Sequence;
given A being Ordinal such that A1: A is_limes_of fi ;
func lim fi -> Ordinal means :Def10: :: ORDINAL2:def 10
it is_limes_of fi;
existence
ex b1 being Ordinal st b1 is_limes_of fi by A1;
uniqueness
for b1, b2 being Ordinal st b1 is_limes_of fi & b2 is_limes_of fi holds
b1 = b2
proof end;
end;

:: deftheorem Def10 defines lim ORDINAL2:def 10 :
for fi being Ordinal-Sequence st ex A being Ordinal st A is_limes_of fi holds
for b2 being Ordinal holds
( b2 = lim fi iff b2 is_limes_of fi );

definition
let A be Ordinal;
let fi be Ordinal-Sequence;
func lim (A,fi) -> Ordinal equals :: ORDINAL2:def 11
 lim (fi | A);
correctness
coherence
lim (fi | A) is Ordinal;
;
end;

:: deftheorem defines lim ORDINAL2:def 11 :
for A being Ordinal
for fi being Ordinal-Sequence holds lim (A,fi) = lim (fi | A);

definition
let L be Ordinal-Sequence;
attr L is increasing means :: ORDINAL2:def 12
 for A, B being Ordinal st A in B & B in dom L holds
L . A in L . B;
attr L is continuous means :: ORDINAL2:def 13
 for A, B being Ordinal st A in dom L & A <> 0 & A is limit_ordinal & B = L . A holds
B is_limes_of L | A;
end;

:: deftheorem defines increasing ORDINAL2:def 12 :
for L being Ordinal-Sequence holds
( L is increasing iff for A, B being Ordinal st A in B & B in dom L holds
L . A in L . B );

:: deftheorem defines continuous ORDINAL2:def 13 :
for L being Ordinal-Sequence holds
( L is continuous iff for A, B being Ordinal st A in dom L & A <> 0 & A is limit_ordinal & B = L . A holds
B is_limes_of L | A );

definition
let A, B be Ordinal;
func A +^ B -> Ordinal means :Def14: :: ORDINAL2:def 14
 ex fi being Ordinal-Sequence st
( it = last fi & dom fi = succ B & fi . 0 = A & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = succ (fi . C) ) & ( for C being Ordinal st C in succ B & C <> 0 & C is limit_ordinal holds
fi . C = sup (fi | C) ) );
correctness
existence
ex b1 being Ordinal ex fi being Ordinal-Sequence st
( b1 = last fi & dom fi = succ B & fi . 0 = A & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = succ (fi . C) ) & ( for C being Ordinal st C in succ B & C <> 0 & C is limit_ordinal holds
fi . C = sup (fi | C) ) );
uniqueness
for b1, b2 being Ordinal st ex fi being Ordinal-Sequence st
( b1 = last fi & dom fi = succ B & fi . 0 = A & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = succ (fi . C) ) & ( for C being Ordinal st C in succ B & C <> 0 & C is limit_ordinal holds
fi . C = sup (fi | C) ) ) & ex fi being Ordinal-Sequence st
( b2 = last fi & dom fi = succ B & fi . 0 = A & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = succ (fi . C) ) & ( for C being Ordinal st C in succ B & C <> 0 & C is limit_ordinal holds
fi . C = sup (fi | C) ) ) holds
b1 = b2;
proof end;
end;

:: deftheorem Def14 defines +^ ORDINAL2:def 14 :
for A, B, b3 being Ordinal holds
( b3 = A +^ B iff ex fi being Ordinal-Sequence st
( b3 = last fi & dom fi = succ B & fi . 0 = A & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = succ (fi . C) ) & ( for C being Ordinal st C in succ B & C <> 0 & C is limit_ordinal holds
fi . C = sup (fi | C) ) ) );

definition
let A, B be Ordinal;
func A *^ B -> Ordinal means :Def15: :: ORDINAL2:def 15
 ex fi being Ordinal-Sequence st
( it = last fi & dom fi = succ A & fi . 0 = 0 & ( for C being Ordinal st succ C in succ A holds
fi . (succ C) = (fi . C) +^ B ) & ( for C being Ordinal st C in succ A & C <> 0 & C is limit_ordinal holds
fi . C = union (sup (fi | C)) ) );
correctness
existence
ex b1 being Ordinal ex fi being Ordinal-Sequence st
( b1 = last fi & dom fi = succ A & fi . 0 = 0 & ( for C being Ordinal st succ C in succ A holds
fi . (succ C) = (fi . C) +^ B ) & ( for C being Ordinal st C in succ A & C <> 0 & C is limit_ordinal holds
fi . C = union (sup (fi | C)) ) );
uniqueness
for b1, b2 being Ordinal st ex fi being Ordinal-Sequence st
( b1 = last fi & dom fi = succ A & fi . 0 = 0 & ( for C being Ordinal st succ C in succ A holds
fi . (succ C) = (fi . C) +^ B ) & ( for C being Ordinal st C in succ A & C <> 0 & C is limit_ordinal holds
fi . C = union (sup (fi | C)) ) ) & ex fi being Ordinal-Sequence st
( b2 = last fi & dom fi = succ A & fi . 0 = 0 & ( for C being Ordinal st succ C in succ A holds
fi . (succ C) = (fi . C) +^ B ) & ( for C being Ordinal st C in succ A & C <> 0 & C is limit_ordinal holds
fi . C = union (sup (fi | C)) ) ) holds
b1 = b2;
proof end;
end;

:: deftheorem Def15 defines *^ ORDINAL2:def 15 :
for A, B, b3 being Ordinal holds
( b3 = A *^ B iff ex fi being Ordinal-Sequence st
( b3 = last fi & dom fi = succ A & fi . 0 = 0 & ( for C being Ordinal st succ C in succ A holds
fi . (succ C) = (fi . C) +^ B ) & ( for C being Ordinal st C in succ A & C <> 0 & C is limit_ordinal holds
fi . C = union (sup (fi | C)) ) ) );

registration
let O be Ordinal;
cluster -> ordinal for Element of O;
coherence
for b1 being Element of O holds b1 is ordinal ;
end;

definition
let A, B be Ordinal;
func exp (A,B) -> Ordinal means :Def16: :: ORDINAL2:def 16
 ex fi being Ordinal-Sequence st
( it = last fi & dom fi = succ B & fi . 0 = 1 & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = A *^ (fi . C) ) & ( for C being Ordinal st C in succ B & C <> 0 & C is limit_ordinal holds
fi . C = lim (fi | C) ) );
correctness
existence
ex b1 being Ordinal ex fi being Ordinal-Sequence st
( b1 = last fi & dom fi = succ B & fi . 0 = 1 & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = A *^ (fi . C) ) & ( for C being Ordinal st C in succ B & C <> 0 & C is limit_ordinal holds
fi . C = lim (fi | C) ) );
uniqueness
for b1, b2 being Ordinal st ex fi being Ordinal-Sequence st
( b1 = last fi & dom fi = succ B & fi . 0 = 1 & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = A *^ (fi . C) ) & ( for C being Ordinal st C in succ B & C <> 0 & C is limit_ordinal holds
fi . C = lim (fi | C) ) ) & ex fi being Ordinal-Sequence st
( b2 = last fi & dom fi = succ B & fi . 0 = 1 & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = A *^ (fi . C) ) & ( for C being Ordinal st C in succ B & C <> 0 & C is limit_ordinal holds
fi . C = lim (fi | C) ) ) holds
b1 = b2;
proof end;
end;

:: deftheorem Def16 defines exp ORDINAL2:def 16 :
for A, B, b3 being Ordinal holds
( b3 = exp (A,B) iff ex fi being Ordinal-Sequence st
( b3 = last fi & dom fi = succ B & fi . 0 = 1 & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = A *^ (fi . C) ) & ( for C being Ordinal st C in succ B & C <> 0 & C is limit_ordinal holds
fi . C = lim (fi | C) ) ) );

theorem Th27: :: ORDINAL2:27
for A being Ordinal holds A +^ 0 = A
proof end;

theorem Th28: :: ORDINAL2:28
for A, B being Ordinal holds A +^ (succ B) = succ (A +^ B)
proof end;

theorem Th29: :: ORDINAL2:29
for A, B being Ordinal st B <> 0 & B is limit_ordinal holds
for fi being Ordinal-Sequence st dom fi = B & ( for C being Ordinal st C in B holds
fi . C = A +^ C ) holds
A +^ B = sup fi
proof end;

theorem Th30: :: ORDINAL2:30
for A being Ordinal holds 0 +^ A = A
proof end;

Lm1: 1 = succ 0
;

theorem :: ORDINAL2:31
for A being Ordinal holds A +^ 1 = succ A
proof end;

theorem Th32: :: ORDINAL2:32
for A, B, C being Ordinal st A in B holds
C +^ A in C +^ B
proof end;

theorem Th33: :: ORDINAL2:33
for A, B, C being Ordinal st A c= B holds
C +^ A c= C +^ B
proof end;

theorem Th34: :: ORDINAL2:34
for A, B, C being Ordinal st A c= B holds
A +^ C c= B +^ C
proof end;

theorem Th35: :: ORDINAL2:35
for A being Ordinal holds 0 *^ A = 0
proof end;

theorem Th36: :: ORDINAL2:36
for A, B being Ordinal holds (succ B) *^ A = (B *^ A) +^ A
proof end;

theorem Th37: :: ORDINAL2:37
for A, B being Ordinal st B <> 0 & B is limit_ordinal holds
for fi being Ordinal-Sequence st dom fi = B & ( for C being Ordinal st C in B holds
fi . C = C *^ A ) holds
B *^ A = union (sup fi)
proof end;

theorem Th38: :: ORDINAL2:38
for A being Ordinal holds A *^ 0 = 0
proof end;

theorem Th39: :: ORDINAL2:39
for A being Ordinal holds
( 1 *^ A = A & A *^ 1 = A )
proof end;

theorem Th40: :: ORDINAL2:40
for A, B, C being Ordinal st C <> 0 & A in B holds
A *^ C in B *^ C
proof end;

theorem :: ORDINAL2:41
for A, B, C being Ordinal st A c= B holds
A *^ C c= B *^ C
proof end;

theorem :: ORDINAL2:42
for A, B, C being Ordinal st A c= B holds
C *^ A c= C *^ B
proof end;

theorem Th43: :: ORDINAL2:43
for A being Ordinal holds exp (A,0) = 1
proof end;

theorem Th44: :: ORDINAL2:44
for A, B being Ordinal holds exp (A,(succ B)) = A *^ (exp (A,B))
proof end;

theorem Th45: :: ORDINAL2:45
for A, B being Ordinal st B <> 0 & B is limit_ordinal holds
for fi being Ordinal-Sequence st dom fi = B & ( for C being Ordinal st C in B holds
fi . C = exp (A,C) ) holds
exp (A,B) = lim fi
proof end;

theorem :: ORDINAL2:46
for A being Ordinal holds
( exp (A,1) = A & exp (1,A) = 1 )
proof end;

theorem :: ORDINAL2:47
for A being Ordinal ex B, C being Ordinal st
( B is limit_ordinal & C is natural & A = B +^ C )
proof end;

:: 2005.05.04, A.T.
registration
let X be set ;
let o be Ordinal;
cluster X --> o -> Ordinal-yielding ;
coherence
X --> o is Ordinal-yielding
proof end;
end;

registration
let O be Ordinal;
let x be object ;
cluster O --> x -> Sequence-like ;
coherence
O --> x is Sequence-like ;
end;

:: from ZFREFLE1, 2007.03.14, A.T.
definition
let A, B be Ordinal;
pred A is_cofinal_with B means :: ORDINAL2:def 17
 ex xi being Ordinal-Sequence st
( dom xi = B & rng xi c= A & xi is increasing & A = sup xi );
reflexivity
for A being Ordinal ex xi being Ordinal-Sequence st
( dom xi = A & rng xi c= A & xi is increasing & A = sup xi )
proof end;
end;

:: deftheorem defines is_cofinal_with ORDINAL2:def 17 :
for A, B being Ordinal holds
( A is_cofinal_with B iff ex xi being Ordinal-Sequence st
( dom xi = B & rng xi c= A & xi is increasing & A = sup xi ) );

theorem Th48: :: ORDINAL2:48
for psi being Ordinal-Sequence
for e being set st e in rng psi holds
e is Ordinal
proof end;

theorem :: ORDINAL2:49
for psi being Ordinal-Sequence holds rng psi c= sup psi
proof end;

theorem :: ORDINAL2:50
for A being Ordinal st A is_cofinal_with 0 holds
A = 0
proof end;

:: from ARYTM_3, 2007.10.23, A.T.
scheme :: ORDINAL2:sch 17
OmegaInd{ F1() -> Nat, P1[ object ] } :
P1[F1()]
provided
A1: P1[ 0 ] and
A2: for a being Nat st P1[a] holds
P1[ succ a]
proof end;

registration
let a, b be Nat;
cluster a +^ b -> natural ;
coherence
a +^ b is natural
proof end;
end;

:: from AMI_2, 2008.02.14, A.T.
registration
let x, y be set ;
let a, b be Nat;
cluster IFEQ (x,y,a,b) -> natural ;
coherence
IFEQ (x,y,a,b) is natural
proof end;
end;

:: 2010.03.16, A.T.
scheme :: ORDINAL2:sch 18
LambdaRecEx{ F1() -> set , F2( set , set ) -> set } :
ex f being Function st
( dom f = omega & f . 0 = F1() & ( for n being Nat holds f . (succ n) = F2(n,(f . n)) ) )
proof end;

scheme :: ORDINAL2:sch 19
RecUn{ F1() -> set , F2() -> Function, F3() -> Function, P1[ set , set , set ] } :
F2() = F3()
provided
A1: dom F2() = omega and
A2: F2() . 0 = F1() and
A3: for n being Nat holds P1[n,F2() . n,F2() . (succ n)] and
A4: dom F3() = omega and
A5: F3() . 0 = F1() and
A6: for n being Nat holds P1[n,F3() . n,F3() . (succ n)] and
A7: for n being Nat
for x, y1, y2 being set st P1[n,x,y1] & P1[n,x,y2] holds
y1 = y2
proof end;

scheme :: ORDINAL2:sch 20
LambdaRecUn{ F1() -> set , F2( set , set ) -> set , F3() -> Function, F4() -> Function } :
F3() = F4()
provided
A1: dom F3() = omega and
A2: F3() . 0 = F1() and
A3: for n being Nat holds F3() . (succ n) = F2(n,(F3() . n)) and
A4: dom F4() = omega and
A5: F4() . 0 = F1() and
A6: for n being Nat holds F4() . (succ n) = F2(n,(F4() . n))
proof end;