:: ORDINAL4 semantic presentation

registration

let L be Ordinal-Sequence;
cluster last L -> ordinal ;
coherence ;

end;

theorem :: ORDINAL4:1

for fi being Ordinal-Sequence
for A being Ordinal st dom fi = succ A holds
( last fi is_limes_of fi & lim fi = last fi )

proof end;

definition

let fi, psi be T-Sequence;
func fi ^ psi -> T-Sequence means :Def1: :: ORDINAL4:def 1
( dom it = (dom fi) +^ (dom psi) & ( for A being Ordinal st A in dom fi holds
it . A = fi . A ) & ( for A being Ordinal st A in dom psi holds
it . ((dom fi) +^ A) = psi . A ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines ^ ORDINAL4:def 1 :

registration

let fi, psi be Ordinal-Sequence;
cluster fi ^ psi -> Ordinal-yielding ;
coherence

proof end;

end;

theorem :: ORDINAL4:2

canceled;

theorem Th3: :: ORDINAL4:3

for psi, fi being Ordinal-Sequence
for A being Ordinal st A is_limes_of psi holds
A is_limes_of fi ^ psi

proof end;

theorem :: ORDINAL4:4

for fi being Ordinal-Sequence
for A, B being Ordinal st A is_limes_of fi holds
B +^ A is_limes_of B +^ fi

proof end;

Lm1: for fi being Ordinal-Sequence
for A being Ordinal st A is_limes_of fi holds
dom fi <> {}

proof end;

theorem Th5: :: ORDINAL4:5

for fi being Ordinal-Sequence
for A, B being Ordinal st A is_limes_of fi holds
A *^ B is_limes_of fi *^ B

proof end;

theorem Th6: :: ORDINAL4:6

for fi, psi being Ordinal-Sequence
for B, C being Ordinal st dom fi = dom psi & B is_limes_of fi & C is_limes_of psi & ( for A being Ordinal st A in dom fi holds
fi . A c= psi . A or for A being Ordinal st A in dom fi holds
fi . A in psi . A ) holds
B c= C

proof end;

theorem :: ORDINAL4:7

for fi being Ordinal-Sequence
for A being Ordinal
for f1, f2 being Ordinal-Sequence st dom f1 = dom fi & dom fi = dom f2 & A is_limes_of f1 & A is_limes_of f2 & ( for A being Ordinal st A in dom fi holds
( f1 . A c= fi . A & fi . A c= f2 . A ) ) holds
A is_limes_of fi

proof end;

theorem Th8: :: ORDINAL4:8

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

proof end;

theorem Th9: :: ORDINAL4:9

for fi being Ordinal-Sequence
for A, B being Ordinal st fi is increasing & A c= B & B in dom fi holds
fi . A c= fi . B

proof end;

theorem Th10: :: ORDINAL4:10

for fi being Ordinal-Sequence
for A being Ordinal st fi is increasing & A in dom fi holds
A c= fi . A

proof end;

theorem Th11: :: ORDINAL4:11

for phi being Ordinal-Sequence
for A being Ordinal st phi is increasing holds
phi " A is Ordinal

proof end;

theorem Th12: :: ORDINAL4:12

for f1, f2 being Ordinal-Sequence st f1 is increasing holds
f2 * f1 is Ordinal-Sequence

proof end;

theorem :: ORDINAL4:13

for f1, f2 being Ordinal-Sequence st f1 is increasing & f2 is increasing holds
ex phi being Ordinal-Sequence st
( phi = f1 * f2 & phi is increasing )

proof end;

theorem Th14: :: ORDINAL4:14

for fi being Ordinal-Sequence
for A being Ordinal
for f1, f2 being Ordinal-Sequence st f1 is increasing & A is_limes_of f2 & sup (rng f1) = dom f2 & fi = f2 * f1 holds
A is_limes_of fi

proof end;

theorem Th15: :: ORDINAL4:15

for phi being Ordinal-Sequence
for A being Ordinal st phi is increasing holds
phi | A is increasing

proof end;

theorem Th16: :: ORDINAL4:16

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

proof end;

Lm2: for f, g being Function
for X being set st rng f c= X holds
(g | X) * f = g * f

proof end;

theorem :: ORDINAL4:17

for fi, psi, phi being Ordinal-Sequence st fi is increasing & fi is continuous & psi is continuous & phi = psi * fi holds
phi is continuous

proof end;

theorem :: ORDINAL4:18

for fi being Ordinal-Sequence
for C being Ordinal st ( for A being Ordinal st A in dom fi holds
fi . A = C +^ A ) holds
fi is increasing

proof end;

theorem Th19: :: ORDINAL4:19

for fi being Ordinal-Sequence
for C being Ordinal st C <> {} & ( for A being Ordinal st A in dom fi holds
fi . A = A *^ C ) holds
fi is increasing

proof end;

theorem Th20: :: ORDINAL4:20

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

proof end;

Lm3: for A being Ordinal st A <> {} & A is_limit_ordinal holds
for fi being Ordinal-Sequence st dom fi = A & ( for B being Ordinal st B in A holds
fi . B = exp {} ,B ) holds
{} is_limes_of fi

proof end;

Lm4: for A being Ordinal st A <> {} & A is_limit_ordinal holds
for fi being Ordinal-Sequence st dom fi = A & ( for B being Ordinal st B in A holds
fi . B = exp one ,B ) holds
one is_limes_of fi

proof end;

Lm5: for C, A being Ordinal st A <> {} & A is_limit_ordinal holds
ex fi being Ordinal-Sequence st
( dom fi = A & ( for B being Ordinal st B in A holds
fi . B = exp C,B ) & ex D being Ordinal st D is_limes_of fi )

proof end;

theorem Th21: :: ORDINAL4:21

for A, C being Ordinal st A <> {} & A is_limit_ordinal holds
for fi being Ordinal-Sequence st dom fi = A & ( for B being Ordinal st B in A holds
fi . B = exp C,B ) holds
exp C,A is_limes_of fi

proof end;

theorem Th22: :: ORDINAL4:22

for C, A being Ordinal st C <> {} holds
exp C,A <> {}

proof end;

theorem Th23: :: ORDINAL4:23

for C, A being Ordinal st one in C holds
exp C,A in exp C,(succ A)

proof end;

theorem Th24: :: ORDINAL4:24

for C, A, B being Ordinal st one in C & A in B holds
exp C,A in exp C,B

proof end;

theorem Th25: :: ORDINAL4:25

for fi being Ordinal-Sequence
for C being Ordinal st one in C & ( for A being Ordinal st A in dom fi holds
fi . A = exp C,A ) holds
fi is increasing

proof end;

theorem :: ORDINAL4:26

for C, A being Ordinal st one in C & A <> {} & A is_limit_ordinal holds
for fi being Ordinal-Sequence st dom fi = A & ( for B being Ordinal st B in A holds
fi . B = exp C,B ) holds
exp C,A = sup fi

proof end;

theorem :: ORDINAL4:27

for C, A, B being Ordinal st C <> {} & A c= B holds
exp C,A c= exp C,B

proof end;

theorem :: ORDINAL4:28

for A, B, C being Ordinal st A c= B holds
exp A,C c= exp B,C

proof end;

theorem :: ORDINAL4:29

for C, A being Ordinal st one in C & A <> {} holds
one in exp C,A

proof end;

theorem Th30: :: ORDINAL4:30

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

proof end;

theorem :: ORDINAL4:31

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

proof end;

theorem :: ORDINAL4:32

for C, A being Ordinal st one in C holds
A c= exp C,A

proof end;

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

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

provided

A1: for A, B being Ordinal st A in B holds
F₁(A) in F₁(B) and
A2: for fi being Ordinal-Sequence
for A being Ordinal st A <> {} & A is_limit_ordinal holds
for phi being Ordinal-Sequence st dom fi = A & ( for B being Ordinal st B in A holds
phi . B = F₁(B) ) holds
F₁(A) is_limes_of phi

proof end;

definition

let W be Universe;
mode Ordinal of W -> Ordinal means :Def2: :: ORDINAL4:def 2
it in W;
existence

proof end;

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

proof end;

end;

:: deftheorem Def2 defines Ordinal ORDINAL4:def 2 :

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

registration

let W be Universe;
cluster non empty Ordinal of W;
existence

proof end;

end;

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

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

proof end;

definition

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

proof end;

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

proof end;

let phi be Ordinal-Sequence of W;
let A1 be Ordinal of W;
:: original: .
redefine func phi . A1 -> Ordinal of W;
coherence

proof end;

end;

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

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

definition

let W be Universe;
let p2, p1 be Ordinal-Sequence of W;
:: original: *
redefine func p1 * p2 -> Ordinal-Sequence of W;
coherence

proof end;

end;

theorem :: ORDINAL4:33

canceled;

theorem :: ORDINAL4:34

canceled;

theorem :: ORDINAL4:35

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

definition

let W be Universe;
let A1 be Ordinal of W;
:: original: succ
redefine func succ A1 -> non empty Ordinal of W;
coherence

proof end;

let B1 be Ordinal of W;
:: original: +^
redefine func A1 +^ B1 -> Ordinal of W;
coherence

proof end;

end;

definition

let W be Universe;
let A1, B1 be Ordinal of W;
:: original: *^
redefine func A1 *^ B1 -> Ordinal of W;
coherence

proof end;

end;

theorem Th36: :: ORDINAL4:36

for W being Universe
for A1 being Ordinal of W
for phi being Ordinal-Sequence of W holds A1 in dom phi

proof end;

theorem Th37: :: ORDINAL4:37

for fi being Ordinal-Sequence
for W being Universe st dom fi in W & rng fi c= W holds
sup fi in W

proof end;

theorem :: ORDINAL4:38

for W being Universe
for phi being Ordinal-Sequence of W st phi is increasing & phi is continuous & omega in W holds
ex A being Ordinal st
( A in dom phi & phi . A = A )

proof end;