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

begin

scheme :: ORDINAL2:sch 1
OrdinalInd{ P₁[ Ordinal] } :

for A being Ordinal holds P₁[A]

provided

A1: P₁[ {} ] and
A2: for A being Ordinal st P₁[A] holds
P₁[ succ A] and
A3: for A being Ordinal st A <> {} & A is limit_ordinal & ( for B being Ordinal st B in A holds
P₁[B] ) holds
P₁[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

{} is limit_ordinal

proof end;

theorem Th5: :: ORDINAL2:5

for A being Ordinal holds union A c= A

proof end;

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

canceled;

theorem :: ORDINAL2:7

for A being Ordinal
for L being T-Sequence st dom L = succ A holds
last L = L . A by Th2;

theorem :: ORDINAL2:8

canceled;

theorem :: ORDINAL2:9

for X being set holds On X c= X

proof end;

theorem Th10: :: ORDINAL2:10

for A being Ordinal holds On A = A

proof end;

theorem Th11: :: ORDINAL2:11

for X, Y being set st X c= Y holds
On X c= On Y

proof end;

theorem :: ORDINAL2:12

canceled;

theorem :: ORDINAL2:13

for X being set holds Lim X c= X

proof end;

theorem :: ORDINAL2:14

for X, Y being set st X c= Y holds
Lim X c= Lim Y

proof end;

theorem :: ORDINAL2:15

for X being set holds Lim X c= On X

proof end;

theorem :: ORDINAL2:16

canceled;

theorem Th17: :: ORDINAL2:17

for X being set st ( for x being set st x in X holds
x is Ordinal ) holds
meet X is Ordinal

proof end;

registration

cluster epsilon-transitive epsilon-connected ordinal limit_ordinal set ;
existence
ex b₁ being Ordinal st b₁ is limit_ordinal

proof end;

end;

definition

let X be set ;
canceled;
canceled;
canceled;
canceled;
func inf X -> Ordinal equals :: ORDINAL2:def 6
meet (On X);
coherence
meet (On X) is Ordinal

proof end;

func sup X -> Ordinal means :Def7: :: ORDINAL2:def 7
( On X c= it & ( for A being Ordinal st On X c= A holds
it c= A ) );
existence
ex b₁ being Ordinal st
( On X c= b₁ & ( for A being Ordinal st On X c= A holds
b₁ c= A ) )

proof end;

uniqueness
for b₁, b₂ being Ordinal st On X c= b₁ & ( for A being Ordinal st On X c= A holds
b₁ c= A ) & On X c= b₂ & ( for A being Ordinal st On X c= A holds
b₂ c= A ) holds
b₁ = b₂

proof end;

end;

:: deftheorem ORDINAL2:def 2 :
canceled;

:: deftheorem ORDINAL2:def 3 :
canceled;

:: deftheorem ORDINAL2:def 4 :
canceled;

:: deftheorem ORDINAL2:def 5 :
canceled;

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

:: deftheorem Def7 defines sup ORDINAL2:def 7 :
for X being set
for b₂ being Ordinal holds
( b₂ = sup X iff ( On X c= b₂ & ( for A being Ordinal st On X c= A holds
b₂ c= A ) ) );

theorem :: ORDINAL2:18

canceled;

theorem :: ORDINAL2:19

canceled;

theorem :: ORDINAL2:20

canceled;

theorem :: ORDINAL2:21

canceled;

theorem :: ORDINAL2:22

for A being Ordinal
for X being set st A in X holds
inf X c= A

proof end;

theorem :: ORDINAL2:23

for D being Ordinal
for X being set st On X <> {} & ( for A being Ordinal st A in X holds
D c= A ) holds
D c= inf X

proof end;

theorem :: ORDINAL2:24

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

for A being Ordinal
for X being set st A in X holds
inf X in X

proof end;

theorem Th26: :: ORDINAL2:26

for A being Ordinal holds sup A = A

proof end;

theorem Th27: :: ORDINAL2:27

for A being Ordinal
for X being set st A in X holds
A in sup X

proof end;

theorem Th28: :: ORDINAL2:28

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

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

for X, Y being set st X c= Y holds
sup X c= sup Y

proof end;

theorem :: ORDINAL2:31

for A being Ordinal holds sup {A} = succ A

proof end;

theorem :: ORDINAL2:32

for X being set holds inf X c= sup X

proof end;

scheme :: ORDINAL2:sch 2
TSLambda{ F₁() -> Ordinal, F₂( Ordinal) -> set } :

ex L being T-Sequence st
( dom L = F₁() & ( for A being Ordinal st A in F₁() holds
L . A = F₂(A) ) )

proof end;

definition

let f be Function;
attr f is Ordinal-yielding means :Def8: :: ORDINAL2:def 8
ex A being Ordinal st rng f c= A;

end;

:: deftheorem Def8 defines Ordinal-yielding ORDINAL2:def 8 :
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 set ;
existence
ex b₁ being T-Sequence st b₁ is Ordinal-yielding

proof end;

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 set ;
coherence
for b₁ being T-Sequence of holds b₁ is Ordinal-yielding

proof end;

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

canceled;

theorem Th34: :: ORDINAL2:34

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 Ordinal;
cluster f . a -> ordinal ;
coherence
f . a is ordinal

proof end;

end;

scheme :: ORDINAL2:sch 3
OSLambda{ F₁() -> Ordinal, F₂( Ordinal) -> Ordinal } :

ex fi being Ordinal-Sequence st
( dom fi = F₁() & ( for A being Ordinal st A in F₁() holds
fi . A = F₂(A) ) )

proof end;

scheme :: ORDINAL2:sch 4
TSUniq1{ F₁() -> Ordinal, F₂() -> set , F₃( Ordinal, set ) -> set , F₄( Ordinal, T-Sequence) -> set , F₅() -> T-Sequence, F₆() -> T-Sequence } :

F₅() = F₆()

provided

A1: dom F₅() = F₁() and
A2: ( {} in F₁() implies F₅() . {} = F₂() ) and
A3: for A being Ordinal st succ A in F₁() holds
F₅() . (succ A) = F₃(A,(F₅() . A)) and
A4: for A being Ordinal st A in F₁() & A <> {} & A is limit_ordinal holds
F₅() . A = F₄(A,(F₅() | A)) and
A5: dom F₆() = F₁() and
A6: ( {} in F₁() implies F₆() . {} = F₂() ) and
A7: for A being Ordinal st succ A in F₁() holds
F₆() . (succ A) = F₃(A,(F₆() . A)) and
A8: for A being Ordinal st A in F₁() & A <> {} & A is limit_ordinal holds
F₆() . A = F₄(A,(F₆() | A))

proof end;

scheme :: ORDINAL2:sch 5
TSExist1{ F₁() -> Ordinal, F₂() -> set , F₃( Ordinal, set ) -> set , F₄( Ordinal, T-Sequence) -> set } :

ex L being T-Sequence st
( dom L = F₁() & ( {} in F₁() implies L . {} = F₂() ) & ( for A being Ordinal st succ A in F₁() holds
L . (succ A) = F₃(A,(L . A)) ) & ( for A being Ordinal st A in F₁() & A <> {} & A is limit_ordinal holds
L . A = F₄(A,(L | A)) ) )

proof end;

scheme :: ORDINAL2:sch 6
TSResult{ F₁() -> T-Sequence, F₂( Ordinal) -> set , F₃() -> Ordinal, F₄() -> set , F₅( Ordinal, set ) -> set , F₆( Ordinal, T-Sequence) -> set } :

for A being Ordinal st A in dom F₁() holds
F₁() . A = F₂(A)

provided

A1: for A being Ordinal
for x being set holds
( x = F₂(A) iff ex L being T-Sequence st
( x = last L & dom L = succ A & L . {} = F₄() & ( for C being Ordinal st succ C in succ A holds
L . (succ C) = F₅(C,(L . C)) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
L . C = F₆(C,(L | C)) ) ) ) and
A2: dom F₁() = F₃() and
A3: ( {} in F₃() implies F₁() . {} = F₄() ) and
A4: for A being Ordinal st succ A in F₃() holds
F₁() . (succ A) = F₅(A,(F₁() . A)) and
A5: for A being Ordinal st A in F₃() & A <> {} & A is limit_ordinal holds
F₁() . A = F₆(A,(F₁() | A))

proof end;

scheme :: ORDINAL2:sch 7
TSDef{ F₁() -> Ordinal, F₂() -> set , F₃( Ordinal, set ) -> set , F₄( Ordinal, T-Sequence) -> set } :

( ex x being set ex L being T-Sequence st
( x = last L & dom L = succ F₁() & L . {} = F₂() & ( for C being Ordinal st succ C in succ F₁() holds
L . (succ C) = F₃(C,(L . C)) ) & ( for C being Ordinal st C in succ F₁() & C <> {} & C is limit_ordinal holds
L . C = F₄(C,(L | C)) ) ) & ( for x1, x2 being set st ex L being T-Sequence st
( x1 = last L & dom L = succ F₁() & L . {} = F₂() & ( for C being Ordinal st succ C in succ F₁() holds
L . (succ C) = F₃(C,(L . C)) ) & ( for C being Ordinal st C in succ F₁() & C <> {} & C is limit_ordinal holds
L . C = F₄(C,(L | C)) ) ) & ex L being T-Sequence st
( x2 = last L & dom L = succ F₁() & L . {} = F₂() & ( for C being Ordinal st succ C in succ F₁() holds
L . (succ C) = F₃(C,(L . C)) ) & ( for C being Ordinal st C in succ F₁() & C <> {} & C is limit_ordinal holds
L . C = F₄(C,(L | C)) ) ) holds
x1 = x2 ) )

proof end;

scheme :: ORDINAL2:sch 8
TSResult0{ F₁( Ordinal) -> set , F₂() -> set , F₃( Ordinal, set ) -> set , F₄( Ordinal, T-Sequence) -> set } :

F₁({}) = F₂()

provided

A1: for A being Ordinal
for x being set holds
( x = F₁(A) iff ex L being T-Sequence st
( x = last L & dom L = succ A & L . {} = F₂() & ( for C being Ordinal st succ C in succ A holds
L . (succ C) = F₃(C,(L . C)) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
L . C = F₄(C,(L | C)) ) ) )

proof end;

scheme :: ORDINAL2:sch 9
TSResultS{ F₁() -> set , F₂( Ordinal, set ) -> set , F₃( Ordinal, T-Sequence) -> set , F₄( Ordinal) -> set } :

for A being Ordinal holds F₄((succ A)) = F₂(A,F₄(A))

provided

A1: for A being Ordinal
for x being set holds
( x = F₄(A) iff ex L being T-Sequence st
( x = last L & dom L = succ A & L . {} = F₁() & ( for C being Ordinal st succ C in succ A holds
L . (succ C) = F₂(C,(L . C)) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
L . C = F₃(C,(L | C)) ) ) )

proof end;

scheme :: ORDINAL2:sch 10
TSResultL{ F₁() -> T-Sequence, F₂() -> Ordinal, F₃( Ordinal) -> set , F₄() -> set , F₅( Ordinal, set ) -> set , F₆( Ordinal, T-Sequence) -> set } :

F₃(F₂()) = F₆(F₂(),F₁())

provided

A1: for A being Ordinal
for x being set holds
( x = F₃(A) iff ex L being T-Sequence st
( x = last L & dom L = succ A & L . {} = F₄() & ( for C being Ordinal st succ C in succ A holds
L . (succ C) = F₅(C,(L . C)) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
L . C = F₆(C,(L | C)) ) ) ) and
A2: ( F₂() <> {} & F₂() is limit_ordinal ) and
A3: dom F₁() = F₂() and
A4: for A being Ordinal st A in F₂() holds
F₁() . A = F₃(A)

proof end;

scheme :: ORDINAL2:sch 11
OSExist{ F₁() -> Ordinal, F₂() -> Ordinal, F₃( Ordinal, Ordinal) -> Ordinal, F₄( Ordinal, T-Sequence) -> Ordinal } :

ex fi being Ordinal-Sequence st
( dom fi = F₁() & ( {} in F₁() implies fi . {} = F₂() ) & ( for A being Ordinal st succ A in F₁() holds
fi . (succ A) = F₃(A,(fi . A)) ) & ( for A being Ordinal st A in F₁() & A <> {} & A is limit_ordinal holds
fi . A = F₄(A,(fi | A)) ) )

proof end;

scheme :: ORDINAL2:sch 12
OSResult{ F₁() -> Ordinal-Sequence, F₂( Ordinal) -> Ordinal, F₃() -> Ordinal, F₄() -> Ordinal, F₅( Ordinal, Ordinal) -> Ordinal, F₆( Ordinal, T-Sequence) -> Ordinal } :

for A being Ordinal st A in dom F₁() holds
F₁() . A = F₂(A)

provided

A1: for A, B being Ordinal holds
( B = F₂(A) iff ex fi being Ordinal-Sequence st
( B = last fi & dom fi = succ A & fi . {} = F₄() & ( for C being Ordinal st succ C in succ A holds
fi . (succ C) = F₅(C,(fi . C)) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
fi . C = F₆(C,(fi | C)) ) ) ) and
A2: dom F₁() = F₃() and
A3: ( {} in F₃() implies F₁() . {} = F₄() ) and
A4: for A being Ordinal st succ A in F₃() holds
F₁() . (succ A) = F₅(A,(F₁() . A)) and
A5: for A being Ordinal st A in F₃() & A <> {} & A is limit_ordinal holds
F₁() . A = F₆(A,(F₁() | A))

proof end;

scheme :: ORDINAL2:sch 13
OSDef{ F₁() -> Ordinal, F₂() -> Ordinal, F₃( Ordinal, Ordinal) -> Ordinal, F₄( Ordinal, T-Sequence) -> Ordinal } :

( ex A being Ordinal ex fi being Ordinal-Sequence st
( A = last fi & dom fi = succ F₁() & fi . {} = F₂() & ( for C being Ordinal st succ C in succ F₁() holds
fi . (succ C) = F₃(C,(fi . C)) ) & ( for C being Ordinal st C in succ F₁() & C <> {} & C is limit_ordinal holds
fi . C = F₄(C,(fi | C)) ) ) & ( for A1, A2 being Ordinal st ex fi being Ordinal-Sequence st
( A1 = last fi & dom fi = succ F₁() & fi . {} = F₂() & ( for C being Ordinal st succ C in succ F₁() holds
fi . (succ C) = F₃(C,(fi . C)) ) & ( for C being Ordinal st C in succ F₁() & C <> {} & C is limit_ordinal holds
fi . C = F₄(C,(fi | C)) ) ) & ex fi being Ordinal-Sequence st
( A2 = last fi & dom fi = succ F₁() & fi . {} = F₂() & ( for C being Ordinal st succ C in succ F₁() holds
fi . (succ C) = F₃(C,(fi . C)) ) & ( for C being Ordinal st C in succ F₁() & C <> {} & C is limit_ordinal holds
fi . C = F₄(C,(fi | C)) ) ) holds
A1 = A2 ) )

proof end;

scheme :: ORDINAL2:sch 14
OSResult0{ F₁( Ordinal) -> Ordinal, F₂() -> Ordinal, F₃( Ordinal, Ordinal) -> Ordinal, F₄( Ordinal, T-Sequence) -> Ordinal } :

F₁({}) = F₂()

provided

A1: for A, B being Ordinal holds
( B = F₁(A) iff ex fi being Ordinal-Sequence st
( B = last fi & dom fi = succ A & fi . {} = F₂() & ( for C being Ordinal st succ C in succ A holds
fi . (succ C) = F₃(C,(fi . C)) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
fi . C = F₄(C,(fi | C)) ) ) )

proof end;

scheme :: ORDINAL2:sch 15
OSResultS{ F₁() -> Ordinal, F₂( Ordinal, Ordinal) -> Ordinal, F₃( Ordinal, T-Sequence) -> Ordinal, F₄( Ordinal) -> Ordinal } :

for A being Ordinal holds F₄((succ A)) = F₂(A,F₄(A))

provided

A1: for A, B being Ordinal holds
( B = F₄(A) iff ex fi being Ordinal-Sequence st
( B = last fi & dom fi = succ A & fi . {} = F₁() & ( for C being Ordinal st succ C in succ A holds
fi . (succ C) = F₂(C,(fi . C)) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
fi . C = F₃(C,(fi | C)) ) ) )

proof end;

scheme :: ORDINAL2:sch 16
OSResultL{ F₁() -> Ordinal-Sequence, F₂() -> Ordinal, F₃( Ordinal) -> Ordinal, F₄() -> Ordinal, F₅( Ordinal, Ordinal) -> Ordinal, F₆( Ordinal, T-Sequence) -> Ordinal } :

F₃(F₂()) = F₆(F₂(),F₁())

provided

A1: for A, B being Ordinal holds
( B = F₃(A) iff ex fi being Ordinal-Sequence st
( B = last fi & dom fi = succ A & fi . {} = F₄() & ( for C being Ordinal st succ C in succ A holds
fi . (succ C) = F₅(C,(fi . C)) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
fi . C = F₆(C,(fi | C)) ) ) ) and
A2: ( F₂() <> {} & F₂() is limit_ordinal ) and
A3: dom F₁() = F₂() and
A4: for A being Ordinal st A in F₂() holds
F₁() . A = F₃(A)

proof end;

definition

let L be T-Sequence;
func sup L -> Ordinal equals :: ORDINAL2:def 9
sup (rng L);
correctness
coherence
sup (rng L) is Ordinal;
;
func inf L -> Ordinal equals :: ORDINAL2:def 10
inf (rng L);
correctness
coherence
inf (rng L) is Ordinal;
;

end;

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

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

theorem :: ORDINAL2:35

for L being T-Sequence holds
( sup L = sup (rng L) & inf L = inf (rng L) ) ;

definition

let L be T-Sequence;
func lim_sup L -> Ordinal means :: ORDINAL2:def 11
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 b₁ being Ordinal ex fi being Ordinal-Sequence st
( b₁ = 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 b₁, b₂ being Ordinal st ex fi being Ordinal-Sequence st
( b₁ = 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
( b₂ = 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
b₁ = b₂

proof end;

func lim_inf L -> Ordinal means :: ORDINAL2:def 12
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 b₁ being Ordinal ex fi being Ordinal-Sequence st
( b₁ = 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 b₁, b₂ being Ordinal st ex fi being Ordinal-Sequence st
( b₁ = 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
( b₂ = 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
b₁ = b₂

proof end;

end;

:: deftheorem defines lim_sup ORDINAL2:def 11 :
for L being T-Sequence
for b₂ being Ordinal holds
( b₂ = lim_sup L iff ex fi being Ordinal-Sequence st
( b₂ = 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 12 :
for L being T-Sequence
for b₂ being Ordinal holds
( b₂ = lim_inf L iff ex fi being Ordinal-Sequence st
( b₂ = 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 :Def13: :: ORDINAL2:def 13
ex B being Ordinal st
( B in dom fi & ( for C being Ordinal st B c= C & C in dom fi holds
fi . C = {} ) ) if A = {}
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 Def13 defines is_limes_of ORDINAL2:def 13 :
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 & ( for C being Ordinal st B c= C & C in dom fi holds
fi . C = {} ) ) ) ) & ( not A = {} 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 :Def14: :: ORDINAL2:def 14
it is_limes_of fi;
existence
ex b₁ being Ordinal st b₁ is_limes_of fi by A1;
uniqueness
for b₁, b₂ being Ordinal st b₁ is_limes_of fi & b₂ is_limes_of fi holds
b₁ = b₂

proof end;

end;

:: deftheorem Def14 defines lim ORDINAL2:def 14 :
for fi being Ordinal-Sequence st ex A being Ordinal st A is_limes_of fi holds
for b₂ being Ordinal holds
( b₂ = lim fi iff b₂ is_limes_of fi );

definition

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

end;

:: deftheorem defines lim ORDINAL2:def 15 :
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 16
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 17
for A, B being Ordinal st A in dom L & A <> {} & A is limit_ordinal & B = L . A holds
B is_limes_of L | A;

end;

:: deftheorem defines increasing ORDINAL2:def 16 :
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 17 :
for L being Ordinal-Sequence holds
( L is continuous iff for A, B being Ordinal st A in dom L & A <> {} & 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 :Def18: :: ORDINAL2:def 18
ex fi being Ordinal-Sequence st
( it = last fi & dom fi = succ B & fi . {} = 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 <> {} & C is limit_ordinal holds
fi . C = sup (fi | C) ) );
correctness
existence
ex b₁ being Ordinal ex fi being Ordinal-Sequence st
( b₁ = last fi & dom fi = succ B & fi . {} = 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 <> {} & C is limit_ordinal holds
fi . C = sup (fi | C) ) );
uniqueness
for b₁, b₂ being Ordinal st ex fi being Ordinal-Sequence st
( b₁ = last fi & dom fi = succ B & fi . {} = 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 <> {} & C is limit_ordinal holds
fi . C = sup (fi | C) ) ) & ex fi being Ordinal-Sequence st
( b₂ = last fi & dom fi = succ B & fi . {} = 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 <> {} & C is limit_ordinal holds
fi . C = sup (fi | C) ) ) holds
b₁ = b₂;

proof end;

end;

:: deftheorem Def18 defines +^ ORDINAL2:def 18 :
for A, B, b₃ being Ordinal holds
( b₃ = A +^ B iff ex fi being Ordinal-Sequence st
( b₃ = last fi & dom fi = succ B & fi . {} = 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 <> {} & C is limit_ordinal holds
fi . C = sup (fi | C) ) ) );

definition

let A, B be Ordinal;
func A *^ B -> Ordinal means :Def19: :: ORDINAL2:def 19
ex fi being Ordinal-Sequence st
( it = last fi & dom fi = succ A & fi . {} = {} & ( 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 <> {} & C is limit_ordinal holds
fi . C = union (sup (fi | C)) ) );
correctness
existence
ex b₁ being Ordinal ex fi being Ordinal-Sequence st
( b₁ = last fi & dom fi = succ A & fi . {} = {} & ( 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 <> {} & C is limit_ordinal holds
fi . C = union (sup (fi | C)) ) );
uniqueness
for b₁, b₂ being Ordinal st ex fi being Ordinal-Sequence st
( b₁ = last fi & dom fi = succ A & fi . {} = {} & ( 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 <> {} & C is limit_ordinal holds
fi . C = union (sup (fi | C)) ) ) & ex fi being Ordinal-Sequence st
( b₂ = last fi & dom fi = succ A & fi . {} = {} & ( 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 <> {} & C is limit_ordinal holds
fi . C = union (sup (fi | C)) ) ) holds
b₁ = b₂;

proof end;

end;

:: deftheorem Def19 defines *^ ORDINAL2:def 19 :
for A, B, b₃ being Ordinal holds
( b₃ = A *^ B iff ex fi being Ordinal-Sequence st
( b₃ = last fi & dom fi = succ A & fi . {} = {} & ( 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 <> {} & C is limit_ordinal holds
fi . C = union (sup (fi | C)) ) ) );

registration

let O be Ordinal;
cluster -> ordinal Element of O;
coherence
for b₁ being Element of O holds b₁ is ordinal ;

end;

definition

let A, B be Ordinal;
func exp (A,B) -> Ordinal means :Def20: :: ORDINAL2:def 20
ex fi being Ordinal-Sequence st
( it = last fi & dom fi = succ B & fi . {} = 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 <> {} & C is limit_ordinal holds
fi . C = lim (fi | C) ) );
correctness
existence
ex b₁ being Ordinal ex fi being Ordinal-Sequence st
( b₁ = last fi & dom fi = succ B & fi . {} = 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 <> {} & C is limit_ordinal holds
fi . C = lim (fi | C) ) );
uniqueness
for b₁, b₂ being Ordinal st ex fi being Ordinal-Sequence st
( b₁ = last fi & dom fi = succ B & fi . {} = 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 <> {} & C is limit_ordinal holds
fi . C = lim (fi | C) ) ) & ex fi being Ordinal-Sequence st
( b₂ = last fi & dom fi = succ B & fi . {} = 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 <> {} & C is limit_ordinal holds
fi . C = lim (fi | C) ) ) holds
b₁ = b₂;

proof end;

end;

:: deftheorem Def20 defines exp ORDINAL2:def 20 :
for A, B, b₃ being Ordinal holds
( b₃ = exp (A,B) iff ex fi being Ordinal-Sequence st
( b₃ = last fi & dom fi = succ B & fi . {} = 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 <> {} & C is limit_ordinal holds
fi . C = lim (fi | C) ) ) );

theorem :: ORDINAL2:36

canceled;

theorem :: ORDINAL2:37

canceled;

theorem :: ORDINAL2:38

canceled;

theorem :: ORDINAL2:39

canceled;

theorem :: ORDINAL2:40

canceled;

theorem :: ORDINAL2:41

canceled;

theorem :: ORDINAL2:42

canceled;

theorem :: ORDINAL2:43

canceled;

theorem Th44: :: ORDINAL2:44

for A being Ordinal holds A +^ {} = A

proof end;

theorem Th45: :: ORDINAL2:45

for A, B being Ordinal holds A +^ (succ B) = succ (A +^ B)

proof end;

theorem Th46: :: ORDINAL2:46

for B, A being Ordinal st B <> {} & 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 Th47: :: ORDINAL2:47

for A being Ordinal holds {} +^ A = A

proof end;

Lm1: 1 = succ {}
;

theorem :: ORDINAL2:48

for A being Ordinal holds A +^ 1 = succ A

proof end;

theorem Th49: :: ORDINAL2:49

for A, B, C being Ordinal st A in B holds
C +^ A in C +^ B

proof end;

theorem Th50: :: ORDINAL2:50

for A, B, C being Ordinal st A c= B holds
C +^ A c= C +^ B

proof end;

theorem Th51: :: ORDINAL2:51

for A, B, C being Ordinal st A c= B holds
A +^ C c= B +^ C

proof end;

theorem Th52: :: ORDINAL2:52

for A being Ordinal holds {} *^ A = {}

proof end;

theorem Th53: :: ORDINAL2:53

for B, A being Ordinal holds (succ B) *^ A = (B *^ A) +^ A

proof end;

theorem Th54: :: ORDINAL2:54

for B, A being Ordinal st B <> {} & 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 Th55: :: ORDINAL2:55

for A being Ordinal holds A *^ {} = {}

proof end;

theorem Th56: :: ORDINAL2:56

for A being Ordinal holds
( 1 *^ A = A & A *^ 1 = A )

proof end;

theorem Th57: :: ORDINAL2:57

for C, A, B being Ordinal st C <> {} & A in B holds
A *^ C in B *^ C

proof end;

theorem :: ORDINAL2:58

for A, B, C being Ordinal st A c= B holds
A *^ C c= B *^ C

proof end;

theorem :: ORDINAL2:59

for A, B, C being Ordinal st A c= B holds
C *^ A c= C *^ B

proof end;

theorem Th60: :: ORDINAL2:60

for A being Ordinal holds exp (A,{}) = 1

proof end;

theorem Th61: :: ORDINAL2:61

for A, B being Ordinal holds exp (A,(succ B)) = A *^ (exp (A,B))

proof end;

theorem Th62: :: ORDINAL2:62

for B, A being Ordinal st B <> {} & 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:63

for A being Ordinal holds
( exp (A,1) = A & exp (1,A) = 1 )

proof end;

theorem :: ORDINAL2:64

canceled;

theorem :: ORDINAL2:65

for A being Ordinal ex B, C being Ordinal st
( B is limit_ordinal & C is natural & A = B +^ C )

proof end;

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 set ;
cluster O --> x -> T-Sequence-like ;
coherence
O --> x is T-Sequence-like

proof end;

end;

definition

let A, B be Ordinal;
pred A is_cofinal_with B means :: ORDINAL2:def 21
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 21 :
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 Th66: :: ORDINAL2:66

for psi being Ordinal-Sequence
for e being set st e in rng psi holds
e is Ordinal

proof end;

theorem :: ORDINAL2:67

for psi being Ordinal-Sequence holds rng psi c= sup psi

proof end;

theorem :: ORDINAL2:68

for A being Ordinal st A is_cofinal_with {} holds
A = {}

proof end;

scheme :: ORDINAL2:sch 17
OmegaInd{ F₁() -> natural number , P₁[ set ] } :

P₁[F₁()]

provided

A1: P₁[ {} ] and
A2: for a being natural number st P₁[a] holds
P₁[ succ a]

proof end;

registration

let a, b be natural number ;
cluster a +^ b -> natural ;
coherence
a +^ b is natural

proof end;

end;

registration

let x, y be set ;
let a, b be natural number ;
cluster IFEQ (x,y,a,b) -> natural ;
coherence
IFEQ (x,y,a,b) is natural

proof end;

end;

scheme :: ORDINAL2:sch 18
LambdaRecEx{ F₁() -> set , F₂( set , set ) -> set } :

ex f being Function st
( dom f = omega & f . {} = F₁() & ( for n being natural number holds f . (succ n) = F₂(n,(f . n)) ) )

proof end;

scheme :: ORDINAL2:sch 19
RecUn{ F₁() -> set , F₂() -> Function, F₃() -> Function, P₁[ set , set , set ] } :

F₂() = F₃()

provided

A1: dom F₂() = omega and
A2: F₂() . {} = F₁() and
A3: for n being natural number holds P₁[n,F₂() . n,F₂() . (succ n)] and
A4: dom F₃() = omega and
A5: F₃() . {} = F₁() and
A6: for n being natural number holds P₁[n,F₃() . n,F₃() . (succ n)] and
A7: for n being natural number
for x, y1, y2 being set st P₁[n,x,y1] & P₁[n,x,y2] holds
y1 = y2

proof end;

scheme :: ORDINAL2:sch 20
LambdaRecUn{ F₁() -> set , F₂( set , set ) -> set , F₃() -> Function, F₄() -> Function } :

F₃() = F₄()

provided

A1: dom F₃() = omega and
A2: F₃() . {} = F₁() and
A3: for n being natural number holds F₃() . (succ n) = F₂(n,(F₃() . n)) and
A4: dom F₄() = omega and
A5: F₄() . {} = F₁() and
A6: for n being natural number holds F₄() . (succ n) = F₂(n,(F₄() . n))

proof end;