:: ORDINAL4 semantic presentation

registration

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

end;

theorem Th1: :: ORDINAL4:1

for b₁ being Ordinal-Sequence
for b₂ being Ordinal st dom b₁ = succ b₂ holds
( last b₁ is_limes_of b₁ & lim b₁ = last b₁ )

proof end;

definition

let c₁, c₂ be T-Sequence;
func c₁ ^ c₂ -> T-Sequence means :Def1: :: ORDINAL4:def 1
( dom a₃ = (dom a₁) +^ (dom a₂) & ( for b₁ being Ordinal st b₁ in dom a₁ holds
a₃ . b₁ = a₁ . b₁ ) & ( for b₁ being Ordinal st b₁ in dom a₂ holds
a₃ . ((dom a₁) +^ b₁) = a₂ . b₁ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines ^ ORDINAL4:def 1 :

registration

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

proof end;

end;

theorem Th2: :: ORDINAL4:2

canceled;

theorem Th3: :: ORDINAL4:3

for b₁, b₂ being Ordinal-Sequence
for b₃ being Ordinal st b₃ is_limes_of b₁ holds
b₃ is_limes_of b₂ ^ b₁

proof end;

theorem Th4: :: ORDINAL4:4

for b₁ being Ordinal-Sequence
for b₂, b₃ being Ordinal st b₂ is_limes_of b₁ holds
b₃ +^ b₂ is_limes_of b₃ +^ b₁

proof end;

Lemma3: for b₁ being Ordinal-Sequence
for b₂ being Ordinal st b₂ is_limes_of b₁ holds
dom b₁ <> {}

proof end;

theorem Th5: :: ORDINAL4:5

for b₁ being Ordinal-Sequence
for b₂, b₃ being Ordinal st b₂ is_limes_of b₁ holds
b₂ *^ b₃ is_limes_of b₁ *^ b₃

proof end;

theorem Th6: :: ORDINAL4:6

for b₁, b₂ being Ordinal-Sequence
for b₃, b₄ being Ordinal st dom b₁ = dom b₂ & b₃ is_limes_of b₁ & b₄ is_limes_of b₂ & ( for b₅ being Ordinal st b₅ in dom b₁ holds
b₁ . b₅ c= b₂ . b₅ or for b₅ being Ordinal st b₅ in dom b₁ holds
b₁ . b₅ in b₂ . b₅ ) holds
b₃ c= b₄

proof end;

theorem Th7: :: ORDINAL4:7

for b₁ being Ordinal-Sequence
for b₂ being Ordinal
for b₃, b₄ being Ordinal-Sequence st dom b₃ = dom b₁ & dom b₁ = dom b₄ & b₂ is_limes_of b₃ & b₂ is_limes_of b₄ & ( for b₅ being Ordinal st b₅ in dom b₁ holds
( b₃ . b₅ c= b₁ . b₅ & b₁ . b₅ c= b₄ . b₅ ) ) holds
b₂ is_limes_of b₁

proof end;

theorem Th8: :: ORDINAL4:8

for b₁ being Ordinal-Sequence st dom b₁ <> {} & dom b₁ is_limit_ordinal & b₁ is increasing holds
( sup b₁ is_limes_of b₁ & lim b₁ = sup b₁ )

proof end;

theorem Th9: :: ORDINAL4:9

for b₁ being Ordinal-Sequence
for b₂, b₃ being Ordinal st b₁ is increasing & b₂ c= b₃ & b₃ in dom b₁ holds
b₁ . b₂ c= b₁ . b₃

proof end;

theorem Th10: :: ORDINAL4:10

for b₁ being Ordinal-Sequence
for b₂ being Ordinal st b₁ is increasing & b₂ in dom b₁ holds
b₂ c= b₁ . b₂

proof end;

theorem Th11: :: ORDINAL4:11

for b₁ being Ordinal-Sequence
for b₂ being Ordinal st b₁ is increasing holds
b₁ " b₂ is Ordinal

proof end;

theorem Th12: :: ORDINAL4:12

for b₁, b₂ being Ordinal-Sequence st b₁ is increasing holds
b₂ * b₁ is Ordinal-Sequence

proof end;

theorem Th13: :: ORDINAL4:13

for b₁, b₂ being Ordinal-Sequence st b₁ is increasing & b₂ is increasing holds
ex b₃ being Ordinal-Sequence st
( b₃ = b₁ * b₂ & b₃ is increasing )

proof end;

theorem Th14: :: ORDINAL4:14

for b₁ being Ordinal-Sequence
for b₂ being Ordinal
for b₃, b₄ being Ordinal-Sequence st b₃ is increasing & b₂ is_limes_of b₄ & sup (rng b₃) = dom b₄ & b₁ = b₄ * b₃ holds
b₂ is_limes_of b₁

proof end;

theorem Th15: :: ORDINAL4:15

for b₁ being Ordinal-Sequence
for b₂ being Ordinal st b₁ is increasing holds
b₁ | b₂ is increasing

proof end;

theorem Th16: :: ORDINAL4:16

for b₁ being Ordinal-Sequence st b₁ is increasing & dom b₁ is_limit_ordinal holds
sup b₁ is_limit_ordinal

proof end;

Lemma14: for b₁, b₂ being Function
for b₃ being set st rng b₁ c= b₃ holds
(b₂ | b₃) * b₁ = b₂ * b₁

proof end;

theorem Th17: :: ORDINAL4:17

for b₁, b₂, b₃ being Ordinal-Sequence st b₁ is increasing & b₁ is continuous & b₂ is continuous & b₃ = b₂ * b₁ holds
b₃ is continuous

proof end;

theorem Th18: :: ORDINAL4:18

for b₁ being Ordinal-Sequence
for b₂ being Ordinal st ( for b₃ being Ordinal st b₃ in dom b₁ holds
b₁ . b₃ = b₂ +^ b₃ ) holds
b₁ is increasing

proof end;

theorem Th19: :: ORDINAL4:19

for b₁ being Ordinal-Sequence
for b₂ being Ordinal st b₂ <> {} & ( for b₃ being Ordinal st b₃ in dom b₁ holds
b₁ . b₃ = b₃ *^ b₂ ) holds
b₁ is increasing

proof end;

theorem Th20: :: ORDINAL4:20

for b₁ being Ordinal st b₁ <> {} holds
exp {} ,b₁ = {}

proof end;

Lemma17: for 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₃ ) holds
{} is_limes_of b₂

proof end;

Lemma18: for 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 one ,b₃ ) holds
one is_limes_of b₂

proof end;

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

proof end;

theorem Th21: :: ORDINAL4:21

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₁ is_limes_of b₃

proof end;

theorem Th22: :: ORDINAL4:22

for b₁, b₂ being Ordinal st b₁ <> {} holds
exp b₁,b₂ <> {}

proof end;

theorem Th23: :: ORDINAL4:23

for b₁, b₂ being Ordinal st one in b₁ holds
exp b₁,b₂ in exp b₁,(succ b₂)

proof end;

theorem Th24: :: ORDINAL4:24

for b₁, b₂, b₃ being Ordinal st one in b₁ & b₂ in b₃ holds
exp b₁,b₂ in exp b₁,b₃

proof end;

theorem Th25: :: ORDINAL4:25

for b₁ being Ordinal-Sequence
for b₂ being Ordinal st one in b₂ & ( for b₃ being Ordinal st b₃ in dom b₁ holds
b₁ . b₃ = exp b₂,b₃ ) holds
b₁ is increasing

proof end;

theorem Th26: :: ORDINAL4:26

for b₁, b₂ being Ordinal st one in b₁ & 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₂ = sup b₃

proof end;

theorem Th27: :: ORDINAL4:27

for b₁, b₂, b₃ being Ordinal st b₁ <> {} & b₂ c= b₃ holds
exp b₁,b₂ c= exp b₁,b₃

proof end;

theorem Th28: :: ORDINAL4:28

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

proof end;

theorem Th29: :: ORDINAL4:29

for b₁, b₂ being Ordinal st one in b₁ & b₂ <> {} holds
one in exp b₁,b₂

proof end;

theorem Th30: :: ORDINAL4:30

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

proof end;

theorem Th31: :: ORDINAL4:31

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

proof end;

theorem Th32: :: ORDINAL4:32

for b₁, b₂ being Ordinal st one in b₁ holds
b₂ c= exp b₁,b₂

proof end;

scheme :: ORDINAL4:sch 1
s1{ F₁( Ordinal) -> Ordinal } :

ex b₁ being Ordinal st F₁(b₁) = b₁

provided

E26: for b₁, b₂ being Ordinal st b₁ in b₂ holds
F₁(b₁) in F₁(b₂) and
E27: for b₁ being Ordinal-Sequence
for 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₄ = F₁(b₄) ) holds
F₁(b₂) is_limes_of b₃

proof end;

definition

let c₁ be Universe;
mode Ordinal of c₁ -> Ordinal means :Def2: :: ORDINAL4:def 2
a₂ in a₁;
existence

proof end;

mode Ordinal-Sequence of c₁ -> Ordinal-Sequence means :Def3: :: ORDINAL4:def 3
( dom a₂ = On a₁ & rng a₂ c= On a₁ );
existence

proof end;

end;

:: deftheorem Def2 defines Ordinal ORDINAL4:def 2 :

:: deftheorem Def3 defines Ordinal-Sequence ORDINAL4:def 3 :

registration

let c₁ be Universe;
cluster non empty Ordinal of a₁;
existence

proof end;

end;

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

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

proof end;

definition

let c₁ be Universe;
func 0-element_of c₁ -> Ordinal of a₁ equals :: ORDINAL4:def 4
{} ;
correctness

proof end;

func 1-element_of c₁ -> non empty Ordinal of a₁ equals :: ORDINAL4:def 5
one ;
correctness

proof end;

let c₂ be Ordinal-Sequence of c₁;
let c₃ be Ordinal of c₁;
redefine func . as c₂ . c₃ -> Ordinal of a₁;
coherence

proof end;

end;

:: deftheorem Def4 defines 0-element_of ORDINAL4:def 4 :

:: deftheorem Def5 defines 1-element_of ORDINAL4:def 5 :

definition

let c₁ be Universe;
let c₂, c₃ be Ordinal-Sequence of c₁;
redefine func * as c₃ * c₂ -> Ordinal-Sequence of a₁;
coherence

proof end;

end;

theorem Th33: :: ORDINAL4:33

canceled;

theorem Th34: :: ORDINAL4:34

canceled;

theorem Th35: :: ORDINAL4:35

for b₁ being Universe holds
( 0-element_of b₁ = {} & 1-element_of b₁ = one ) ;

definition

let c₁ be Universe;
let c₂ be Ordinal of c₁;
redefine func succ as succ c₂ -> non empty Ordinal of a₁;
coherence

proof end;

let c₃ be Ordinal of c₁;
redefine func +^ as c₂ +^ c₃ -> Ordinal of a₁;
coherence

proof end;

end;

definition

let c₁ be Universe;
let c₂, c₃ be Ordinal of c₁;
redefine func *^ as c₂ *^ c₃ -> Ordinal of a₁;
coherence

proof end;

end;

theorem Th36: :: ORDINAL4:36

for b₁ being Universe
for b₂ being Ordinal of b₁
for b₃ being Ordinal-Sequence of b₁ holds b₂ in dom b₃

proof end;

theorem Th37: :: ORDINAL4:37

for b₁ being Ordinal-Sequence
for b₂ being Universe st dom b₁ in b₂ & rng b₁ c= b₂ holds
sup b₁ in b₂

proof end;

theorem Th38: :: ORDINAL4:38

for b₁ being Universe
for b₂ being Ordinal-Sequence of b₁ st b₂ is increasing & b₂ is continuous & omega in b₁ holds
ex b₃ being Ordinal st
( b₃ in dom b₂ & b₂ . b₃ = b₃ )

proof end;