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


begin

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

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

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

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

theorem :: ORDINAL2:4
{} is limit_ordinal
proofend;

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

definition
let L be T-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 T-Sequence holds last L = L . (union (dom L));

theorem :: ORDINAL2:6
for A being Ordinal
for L being T-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
proofend;

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

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

theorem :: ORDINAL2:10
for X being set holds Lim X c= X
proofend;

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

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

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

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

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

theorem :: ORDINAL2:15
for D being Ordinal
for X being set st On X <> {} &amp; ( for A being Ordinal st A in X holds
D c= A ) holds
D c= inf X
proofend;

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

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

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

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

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

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 &amp; A c= B )
proofend;

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

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

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

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

definition
let f be Function;
attrf 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 T-Sequence-like Relation-like Function-like Ordinal-yielding for set ;
existence
 ex b1 being T-Sequence st b1 is Ordinal-yielding
proofend;
end;

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

registration
let A be Ordinal;
cluster T-Sequence-like Relation-like A -valued Function-like  ->  Ordinal-yielding for set ;
coherence
 for b1 being T-Sequence of holds b1 is Ordinal-yielding
proofend;
end;

registration
let L be Ordinal-Sequence;
let A be Ordinal;
clusterL | A ->  Ordinal-yielding ;
coherence
 L | A is Ordinal-yielding
proofend;
end;

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

registration
let f be Ordinal-Sequence;
let a be Ordinal;
clusterf . a ->  ordinal ;
coherence
 f . a is ordinal
proofend;
end;

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

scheme :: ORDINAL2:sch 4
TSUniq1{ F1() ->  Ordinal, F2() ->  set , F3( Ordinal, set ) ->  set , F4( Ordinal, T-Sequence) ->  set , F5() ->  T-Sequence, F6() ->  T-Sequence } :
 F5() = F6()
provided
A1: dom F5() = F1() and
A2: ( {} in F1() implies F5() . {} = 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() &amp; A <> {} &amp; A is limit_ordinal holds
F5() . A = F4(A,(F5() | A)) and
A5: dom F6() = F1() and
A6: ( {} in F1() implies F6() . {} = 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() &amp; A <> {} &amp; A is limit_ordinal holds
F6() . A = F4(A,(F6() | A))
proofend;

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

scheme :: ORDINAL2:sch 6
TSResult{ F1() ->  T-Sequence, F2( Ordinal) ->  set , F3() ->  Ordinal, F4() ->  set , F5( Ordinal, set ) ->  set , F6( Ordinal, T-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 set holds
( x = F2(A) iff ex L being T-Sequence st
( x = last L &amp; dom L = succ A &amp; L . {} = F4() &amp; ( for C being Ordinal st succ C in succ A holds
L . (succ C) = F5(C,(L . C)) ) &amp; ( for C being Ordinal st C in succ A &amp; C <> {} &amp; C is limit_ordinal holds
L . C = F6(C,(L | C)) ) ) ) and
A2: dom F1() = F3() and
A3: ( {} in F3() implies F1() . {} = 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() &amp; A <> {} &amp; A is limit_ordinal holds
F1() . A = F6(A,(F1() | A))
proofend;

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

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

scheme :: ORDINAL2:sch 9
TSResultS{ F1() ->  set , F2( Ordinal, set ) ->  set , F3( Ordinal, T-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 set holds
( x = F4(A) iff ex L being T-Sequence st
( x = last L &amp; dom L = succ A &amp; L . {} = F1() &amp; ( for C being Ordinal st succ C in succ A holds
L . (succ C) = F2(C,(L . C)) ) &amp; ( for C being Ordinal st C in succ A &amp; C <> {} &amp; C is limit_ordinal holds
L . C = F3(C,(L | C)) ) ) )
proofend;

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

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

scheme :: ORDINAL2:sch 12
OSResult{ F1() ->  Ordinal-Sequence, F2( Ordinal) ->  Ordinal, F3() ->  Ordinal, F4() ->  Ordinal, F5( Ordinal, Ordinal) ->  Ordinal, F6( Ordinal, T-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 &amp; dom fi = succ A &amp; fi . {} = F4() &amp; ( for C being Ordinal st succ C in succ A holds
fi . (succ C) = F5(C,(fi . C)) ) &amp; ( for C being Ordinal st C in succ A &amp; C <> {} &amp; C is limit_ordinal holds
fi . C = F6(C,(fi | C)) ) ) ) and
A2: dom F1() = F3() and
A3: ( {} in F3() implies F1() . {} = 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() &amp; A <> {} &amp; A is limit_ordinal holds
F1() . A = F6(A,(F1() | A))
proofend;

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

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

scheme :: ORDINAL2:sch 15
OSResultS{ F1() ->  Ordinal, F2( Ordinal, Ordinal) ->  Ordinal, F3( Ordinal, T-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 &amp; dom fi = succ A &amp; fi . {} = F1() &amp; ( for C being Ordinal st succ C in succ A holds
fi . (succ C) = F2(C,(fi . C)) ) &amp; ( for C being Ordinal st C in succ A &amp; C <> {} &amp; C is limit_ordinal holds
fi . C = F3(C,(fi | C)) ) ) )
proofend;

scheme :: ORDINAL2:sch 16
OSResultL{ F1() ->  Ordinal-Sequence, F2() ->  Ordinal, F3( Ordinal) ->  Ordinal, F4() ->  Ordinal, F5( Ordinal, Ordinal) ->  Ordinal, F6( Ordinal, T-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 &amp; dom fi = succ A &amp; fi . {} = F4() &amp; ( for C being Ordinal st succ C in succ A holds
fi . (succ C) = F5(C,(fi . C)) ) &amp; ( for C being Ordinal st C in succ A &amp; C <> {} &amp; C is limit_ordinal holds
fi . C = F6(C,(fi | C)) ) ) ) and
A2: ( F2() <> {} &amp; F2() is limit_ordinal ) and
A3: dom F1() = F2() and
A4: for A being Ordinal st A in F2() holds
F1() . A = F3(A)
proofend;

definition
let L be T-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 T-Sequence holds sup L = sup (rng L);

:: deftheorem  defines inf ORDINAL2:def_6_:_
 for L being T-Sequence holds inf L = inf (rng L);

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

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

:: deftheorem  defines lim_sup ORDINAL2:def_7_:_
 for L being T-Sequence
for b2 being Ordinal holds
( b2 = lim_sup L iff ex fi being Ordinal-Sequence st
( b2 = inf fi &amp; dom fi = dom L &amp; ( 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 T-Sequence
for b2 being Ordinal holds
( b2 = lim_inf L iff ex fi being Ordinal-Sequence st
( b2 = sup fi &amp; dom fi = dom L &amp; ( 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;
predA is_limes_of fi means :Def9: :: ORDINAL2:def 9
 ex B being Ordinal st
( B in dom fi &amp; ( for C being Ordinal st B c= C &amp; C in dom fi holds
fi . C = {} ) ) if A = {}
otherwise  for B, C being Ordinal st B in A &amp; A in C holds
ex D being Ordinal st
( D in dom fi &amp; ( for E being Ordinal st D c= E &amp; E in dom fi holds
( B in fi . E &amp; 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 = {} implies ( A is_limes_of fi iff ex B being Ordinal st
( B in dom fi &amp; ( for C being Ordinal st B c= C &amp; C in dom fi holds
fi . C = {} ) ) ) ) &amp; ( not A = {} implies ( A is_limes_of fi iff for B, C being Ordinal st B in A &amp; A in C holds
ex D being Ordinal st
( D in dom fi &amp; ( for E being Ordinal st D c= E &amp; E in dom fi holds
( B in fi . E &amp; 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 &amp; b2 is_limes_of fi holds
b1 = b2
proofend;
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;
attrL is increasing  means :: ORDINAL2:def 12
 for A, B being Ordinal st A in B &amp; B in dom L holds
L . A in L . B;
attrL is continuous  means :: ORDINAL2:def 13
 for A, B being Ordinal st A in dom L &amp; A <> {} &amp; A is limit_ordinal &amp; 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 &amp; 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 &amp; A <> {} &amp; A is limit_ordinal &amp; B = L . A holds
B is_limes_of L | A );

definition
let A, B be Ordinal;
funcA +^ B ->  Ordinal means :Def14: :: ORDINAL2:def 14
 ex fi being Ordinal-Sequence st
( it = last fi &amp; dom fi = succ B &amp; fi . {} = A &amp; ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = succ (fi . C) ) &amp; ( for C being Ordinal st C in succ B &amp; C <> {} &amp; 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 &amp; dom fi = succ B &amp; fi . {} = A &amp; ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = succ (fi . C) ) &amp; ( for C being Ordinal st C in succ B &amp; C <> {} &amp; 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 &amp; dom fi = succ B &amp; fi . {} = A &amp; ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = succ (fi . C) ) &amp; ( for C being Ordinal st C in succ B &amp; C <> {} &amp; C is limit_ordinal holds
fi . C = sup (fi | C) ) ) &amp; ex fi being Ordinal-Sequence st
( b2 = last fi &amp; dom fi = succ B &amp; fi . {} = A &amp; ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = succ (fi . C) ) &amp; ( for C being Ordinal st C in succ B &amp; C <> {} &amp; C is limit_ordinal holds
fi . C = sup (fi | C) ) ) holds
b1 = b2;
proofend;
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 &amp; dom fi = succ B &amp; fi . {} = A &amp; ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = succ (fi . C) ) &amp; ( for C being Ordinal st C in succ B &amp; C <> {} &amp; C is limit_ordinal holds
fi . C = sup (fi | C) ) ) );

definition
let A, B be Ordinal;
funcA *^ B ->  Ordinal means :Def15: :: ORDINAL2:def 15
 ex fi being Ordinal-Sequence st
( it = last fi &amp; dom fi = succ A &amp; fi . {} = {} &amp; ( for C being Ordinal st succ C in succ A holds
fi . (succ C) = (fi . C) +^ B ) &amp; ( for C being Ordinal st C in succ A &amp; C <> {} &amp; 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 &amp; dom fi = succ A &amp; fi . {} = {} &amp; ( for C being Ordinal st succ C in succ A holds
fi . (succ C) = (fi . C) +^ B ) &amp; ( for C being Ordinal st C in succ A &amp; C <> {} &amp; 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 &amp; dom fi = succ A &amp; fi . {} = {} &amp; ( for C being Ordinal st succ C in succ A holds
fi . (succ C) = (fi . C) +^ B ) &amp; ( for C being Ordinal st C in succ A &amp; C <> {} &amp; C is limit_ordinal holds
fi . C = union (sup (fi | C)) ) ) &amp; ex fi being Ordinal-Sequence st
( b2 = last fi &amp; dom fi = succ A &amp; fi . {} = {} &amp; ( for C being Ordinal st succ C in succ A holds
fi . (succ C) = (fi . C) +^ B ) &amp; ( for C being Ordinal st C in succ A &amp; C <> {} &amp; C is limit_ordinal holds
fi . C = union (sup (fi | C)) ) ) holds
b1 = b2;
proofend;
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 &amp; dom fi = succ A &amp; fi . {} = {} &amp; ( for C being Ordinal st succ C in succ A holds
fi . (succ C) = (fi . C) +^ B ) &amp; ( for C being Ordinal st C in succ A &amp; C <> {} &amp; 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 &amp; dom fi = succ B &amp; fi . {} = 1 &amp; ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = A *^ (fi . C) ) &amp; ( for C being Ordinal st C in succ B &amp; C <> {} &amp; 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 &amp; dom fi = succ B &amp; fi . {} = 1 &amp; ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = A *^ (fi . C) ) &amp; ( for C being Ordinal st C in succ B &amp; C <> {} &amp; 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 &amp; dom fi = succ B &amp; fi . {} = 1 &amp; ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = A *^ (fi . C) ) &amp; ( for C being Ordinal st C in succ B &amp; C <> {} &amp; C is limit_ordinal holds
fi . C = lim (fi | C) ) ) &amp; ex fi being Ordinal-Sequence st
( b2 = last fi &amp; dom fi = succ B &amp; fi . {} = 1 &amp; ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = A *^ (fi . C) ) &amp; ( for C being Ordinal st C in succ B &amp; C <> {} &amp; C is limit_ordinal holds
fi . C = lim (fi | C) ) ) holds
b1 = b2;
proofend;
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 &amp; dom fi = succ B &amp; fi . {} = 1 &amp; ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = A *^ (fi . C) ) &amp; ( for C being Ordinal st C in succ B &amp; C <> {} &amp; C is limit_ordinal holds
fi . C = lim (fi | C) ) ) );

theorem Th27: :: ORDINAL2:27
for A being Ordinal holds A +^ {} = A
proofend;

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

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

theorem Th30: :: ORDINAL2:30
for A being Ordinal holds {} +^ A = A
proofend;

Lm1:  1 = succ {}
;

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

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

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

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

theorem Th35: :: ORDINAL2:35
for A being Ordinal holds {} *^ A = {}
proofend;

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

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

theorem Th38: :: ORDINAL2:38
for A being Ordinal holds A *^ {} = {}
proofend;

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

theorem Th40: :: ORDINAL2:40
for C, A, B being Ordinal st C <> {} &amp; A in B holds
A *^ C in B *^ C
proofend;

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

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

theorem Th43: :: ORDINAL2:43
for A being Ordinal holds exp (A,{}) = 1
proofend;

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

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

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

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

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

registration
let O be Ordinal;
let x be set ;
clusterO --> x ->  T-Sequence-like ;
coherence
 O --> x is T-Sequence-like
proofend;
end;

:: from ZFREFLE1, 2007.03.14, A.T.
definition
let A, B be Ordinal;
predA is_cofinal_with B means :: ORDINAL2:def 17
 ex xi being Ordinal-Sequence st
( dom xi = B &amp; rng xi c= A &amp; xi is increasing &amp; A = sup xi );
reflexivity
 for A being Ordinal ex xi being Ordinal-Sequence st
( dom xi = A &amp; rng xi c= A &amp; xi is increasing &amp; A = sup xi )
proofend;
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 &amp; rng xi c= A &amp; xi is increasing &amp; 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
proofend;

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

theorem :: ORDINAL2:50
for A being Ordinal st A is_cofinal_with {} holds
A = {}
proofend;

scheme :: ORDINAL2:sch 17
OmegaInd{ F1() ->  Nat, P1[ set ] } :
 P1[F1()]
provided
A1: P1[ {} ] and
A2: for a being Nat st P1[a] holds
P1[ succ a]
proofend;

registration
let a, b be Nat;
clustera +^ b ->  natural ;
coherence
 a +^ b is natural
proofend;
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
proofend;
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 &amp; f . {} = F1() &amp; ( for n being Nat holds f . (succ n) = F2(n,(f . n)) ) )
proofend;

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() . {} = F1() and
A3: for n being Nat holds P1[n,F2() . n,F2() . (succ n)] and
A4: dom F3() = omega and
A5: F3() . {} = 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] &amp; P1[n,x,y2] holds
y1 = y2
proofend;

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() . {} = F1() and
A3: for n being Nat holds F3() . (succ n) = F2(n,(F3() . n)) and
A4: dom F4() = omega and
A5: F4() . {} = F1() and
A6: for n being Nat holds F4() . (succ n) = F2(n,(F4() . n))
proofend;