:: ORDINAL2 semantic presentation

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

for b₁ being Ordinal holds P₁[b₁]

provided

E1: P₁[ {} ] and
E2: for b₁ being Ordinal st P₁[b₁] holds
P₁[ succ b₁] and
E3: for b₁ being Ordinal st b₁ <> {} & b₁ is_limit_ordinal & ( for b₂ being Ordinal st b₂ in b₁ holds
P₁[b₂] ) holds
P₁[b₁]

proof end;

theorem Th1: :: ORDINAL2:1

for b₁, b₂ being Ordinal holds
( b₁ c= b₂ iff succ b₁ c= succ b₂ )

proof end;

theorem Th2: :: ORDINAL2:2

for b₁ being Ordinal holds union (succ b₁) = b₁

proof end;

theorem Th3: :: ORDINAL2:3

for b₁ being Ordinal holds succ b₁ c= bool b₁

proof end;

theorem Th4: :: ORDINAL2:4

{} is_limit_ordinal

proof end;

theorem Th5: :: ORDINAL2:5

for b₁ being Ordinal holds union b₁ c= b₁

proof end;

definition

let c₁ be T-Sequence;
func last c₁ -> set equals :: ORDINAL2:def 1
a₁ . (union (dom a₁));
coherence ;

end;

:: deftheorem Def1 defines last ORDINAL2:def 1 :

theorem Th6: :: ORDINAL2:6

canceled;

theorem Th7: :: ORDINAL2:7

for b₁ being Ordinal
for b₂ being T-Sequence st dom b₂ = succ b₁ holds
last b₂ = b₂ . b₁ by Th2;

definition

let c₁ be set ;
func On c₁ -> set means :Def2: :: ORDINAL2:def 2
for b₁ being set holds
( b₁ in a₂ iff ( b₁ in a₁ & b₁ is Ordinal ) );
existence

proof end;

uniqueness

proof end;

func Lim c₁ -> set means :Def3: :: ORDINAL2:def 3
for b₁ being set holds
( b₁ in a₂ iff ( b₁ in a₁ & ex b₂ being Ordinal st
( b₁ = b₂ & b₂ is_limit_ordinal ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines On ORDINAL2:def 2 :

:: deftheorem Def3 defines Lim ORDINAL2:def 3 :

theorem Th8: :: ORDINAL2:8

canceled;

theorem Th9: :: ORDINAL2:9

for b₁ being set holds On b₁ c= b₁

proof end;

theorem Th10: :: ORDINAL2:10

for b₁ being Ordinal holds On b₁ = b₁

proof end;

theorem Th11: :: ORDINAL2:11

for b₁, b₂ being set st b₁ c= b₂ holds
On b₁ c= On b₂

proof end;

theorem Th12: :: ORDINAL2:12

canceled;

theorem Th13: :: ORDINAL2:13

for b₁ being set holds Lim b₁ c= b₁

proof end;

theorem Th14: :: ORDINAL2:14

for b₁, b₂ being set st b₁ c= b₂ holds
Lim b₁ c= Lim b₂

proof end;

theorem Th15: :: ORDINAL2:15

for b₁ being set holds Lim b₁ c= On b₁

proof end;

theorem Th16: :: ORDINAL2:16

for b₁ being Ordinal ex b₂ being Ordinal st
( b₁ in b₂ & b₂ is_limit_ordinal )

proof end;

theorem Th17: :: ORDINAL2:17

for b₁ being set st ( for b₂ being set st b₂ in b₁ holds
b₂ is Ordinal ) holds
meet b₁ is Ordinal

proof end;

definition

func one -> non empty Ordinal equals :: ORDINAL2:def 4
succ {} ;
correctness ;

end;

:: deftheorem Def4 defines one ORDINAL2:def 4 :

definition

func omega -> set means :Def5: :: ORDINAL2:def 5
( {} in a₁ & a₁ is_limit_ordinal & a₁ is ordinal & ( for b₁ being Ordinal st {} in b₁ & b₁ is_limit_ordinal holds
a₁ c= b₁ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines omega ORDINAL2:def 5 :

registration

cluster omega -> ordinal non empty ;
coherence by Def5;

end;

registration

cluster being_limit_ordinal set ;
existence

proof end;

end;

definition

let c₁ be set ;
func inf c₁ -> Ordinal equals :: ORDINAL2:def 6
meet (On a₁);
coherence

proof end;

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines inf ORDINAL2:def 6 :

:: deftheorem Def7 defines sup ORDINAL2:def 7 :

theorem Th18: :: ORDINAL2:18

canceled;

theorem Th19: :: ORDINAL2:19

( {} in omega & omega is_limit_ordinal & ( for b₁ being Ordinal st {} in b₁ & b₁ is_limit_ordinal holds
omega c= b₁ ) ) by Def5;

theorem Th20: :: ORDINAL2:20

canceled;

theorem Th21: :: ORDINAL2:21

canceled;

theorem Th22: :: ORDINAL2:22

for b₁ being Ordinal
for b₂ being set st b₁ in b₂ holds
inf b₂ c= b₁

proof end;

theorem Th23: :: ORDINAL2:23

for b₁ being Ordinal
for b₂ being set st On b₂ <> {} & ( for b₃ being Ordinal st b₃ in b₂ holds
b₁ c= b₃ ) holds
b₁ c= inf b₂

proof end;

theorem Th24: :: ORDINAL2:24

for b₁ being Ordinal
for b₂, b₃ being set st b₁ in b₂ & b₂ c= b₃ holds
inf b₃ c= inf b₂

proof end;

theorem Th25: :: ORDINAL2:25

for b₁ being Ordinal
for b₂ being set st b₁ in b₂ holds
inf b₂ in b₂

proof end;

theorem Th26: :: ORDINAL2:26

for b₁ being Ordinal holds sup b₁ = b₁

proof end;

theorem Th27: :: ORDINAL2:27

for b₁ being Ordinal
for b₂ being set st b₁ in b₂ holds
b₁ in sup b₂

proof end;

theorem Th28: :: ORDINAL2:28

for b₁ being Ordinal
for b₂ being set st ( for b₃ being Ordinal st b₃ in b₂ holds
b₃ in b₁ ) holds
sup b₂ c= b₁

proof end;

theorem Th29: :: ORDINAL2:29

for b₁ being Ordinal
for b₂ being set st b₁ in sup b₂ holds
ex b₃ being Ordinal st
( b₃ in b₂ & b₁ c= b₃ )

proof end;

theorem Th30: :: ORDINAL2:30

for b₁, b₂ being set st b₁ c= b₂ holds
sup b₁ c= sup b₂

proof end;

theorem Th31: :: ORDINAL2:31

for b₁ being Ordinal holds sup {b₁} = succ b₁

proof end;

theorem Th32: :: ORDINAL2:32

for b₁ being set holds inf b₁ c= sup b₁

proof end;

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

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

proof end;

definition

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

end;

:: deftheorem Def8 defines Ordinal-yielding ORDINAL2:def 8 :

registration

cluster Ordinal-yielding set ;
existence

proof end;

end;

definition

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

end;

registration

let c₁ be Ordinal;
cluster -> Ordinal-yielding T-Sequence of a₁;
coherence

proof end;

end;

registration

let c₁ be Ordinal-Sequence;
let c₂ be Ordinal;
cluster a₁ | a₂ -> Ordinal-yielding ;
coherence

proof end;

end;

theorem Th33: :: ORDINAL2:33

canceled;

theorem Th34: :: ORDINAL2:34

for b₁ being Ordinal
for b₂ being Ordinal-Sequence st b₁ in dom b₂ holds
b₂ . b₁ is Ordinal

proof end;

registration

let c₁ be Ordinal-Sequence;
let c₂ be Ordinal;
cluster a₁ . a₂ -> ordinal ;
coherence

proof end;

end;

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

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

proof end;

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

F₅() = F₆()

provided

E18: dom F₅() = F₁() and
E19: ( {} in F₁() implies F₅() . {} = F₂() ) and
E20: for b₁ being Ordinal st succ b₁ in F₁() holds
F₅() . (succ b₁) = F₃(b₁,(F₅() . b₁)) and
E21: for b₁ being Ordinal st b₁ in F₁() & b₁ <> {} & b₁ is_limit_ordinal holds
F₅() . b₁ = F₄(b₁,(F₅() | b₁)) and
E22: dom F₆() = F₁() and
E23: ( {} in F₁() implies F₆() . {} = F₂() ) and
E24: for b₁ being Ordinal st succ b₁ in F₁() holds
F₆() . (succ b₁) = F₃(b₁,(F₆() . b₁)) and
E25: for b₁ being Ordinal st b₁ in F₁() & b₁ <> {} & b₁ is_limit_ordinal holds
F₆() . b₁ = F₄(b₁,(F₆() | b₁))

proof end;

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

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

proof end;

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

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

provided

E18: for b₁ being Ordinal
for b₂ being set holds
( b₂ = F₂(b₁) iff ex b₃ being T-Sequence st
( b₂ = last b₃ & dom b₃ = succ b₁ & b₃ . {} = F₄() & ( for b₄ being Ordinal st succ b₄ in succ b₁ holds
b₃ . (succ b₄) = F₅(b₄,(b₃ . b₄)) ) & ( for b₄ being Ordinal st b₄ in succ b₁ & b₄ <> {} & b₄ is_limit_ordinal holds
b₃ . b₄ = F₆(b₄,(b₃ | b₄)) ) ) ) and
E19: dom F₁() = F₃() and
E20: ( {} in F₃() implies F₁() . {} = F₄() ) and
E21: for b₁ being Ordinal st succ b₁ in F₃() holds
F₁() . (succ b₁) = F₅(b₁,(F₁() . b₁)) and
E22: for b₁ being Ordinal st b₁ in F₃() & b₁ <> {} & b₁ is_limit_ordinal holds
F₁() . b₁ = F₆(b₁,(F₁() | b₁))

proof end;

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

( ex b₁ being set ex b₂ being T-Sequence st
( b₁ = last b₂ & dom b₂ = succ F₁() & b₂ . {} = F₂() & ( for b₃ being Ordinal st succ b₃ in succ F₁() holds
b₂ . (succ b₃) = F₃(b₃,(b₂ . b₃)) ) & ( for b₃ being Ordinal st b₃ in succ F₁() & b₃ <> {} & b₃ is_limit_ordinal holds
b₂ . b₃ = F₄(b₃,(b₂ | b₃)) ) ) & ( for b₁, b₂ being set st ex b₃ being T-Sequence st
( b₁ = last b₃ & dom b₃ = succ F₁() & b₃ . {} = F₂() & ( for b₄ being Ordinal st succ b₄ in succ F₁() holds
b₃ . (succ b₄) = F₃(b₄,(b₃ . b₄)) ) & ( for b₄ being Ordinal st b₄ in succ F₁() & b₄ <> {} & b₄ is_limit_ordinal holds
b₃ . b₄ = F₄(b₄,(b₃ | b₄)) ) ) & ex b₃ being T-Sequence st
( b₂ = last b₃ & dom b₃ = succ F₁() & b₃ . {} = F₂() & ( for b₄ being Ordinal st succ b₄ in succ F₁() holds
b₃ . (succ b₄) = F₃(b₄,(b₃ . b₄)) ) & ( for b₄ being Ordinal st b₄ in succ F₁() & b₄ <> {} & b₄ is_limit_ordinal holds
b₃ . b₄ = F₄(b₄,(b₃ | b₄)) ) ) holds
b₁ = b₂ ) )

proof end;

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

F₁({} ) = F₂()

provided

E18: for b₁ being Ordinal
for b₂ being set holds
( b₂ = F₁(b₁) iff ex b₃ being T-Sequence st
( b₂ = last b₃ & dom b₃ = succ b₁ & b₃ . {} = F₂() & ( for b₄ being Ordinal st succ b₄ in succ b₁ holds
b₃ . (succ b₄) = F₃(b₄,(b₃ . b₄)) ) & ( for b₄ being Ordinal st b₄ in succ b₁ & b₄ <> {} & b₄ is_limit_ordinal holds
b₃ . b₄ = F₄(b₄,(b₃ | b₄)) ) ) )

proof end;

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

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

provided

E18: for b₁ being Ordinal
for b₂ being set holds
( b₂ = F₄(b₁) iff ex b₃ being T-Sequence st
( b₂ = last b₃ & dom b₃ = succ b₁ & b₃ . {} = F₁() & ( for b₄ being Ordinal st succ b₄ in succ b₁ holds
b₃ . (succ b₄) = F₂(b₄,(b₃ . b₄)) ) & ( for b₄ being Ordinal st b₄ in succ b₁ & b₄ <> {} & b₄ is_limit_ordinal holds
b₃ . b₄ = F₃(b₄,(b₃ | b₄)) ) ) )

proof end;

scheme :: ORDINAL2:sch 10
s10{ 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

E18: for b₁ being Ordinal
for b₂ being set holds
( b₂ = F₃(b₁) iff ex b₃ being T-Sequence st
( b₂ = last b₃ & dom b₃ = succ b₁ & b₃ . {} = F₄() & ( for b₄ being Ordinal st succ b₄ in succ b₁ holds
b₃ . (succ b₄) = F₅(b₄,(b₃ . b₄)) ) & ( for b₄ being Ordinal st b₄ in succ b₁ & b₄ <> {} & b₄ is_limit_ordinal holds
b₃ . b₄ = F₆(b₄,(b₃ | b₄)) ) ) ) and
E19: ( F₂() <> {} & F₂() is_limit_ordinal ) and
E20: dom F₁() = F₂() and
E21: for b₁ being Ordinal st b₁ in F₂() holds
F₁() . b₁ = F₃(b₁)

proof end;

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

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

proof end;

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

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

provided

E18: for b₁, b₂ being Ordinal holds
( b₂ = F₂(b₁) iff ex b₃ being Ordinal-Sequence st
( b₂ = last b₃ & dom b₃ = succ b₁ & b₃ . {} = F₄() & ( for b₄ being Ordinal st succ b₄ in succ b₁ holds
b₃ . (succ b₄) = F₅(b₄,(b₃ . b₄)) ) & ( for b₄ being Ordinal st b₄ in succ b₁ & b₄ <> {} & b₄ is_limit_ordinal holds
b₃ . b₄ = F₆(b₄,(b₃ | b₄)) ) ) ) and
E19: dom F₁() = F₃() and
E20: ( {} in F₃() implies F₁() . {} = F₄() ) and
E21: for b₁ being Ordinal st succ b₁ in F₃() holds
F₁() . (succ b₁) = F₅(b₁,(F₁() . b₁)) and
E22: for b₁ being Ordinal st b₁ in F₃() & b₁ <> {} & b₁ is_limit_ordinal holds
F₁() . b₁ = F₆(b₁,(F₁() | b₁))

proof end;

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

( ex b₁ being Ordinalex b₂ being Ordinal-Sequence st
( b₁ = last b₂ & dom b₂ = succ F₁() & b₂ . {} = F₂() & ( for b₃ being Ordinal st succ b₃ in succ F₁() holds
b₂ . (succ b₃) = F₃(b₃,(b₂ . b₃)) ) & ( for b₃ being Ordinal st b₃ in succ F₁() & b₃ <> {} & b₃ is_limit_ordinal holds
b₂ . b₃ = F₄(b₃,(b₂ | b₃)) ) ) & ( for b₁, b₂ being Ordinal st ex b₃ being Ordinal-Sequence st
( b₁ = last b₃ & dom b₃ = succ F₁() & b₃ . {} = F₂() & ( for b₄ being Ordinal st succ b₄ in succ F₁() holds
b₃ . (succ b₄) = F₃(b₄,(b₃ . b₄)) ) & ( for b₄ being Ordinal st b₄ in succ F₁() & b₄ <> {} & b₄ is_limit_ordinal holds
b₃ . b₄ = F₄(b₄,(b₃ | b₄)) ) ) & ex b₃ being Ordinal-Sequence st
( b₂ = last b₃ & dom b₃ = succ F₁() & b₃ . {} = F₂() & ( for b₄ being Ordinal st succ b₄ in succ F₁() holds
b₃ . (succ b₄) = F₃(b₄,(b₃ . b₄)) ) & ( for b₄ being Ordinal st b₄ in succ F₁() & b₄ <> {} & b₄ is_limit_ordinal holds
b₃ . b₄ = F₄(b₄,(b₃ | b₄)) ) ) holds
b₁ = b₂ ) )

proof end;

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

F₁({} ) = F₂()

provided

E18: for b₁, b₂ being Ordinal holds
( b₂ = F₁(b₁) iff ex b₃ being Ordinal-Sequence st
( b₂ = last b₃ & dom b₃ = succ b₁ & b₃ . {} = F₂() & ( for b₄ being Ordinal st succ b₄ in succ b₁ holds
b₃ . (succ b₄) = F₃(b₄,(b₃ . b₄)) ) & ( for b₄ being Ordinal st b₄ in succ b₁ & b₄ <> {} & b₄ is_limit_ordinal holds
b₃ . b₄ = F₄(b₄,(b₃ | b₄)) ) ) )

proof end;

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

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

provided

E18: for b₁, b₂ being Ordinal holds
( b₂ = F₄(b₁) iff ex b₃ being Ordinal-Sequence st
( b₂ = last b₃ & dom b₃ = succ b₁ & b₃ . {} = F₁() & ( for b₄ being Ordinal st succ b₄ in succ b₁ holds
b₃ . (succ b₄) = F₂(b₄,(b₃ . b₄)) ) & ( for b₄ being Ordinal st b₄ in succ b₁ & b₄ <> {} & b₄ is_limit_ordinal holds
b₃ . b₄ = F₃(b₄,(b₃ | b₄)) ) ) )

proof end;

scheme :: ORDINAL2:sch 16
s16{ 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

E18: for b₁, b₂ being Ordinal holds
( b₂ = F₃(b₁) iff ex b₃ being Ordinal-Sequence st
( b₂ = last b₃ & dom b₃ = succ b₁ & b₃ . {} = F₄() & ( for b₄ being Ordinal st succ b₄ in succ b₁ holds
b₃ . (succ b₄) = F₅(b₄,(b₃ . b₄)) ) & ( for b₄ being Ordinal st b₄ in succ b₁ & b₄ <> {} & b₄ is_limit_ordinal holds
b₃ . b₄ = F₆(b₄,(b₃ | b₄)) ) ) ) and
E19: ( F₂() <> {} & F₂() is_limit_ordinal ) and
E20: dom F₁() = F₂() and
E21: for b₁ being Ordinal st b₁ in F₂() holds
F₁() . b₁ = F₃(b₁)

proof end;

definition

let c₁ be T-Sequence;
func sup c₁ -> Ordinal equals :: ORDINAL2:def 9
sup (rng a₁);
correctness ;
func inf c₁ -> Ordinal equals :: ORDINAL2:def 10
inf (rng a₁);
correctness ;

end;

:: deftheorem Def9 defines sup ORDINAL2:def 9 :

:: deftheorem Def10 defines inf ORDINAL2:def 10 :

theorem Th35: :: ORDINAL2:35

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

definition

let c₁ be T-Sequence;
func lim_sup c₁ -> Ordinal means :: ORDINAL2:def 11
ex b₁ being Ordinal-Sequence st
( a₂ = inf b₁ & dom b₁ = dom a₁ & ( for b₂ being Ordinal st b₂ in dom a₁ holds
b₁ . b₂ = sup (rng (a₁ | ((dom a₁) \ b₂))) ) );
existence

proof end;

uniqueness

proof end;

func lim_inf c₁ -> Ordinal means :: ORDINAL2:def 12
ex b₁ being Ordinal-Sequence st
( a₂ = sup b₁ & dom b₁ = dom a₁ & ( for b₂ being Ordinal st b₂ in dom a₁ holds
b₁ . b₂ = inf (rng (a₁ | ((dom a₁) \ b₂))) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def11 defines lim_sup ORDINAL2:def 11 :

:: deftheorem Def12 defines lim_inf ORDINAL2:def 12 :

definition

let c₁ be Ordinal;
let c₂ be Ordinal-Sequence;
pred c₁ is_limes_of c₂ means :Def13: :: ORDINAL2:def 13
ex b₁ being Ordinal st
( b₁ in dom a₂ & ( for b₂ being Ordinal st b₁ c= b₂ & b₂ in dom a₂ holds
a₂ . b₂ = {} ) ) if a₁ = {}
otherwise for b₁, b₂ being Ordinal st b₁ in a₁ & a₁ in b₂ holds
ex b₃ being Ordinal st
( b₃ in dom a₂ & ( for b₄ being Ordinal st b₃ c= b₄ & b₄ in dom a₂ holds
( b₁ in a₂ . b₄ & a₂ . b₄ in b₂ ) ) );
consistency ;

end;

:: deftheorem Def13 defines is_limes_of ORDINAL2:def 13 :

definition

let c₁ be Ordinal-Sequence;
given c₂ being Ordinal such that E19: c₂ is_limes_of c₁ ;
func lim c₁ -> Ordinal means :Def14: :: ORDINAL2:def 14
a₂ is_limes_of a₁;
existence by E19;
uniqueness

proof end;

end;

:: deftheorem Def14 defines lim ORDINAL2:def 14 :

definition

let c₁ be Ordinal;
let c₂ be Ordinal-Sequence;
func lim c₁,c₂ -> Ordinal equals :: ORDINAL2:def 15
lim (a₂ | a₁);
correctness ;

end;

:: deftheorem Def15 defines lim ORDINAL2:def 15 :

definition

let c₁ be Ordinal-Sequence;
attr a₁ is increasing means :: ORDINAL2:def 16
for b₁, b₂ being Ordinal st b₁ in b₂ & b₂ in dom a₁ holds
a₁ . b₁ in a₁ . b₂;
attr a₁ is continuous means :: ORDINAL2:def 17
for b₁, b₂ being Ordinal st b₁ in dom a₁ & b₁ <> {} & b₁ is_limit_ordinal & b₂ = a₁ . b₁ holds
b₂ is_limes_of a₁ | b₁;

end;

:: deftheorem Def16 defines increasing ORDINAL2:def 16 :

:: deftheorem Def17 defines continuous ORDINAL2:def 17 :

definition

let c₁, c₂ be Ordinal;
func c₁ +^ c₂ -> Ordinal means :Def18: :: ORDINAL2:def 18
ex b₁ being Ordinal-Sequence st
( a₃ = last b₁ & dom b₁ = succ a₂ & b₁ . {} = a₁ & ( for b₂ being Ordinal st succ b₂ in succ a₂ holds
b₁ . (succ b₂) = succ (b₁ . b₂) ) & ( for b₂ being Ordinal st b₂ in succ a₂ & b₂ <> {} & b₂ is_limit_ordinal holds
b₁ . b₂ = sup (b₁ | b₂) ) );
correctness

proof end;

end;

:: deftheorem Def18 defines +^ ORDINAL2:def 18 :

definition

let c₁, c₂ be Ordinal;
func c₁ *^ c₂ -> Ordinal means :Def19: :: ORDINAL2:def 19
ex b₁ being Ordinal-Sequence st
( a₃ = last b₁ & dom b₁ = succ a₁ & b₁ . {} = {} & ( for b₂ being Ordinal st succ b₂ in succ a₁ holds
b₁ . (succ b₂) = (b₁ . b₂) +^ a₂ ) & ( for b₂ being Ordinal st b₂ in succ a₁ & b₂ <> {} & b₂ is_limit_ordinal holds
b₁ . b₂ = union (sup (b₁ | b₂)) ) );
correctness

proof end;

end;

:: deftheorem Def19 defines *^ ORDINAL2:def 19 :

definition

let c₁, c₂ be Ordinal;
func exp c₁,c₂ -> Ordinal means :Def20: :: ORDINAL2:def 20
ex b₁ being Ordinal-Sequence st
( a₃ = last b₁ & dom b₁ = succ a₂ & b₁ . {} = one & ( for b₂ being Ordinal st succ b₂ in succ a₂ holds
b₁ . (succ b₂) = a₁ *^ (b₁ . b₂) ) & ( for b₂ being Ordinal st b₂ in succ a₂ & b₂ <> {} & b₂ is_limit_ordinal holds
b₁ . b₂ = lim (b₁ | b₂) ) );
correctness

proof end;

end;

:: deftheorem Def20 defines exp ORDINAL2:def 20 :

theorem Th36: :: ORDINAL2:36

canceled;

theorem Th37: :: ORDINAL2:37

canceled;

theorem Th38: :: ORDINAL2:38

canceled;

theorem Th39: :: ORDINAL2:39

canceled;

theorem Th40: :: ORDINAL2:40

canceled;

theorem Th41: :: ORDINAL2:41

canceled;

theorem Th42: :: ORDINAL2:42

canceled;

theorem Th43: :: ORDINAL2:43

canceled;

theorem Th44: :: ORDINAL2:44

for b₁ being Ordinal holds b₁ +^ {} = b₁

proof end;

theorem Th45: :: ORDINAL2:45

for b₁, b₂ being Ordinal holds b₁ +^ (succ b₂) = succ (b₁ +^ b₂)

proof end;

theorem Th46: :: ORDINAL2:46

for b₁, b₂ being Ordinal st b₁ <> {} & b₁ is_limit_ordinal holds
for b₃ being Ordinal-Sequence st dom b₃ = b₁ & ( for b₄ being Ordinal st b₄ in b₁ holds
b₃ . b₄ = b₂ +^ b₄ ) holds
b₂ +^ b₁ = sup b₃

proof end;

theorem Th47: :: ORDINAL2:47

for b₁ being Ordinal holds {} +^ b₁ = b₁

proof end;

theorem Th48: :: ORDINAL2:48

for b₁ being Ordinal holds b₁ +^ one = succ b₁

proof end;

theorem Th49: :: ORDINAL2:49

for b₁, b₂, b₃ being Ordinal st b₁ in b₂ holds
b₃ +^ b₁ in b₃ +^ b₂

proof end;

theorem Th50: :: ORDINAL2:50

for b₁, b₂, b₃ being Ordinal st b₁ c= b₂ holds
b₃ +^ b₁ c= b₃ +^ b₂

proof end;

theorem Th51: :: ORDINAL2:51

for b₁, b₂, b₃ being Ordinal st b₁ c= b₂ holds
b₁ +^ b₃ c= b₂ +^ b₃

proof end;

theorem Th52: :: ORDINAL2:52

for b₁ being Ordinal holds {} *^ b₁ = {}

proof end;

theorem Th53: :: ORDINAL2:53

for b₁, b₂ being Ordinal holds (succ b₁) *^ b₂ = (b₁ *^ b₂) +^ b₂

proof end;

theorem Th54: :: ORDINAL2:54

for b₁, b₂ being Ordinal st b₁ <> {} & b₁ is_limit_ordinal holds
for b₃ being Ordinal-Sequence st dom b₃ = b₁ & ( for b₄ being Ordinal st b₄ in b₁ holds
b₃ . b₄ = b₄ *^ b₂ ) holds
b₁ *^ b₂ = union (sup b₃)

proof end;

theorem Th55: :: ORDINAL2:55

for b₁ being Ordinal holds b₁ *^ {} = {}

proof end;

theorem Th56: :: ORDINAL2:56

for b₁ being Ordinal holds
( one *^ b₁ = b₁ & b₁ *^ one = b₁ )

proof end;

theorem Th57: :: ORDINAL2:57

for b₁, b₂, b₃ being Ordinal st b₁ <> {} & b₂ in b₃ holds
b₂ *^ b₁ in b₃ *^ b₁

proof end;

theorem Th58: :: ORDINAL2:58

for b₁, b₂, b₃ being Ordinal st b₁ c= b₂ holds
b₁ *^ b₃ c= b₂ *^ b₃

proof end;

theorem Th59: :: ORDINAL2:59

for b₁, b₂, b₃ being Ordinal st b₁ c= b₂ holds
b₃ *^ b₁ c= b₃ *^ b₂

proof end;

theorem Th60: :: ORDINAL2:60

for b₁ being Ordinal holds exp b₁,{} = one

proof end;

theorem Th61: :: ORDINAL2:61

for b₁, b₂ being Ordinal holds exp b₁,(succ b₂) = b₁ *^ (exp b₁,b₂)

proof end;

theorem Th62: :: ORDINAL2:62

for b₁, b₂ being Ordinal st b₁ <> {} & b₁ is_limit_ordinal holds
for b₃ being Ordinal-Sequence st dom b₃ = b₁ & ( for b₄ being Ordinal st b₄ in b₁ holds
b₃ . b₄ = exp b₂,b₄ ) holds
exp b₂,b₁ = lim b₃

proof end;

theorem Th63: :: ORDINAL2:63

for b₁ being Ordinal holds
( exp b₁,one = b₁ & exp one ,b₁ = one )

proof end;

definition

let c₁ be set ;
attr a₁ is natural means :Def21: :: ORDINAL2:def 21
a₁ in omega ;

end;

:: deftheorem Def21 defines natural ORDINAL2:def 21 :

theorem Th64: :: ORDINAL2:64

canceled;

theorem Th65: :: ORDINAL2:65

for b₁ being Ordinal ex b₂, b₃ being Ordinal st
( b₂ is_limit_ordinal & b₃ is natural & b₁ = b₂ +^ b₃ )

proof end;

registration

let c₁ be set ;
let c₂ be Ordinal;
cluster a₁ --> a₂ -> Ordinal-yielding ;
coherence

proof end;

end;