:: by Grzegorz Bancerek

::

:: Received July 18, 1989

:: Copyright (c) 1990 Association of Mizar Users

begin

scheme :: ORDINAL2:sch 1

OrdinalInd{ P_{1}[ Ordinal] } :

provided

OrdinalInd{ P

provided

A1:
P_{1}[ {} ]
and

A2: for A being Ordinal st P_{1}[A] holds

P_{1}[ succ A]
and

A3: for A being Ordinal st A <> {} & A is limit_ordinal & ( for B being Ordinal st B in A holds

P_{1}[B] ) holds

P_{1}[A]

A2: for A being Ordinal st P

P

A3: for A being Ordinal st A <> {} & A is limit_ordinal & ( for B being Ordinal st B in A holds

P

P

proof end;

theorem Th1: :: ORDINAL2:1

proof end;

theorem Th2: :: ORDINAL2:2

proof end;

theorem :: ORDINAL2:3

proof end;

theorem :: ORDINAL2:4

{} is limit_ordinal

proof end;

theorem Th5: :: ORDINAL2:5

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;
func last L -> set equals :: ORDINAL2:def 1

L . (union (dom L));

coherence

L . (union (dom L)) is set ;

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

theorem :: ORDINAL2:8

canceled;

theorem :: ORDINAL2:9

proof end;

theorem Th10: :: ORDINAL2:10

proof end;

theorem Th11: :: ORDINAL2:11

proof end;

theorem :: ORDINAL2:12

canceled;

theorem :: ORDINAL2:13

proof end;

theorem :: ORDINAL2:14

proof end;

theorem :: ORDINAL2:15

proof end;

theorem :: ORDINAL2:16

canceled;

theorem Th17: :: ORDINAL2:17

proof end;

registration

cluster epsilon-transitive epsilon-connected ordinal limit_ordinal set ;

existence

ex b_{1} being Ordinal st b_{1} is limit_ordinal

end;
existence

ex b

proof 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

( On X c= it & ( for A being Ordinal st On X c= A holds

it c= A ) );

existence

ex b_{1} being Ordinal st

( On X c= b_{1} & ( for A being Ordinal st On X c= A holds

b_{1} c= A ) )

for b_{1}, b_{2} being Ordinal st On X c= b_{1} & ( for A being Ordinal st On X c= A holds

b_{1} c= A ) & On X c= b_{2} & ( for A being Ordinal st On X c= A holds

b_{2} c= A ) holds

b_{1} = b_{2}

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

( On X c= b

b

proof end;

uniqueness for b

b

b

b

proof 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

( b

b

theorem :: ORDINAL2:18

canceled;

theorem :: ORDINAL2:19

canceled;

theorem :: ORDINAL2:20

canceled;

theorem :: ORDINAL2:21

canceled;

theorem :: ORDINAL2:22

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

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

proof end;

theorem :: ORDINAL2:25

proof end;

theorem Th26: :: ORDINAL2:26

proof end;

theorem Th27: :: ORDINAL2:27

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

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

proof end;

theorem :: ORDINAL2:30

proof end;

theorem :: ORDINAL2:31

proof end;

theorem :: ORDINAL2:32

proof end;

scheme :: ORDINAL2:sch 2

TSLambda{ F_{1}() -> Ordinal, F_{2}( Ordinal) -> set } :

TSLambda{ F

ex L being T-Sequence st

( dom L = F_{1}() & ( for A being Ordinal st A in F_{1}() holds

L . A = F_{2}(A) ) )

( dom L = F

L . A = F

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;
attr f is Ordinal-yielding means :Def8: :: ORDINAL2:def 8

ex A being Ordinal st rng f c= A;

:: 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_{1} being T-Sequence st b_{1} is Ordinal-yielding

end;
existence

ex b

proof end;

registration

let A be Ordinal;

cluster T-Sequence-like Relation-like A -valued Function-like -> Ordinal-yielding set ;

coherence

for b_{1} being T-Sequence of holds b_{1} is Ordinal-yielding

end;
cluster T-Sequence-like Relation-like A -valued Function-like -> Ordinal-yielding set ;

coherence

for b

proof end;

registration

let L be Ordinal-Sequence;

let A be Ordinal;

cluster L | A -> Ordinal-yielding ;

coherence

L | A is Ordinal-yielding

end;
let A be Ordinal;

cluster L | A -> Ordinal-yielding ;

coherence

L | A is Ordinal-yielding

proof end;

theorem :: ORDINAL2:33

canceled;

theorem Th34: :: ORDINAL2:34

proof end;

registration

let f be Ordinal-Sequence;

let a be Ordinal;

cluster f . a -> ordinal ;

coherence

f . a is ordinal

end;
let a be Ordinal;

cluster f . a -> ordinal ;

coherence

f . a is ordinal

proof end;

scheme :: ORDINAL2:sch 3

OSLambda{ F_{1}() -> Ordinal, F_{2}( Ordinal) -> Ordinal } :

OSLambda{ F

ex fi being Ordinal-Sequence st

( dom fi = F_{1}() & ( for A being Ordinal st A in F_{1}() holds

fi . A = F_{2}(A) ) )

( dom fi = F

fi . A = F

proof end;

scheme :: ORDINAL2:sch 4

TSUniq1{ F_{1}() -> Ordinal, F_{2}() -> set , F_{3}( Ordinal, set ) -> set , F_{4}( Ordinal, T-Sequence) -> set , F_{5}() -> T-Sequence, F_{6}() -> T-Sequence } :

provided

TSUniq1{ F

provided

A1:
dom F_{5}() = F_{1}()
and

A2: ( {} in F_{1}() implies F_{5}() . {} = F_{2}() )
and

A3: for A being Ordinal st succ A in F_{1}() holds

F_{5}() . (succ A) = F_{3}(A,(F_{5}() . A))
and

A4: for A being Ordinal st A in F_{1}() & A <> {} & A is limit_ordinal holds

F_{5}() . A = F_{4}(A,(F_{5}() | A))
and

A5: dom F_{6}() = F_{1}()
and

A6: ( {} in F_{1}() implies F_{6}() . {} = F_{2}() )
and

A7: for A being Ordinal st succ A in F_{1}() holds

F_{6}() . (succ A) = F_{3}(A,(F_{6}() . A))
and

A8: for A being Ordinal st A in F_{1}() & A <> {} & A is limit_ordinal holds

F_{6}() . A = F_{4}(A,(F_{6}() | A))

A2: ( {} in F

A3: for A being Ordinal st succ A in F

F

A4: for A being Ordinal st A in F

F

A5: dom F

A6: ( {} in F

A7: for A being Ordinal st succ A in F

F

A8: for A being Ordinal st A in F

F

proof end;

scheme :: ORDINAL2:sch 5

TSExist1{ F_{1}() -> Ordinal, F_{2}() -> set , F_{3}( Ordinal, set ) -> set , F_{4}( Ordinal, T-Sequence) -> set } :

TSExist1{ F

ex L being T-Sequence st

( dom L = F_{1}() & ( {} in F_{1}() implies L . {} = F_{2}() ) & ( for A being Ordinal st succ A in F_{1}() holds

L . (succ A) = F_{3}(A,(L . A)) ) & ( for A being Ordinal st A in F_{1}() & A <> {} & A is limit_ordinal holds

L . A = F_{4}(A,(L | A)) ) )

( dom L = F

L . (succ A) = F

L . A = F

proof end;

scheme :: ORDINAL2:sch 6

TSResult{ F_{1}() -> T-Sequence, F_{2}( Ordinal) -> set , F_{3}() -> Ordinal, F_{4}() -> set , F_{5}( Ordinal, set ) -> set , F_{6}( Ordinal, T-Sequence) -> set } :

provided

TSResult{ F

provided

A1:
for A being Ordinal

for x being set holds

( x = F_{2}(A) iff ex L being T-Sequence st

( x = last L & dom L = succ A & L . {} = F_{4}() & ( for C being Ordinal st succ C in succ A holds

L . (succ C) = F_{5}(C,(L . C)) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds

L . C = F_{6}(C,(L | C)) ) ) )
and

A2: dom F_{1}() = F_{3}()
and

A3: ( {} in F_{3}() implies F_{1}() . {} = F_{4}() )
and

A4: for A being Ordinal st succ A in F_{3}() holds

F_{1}() . (succ A) = F_{5}(A,(F_{1}() . A))
and

A5: for A being Ordinal st A in F_{3}() & A <> {} & A is limit_ordinal holds

F_{1}() . A = F_{6}(A,(F_{1}() | A))

for x being set holds

( x = F

( x = last L & dom L = succ A & L . {} = F

L . (succ C) = F

L . C = F

A2: dom F

A3: ( {} in F

A4: for A being Ordinal st succ A in F

F

A5: for A being Ordinal st A in F

F

proof end;

scheme :: ORDINAL2:sch 7

TSDef{ F_{1}() -> Ordinal, F_{2}() -> set , F_{3}( Ordinal, set ) -> set , F_{4}( Ordinal, T-Sequence) -> set } :

TSDef{ F

( ex x being set ex L being T-Sequence st

( x = last L & dom L = succ F_{1}() & L . {} = F_{2}() & ( for C being Ordinal st succ C in succ F_{1}() holds

L . (succ C) = F_{3}(C,(L . C)) ) & ( for C being Ordinal st C in succ F_{1}() & C <> {} & C is limit_ordinal holds

L . C = F_{4}(C,(L | C)) ) ) & ( for x1, x2 being set st ex L being T-Sequence st

( x1 = last L & dom L = succ F_{1}() & L . {} = F_{2}() & ( for C being Ordinal st succ C in succ F_{1}() holds

L . (succ C) = F_{3}(C,(L . C)) ) & ( for C being Ordinal st C in succ F_{1}() & C <> {} & C is limit_ordinal holds

L . C = F_{4}(C,(L | C)) ) ) & ex L being T-Sequence st

( x2 = last L & dom L = succ F_{1}() & L . {} = F_{2}() & ( for C being Ordinal st succ C in succ F_{1}() holds

L . (succ C) = F_{3}(C,(L . C)) ) & ( for C being Ordinal st C in succ F_{1}() & C <> {} & C is limit_ordinal holds

L . C = F_{4}(C,(L | C)) ) ) holds

x1 = x2 ) )

( x = last L & dom L = succ F

L . (succ C) = F

L . C = F

( x1 = last L & dom L = succ F

L . (succ C) = F

L . C = F

( x2 = last L & dom L = succ F

L . (succ C) = F

L . C = F

x1 = x2 ) )

proof end;

scheme :: ORDINAL2:sch 8

TSResult0{ F_{1}( Ordinal) -> set , F_{2}() -> set , F_{3}( Ordinal, set ) -> set , F_{4}( Ordinal, T-Sequence) -> set } :

provided

TSResult0{ F

provided

A1:
for A being Ordinal

for x being set holds

( x = F_{1}(A) iff ex L being T-Sequence st

( x = last L & dom L = succ A & L . {} = F_{2}() & ( for C being Ordinal st succ C in succ A holds

L . (succ C) = F_{3}(C,(L . C)) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds

L . C = F_{4}(C,(L | C)) ) ) )

for x being set holds

( x = F

( x = last L & dom L = succ A & L . {} = F

L . (succ C) = F

L . C = F

proof end;

scheme :: ORDINAL2:sch 9

TSResultS{ F_{1}() -> set , F_{2}( Ordinal, set ) -> set , F_{3}( Ordinal, T-Sequence) -> set , F_{4}( Ordinal) -> set } :

provided

TSResultS{ F

provided

A1:
for A being Ordinal

for x being set holds

( x = F_{4}(A) iff ex L being T-Sequence st

( x = last L & dom L = succ A & L . {} = F_{1}() & ( for C being Ordinal st succ C in succ A holds

L . (succ C) = F_{2}(C,(L . C)) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds

L . C = F_{3}(C,(L | C)) ) ) )

for x being set holds

( x = F

( x = last L & dom L = succ A & L . {} = F

L . (succ C) = F

L . C = F

proof end;

scheme :: ORDINAL2:sch 10

TSResultL{ F_{1}() -> T-Sequence, F_{2}() -> Ordinal, F_{3}( Ordinal) -> set , F_{4}() -> set , F_{5}( Ordinal, set ) -> set , F_{6}( Ordinal, T-Sequence) -> set } :

provided

TSResultL{ F

provided

A1:
for A being Ordinal

for x being set holds

( x = F_{3}(A) iff ex L being T-Sequence st

( x = last L & dom L = succ A & L . {} = F_{4}() & ( for C being Ordinal st succ C in succ A holds

L . (succ C) = F_{5}(C,(L . C)) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds

L . C = F_{6}(C,(L | C)) ) ) )
and

A2: ( F_{2}() <> {} & F_{2}() is limit_ordinal )
and

A3: dom F_{1}() = F_{2}()
and

A4: for A being Ordinal st A in F_{2}() holds

F_{1}() . A = F_{3}(A)

for x being set holds

( x = F

( x = last L & dom L = succ A & L . {} = F

L . (succ C) = F

L . C = F

A2: ( F

A3: dom F

A4: for A being Ordinal st A in F

F

proof end;

scheme :: ORDINAL2:sch 11

OSExist{ F_{1}() -> Ordinal, F_{2}() -> Ordinal, F_{3}( Ordinal, Ordinal) -> Ordinal, F_{4}( Ordinal, T-Sequence) -> Ordinal } :

OSExist{ F

ex fi being Ordinal-Sequence st

( dom fi = F_{1}() & ( {} in F_{1}() implies fi . {} = F_{2}() ) & ( for A being Ordinal st succ A in F_{1}() holds

fi . (succ A) = F_{3}(A,(fi . A)) ) & ( for A being Ordinal st A in F_{1}() & A <> {} & A is limit_ordinal holds

fi . A = F_{4}(A,(fi | A)) ) )

( dom fi = F

fi . (succ A) = F

fi . A = F

proof end;

scheme :: ORDINAL2:sch 12

OSResult{ F_{1}() -> Ordinal-Sequence, F_{2}( Ordinal) -> Ordinal, F_{3}() -> Ordinal, F_{4}() -> Ordinal, F_{5}( Ordinal, Ordinal) -> Ordinal, F_{6}( Ordinal, T-Sequence) -> Ordinal } :

provided

OSResult{ F

provided

A1:
for A, B being Ordinal holds

( B = F_{2}(A) iff ex fi being Ordinal-Sequence st

( B = last fi & dom fi = succ A & fi . {} = F_{4}() & ( for C being Ordinal st succ C in succ A holds

fi . (succ C) = F_{5}(C,(fi . C)) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds

fi . C = F_{6}(C,(fi | C)) ) ) )
and

A2: dom F_{1}() = F_{3}()
and

A3: ( {} in F_{3}() implies F_{1}() . {} = F_{4}() )
and

A4: for A being Ordinal st succ A in F_{3}() holds

F_{1}() . (succ A) = F_{5}(A,(F_{1}() . A))
and

A5: for A being Ordinal st A in F_{3}() & A <> {} & A is limit_ordinal holds

F_{1}() . A = F_{6}(A,(F_{1}() | A))

( B = F

( B = last fi & dom fi = succ A & fi . {} = F

fi . (succ C) = F

fi . C = F

A2: dom F

A3: ( {} in F

A4: for A being Ordinal st succ A in F

F

A5: for A being Ordinal st A in F

F

proof end;

scheme :: ORDINAL2:sch 13

OSDef{ F_{1}() -> Ordinal, F_{2}() -> Ordinal, F_{3}( Ordinal, Ordinal) -> Ordinal, F_{4}( Ordinal, T-Sequence) -> Ordinal } :

OSDef{ F

( ex A being Ordinal ex fi being Ordinal-Sequence st

( A = last fi & dom fi = succ F_{1}() & fi . {} = F_{2}() & ( for C being Ordinal st succ C in succ F_{1}() holds

fi . (succ C) = F_{3}(C,(fi . C)) ) & ( for C being Ordinal st C in succ F_{1}() & C <> {} & C is limit_ordinal holds

fi . C = F_{4}(C,(fi | C)) ) ) & ( for A1, A2 being Ordinal st ex fi being Ordinal-Sequence st

( A1 = last fi & dom fi = succ F_{1}() & fi . {} = F_{2}() & ( for C being Ordinal st succ C in succ F_{1}() holds

fi . (succ C) = F_{3}(C,(fi . C)) ) & ( for C being Ordinal st C in succ F_{1}() & C <> {} & C is limit_ordinal holds

fi . C = F_{4}(C,(fi | C)) ) ) & ex fi being Ordinal-Sequence st

( A2 = last fi & dom fi = succ F_{1}() & fi . {} = F_{2}() & ( for C being Ordinal st succ C in succ F_{1}() holds

fi . (succ C) = F_{3}(C,(fi . C)) ) & ( for C being Ordinal st C in succ F_{1}() & C <> {} & C is limit_ordinal holds

fi . C = F_{4}(C,(fi | C)) ) ) holds

A1 = A2 ) )

( A = last fi & dom fi = succ F

fi . (succ C) = F

fi . C = F

( A1 = last fi & dom fi = succ F

fi . (succ C) = F

fi . C = F

( A2 = last fi & dom fi = succ F

fi . (succ C) = F

fi . C = F

A1 = A2 ) )

proof end;

scheme :: ORDINAL2:sch 14

OSResult0{ F_{1}( Ordinal) -> Ordinal, F_{2}() -> Ordinal, F_{3}( Ordinal, Ordinal) -> Ordinal, F_{4}( Ordinal, T-Sequence) -> Ordinal } :

provided

OSResult0{ F

provided

A1:
for A, B being Ordinal holds

( B = F_{1}(A) iff ex fi being Ordinal-Sequence st

( B = last fi & dom fi = succ A & fi . {} = F_{2}() & ( for C being Ordinal st succ C in succ A holds

fi . (succ C) = F_{3}(C,(fi . C)) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds

fi . C = F_{4}(C,(fi | C)) ) ) )

( B = F

( B = last fi & dom fi = succ A & fi . {} = F

fi . (succ C) = F

fi . C = F

proof end;

scheme :: ORDINAL2:sch 15

OSResultS{ F_{1}() -> Ordinal, F_{2}( Ordinal, Ordinal) -> Ordinal, F_{3}( Ordinal, T-Sequence) -> Ordinal, F_{4}( Ordinal) -> Ordinal } :

provided

OSResultS{ F

provided

A1:
for A, B being Ordinal holds

( B = F_{4}(A) iff ex fi being Ordinal-Sequence st

( B = last fi & dom fi = succ A & fi . {} = F_{1}() & ( for C being Ordinal st succ C in succ A holds

fi . (succ C) = F_{2}(C,(fi . C)) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds

fi . C = F_{3}(C,(fi | C)) ) ) )

( B = F

( B = last fi & dom fi = succ A & fi . {} = F

fi . (succ C) = F

fi . C = F

proof end;

scheme :: ORDINAL2:sch 16

OSResultL{ F_{1}() -> Ordinal-Sequence, F_{2}() -> Ordinal, F_{3}( Ordinal) -> Ordinal, F_{4}() -> Ordinal, F_{5}( Ordinal, Ordinal) -> Ordinal, F_{6}( Ordinal, T-Sequence) -> Ordinal } :

provided

OSResultL{ F

provided

A1:
for A, B being Ordinal holds

( B = F_{3}(A) iff ex fi being Ordinal-Sequence st

( B = last fi & dom fi = succ A & fi . {} = F_{4}() & ( for C being Ordinal st succ C in succ A holds

fi . (succ C) = F_{5}(C,(fi . C)) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds

fi . C = F_{6}(C,(fi | C)) ) ) )
and

A2: ( F_{2}() <> {} & F_{2}() is limit_ordinal )
and

A3: dom F_{1}() = F_{2}()
and

A4: for A being Ordinal st A in F_{2}() holds

F_{1}() . A = F_{3}(A)

( B = F

( B = last fi & dom fi = succ A & fi . {} = F

fi . (succ C) = F

fi . C = F

A2: ( F

A3: dom F

A4: for A being Ordinal st A in F

F

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

;

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

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_{1} being Ordinal ex fi being Ordinal-Sequence st

( b_{1} = inf fi & dom fi = dom L & ( for A being Ordinal st A in dom L holds

fi . A = sup (rng (L | ((dom L) \ A))) ) )

for b_{1}, b_{2} being Ordinal st ex fi being Ordinal-Sequence st

( b_{1} = 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_{2} = 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_{1} = b_{2}

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_{1} being Ordinal ex fi being Ordinal-Sequence st

( b_{1} = sup fi & dom fi = dom L & ( for A being Ordinal st A in dom L holds

fi . A = inf (rng (L | ((dom L) \ A))) ) )

for b_{1}, b_{2} being Ordinal st ex fi being Ordinal-Sequence st

( b_{1} = 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_{2} = 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_{1} = b_{2}

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

( b

fi . A = sup (rng (L | ((dom L) \ A))) ) )

proof end;

uniqueness for b

( b

fi . A = sup (rng (L | ((dom L) \ A))) ) ) & ex fi being Ordinal-Sequence st

( b

fi . A = sup (rng (L | ((dom L) \ A))) ) ) holds

b

proof end;

func lim_inf L -> Ordinal means :: ORDINAL2:def 12ex 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

( b

fi . A = inf (rng (L | ((dom L) \ A))) ) )

proof end;

uniqueness for b

( b

fi . A = inf (rng (L | ((dom L) \ A))) ) ) & ex fi being Ordinal-Sequence st

( b

fi . A = inf (rng (L | ((dom L) \ A))) ) ) holds

b

proof end;

:: deftheorem defines lim_sup ORDINAL2:def 11 :

for L being T-Sequence

for b

( b

( b

fi . A = sup (rng (L | ((dom L) \ A))) ) ) );

:: deftheorem defines lim_inf ORDINAL2:def 12 :

for L being T-Sequence

for b

( b

( b

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

:: 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_{1} being Ordinal st b_{1} is_limes_of fi
by A1;

uniqueness

for b_{1}, b_{2} being Ordinal st b_{1} is_limes_of fi & b_{2} is_limes_of fi holds

b_{1} = b_{2}

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

uniqueness

for b

b

proof 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

( b

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;
let fi be Ordinal-Sequence;

func lim (A,fi) -> Ordinal equals :: ORDINAL2:def 15

lim (fi | A);

correctness

coherence

lim (fi | A) is Ordinal;

;

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

:: 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_{1} being Ordinal ex fi being Ordinal-Sequence st

( b_{1} = 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_{1}, b_{2} being Ordinal st ex fi being Ordinal-Sequence st

( b_{1} = 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_{2} = 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_{1} = b_{2};

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

( b

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

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

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

proof end;

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

for A, B, b

( b

( b

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_{1} being Ordinal ex fi being Ordinal-Sequence st

( b_{1} = 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_{1}, b_{2} being Ordinal st ex fi being Ordinal-Sequence st

( b_{1} = 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_{2} = 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_{1} = b_{2};

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

( b

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

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

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

proof end;

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

for A, B, b

( b

( b

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_{1} being Element of O holds b_{1} is ordinal
;

end;
cluster -> ordinal Element of O;

coherence

for b

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_{1} being Ordinal ex fi being Ordinal-Sequence st

( b_{1} = 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_{1}, b_{2} being Ordinal st ex fi being Ordinal-Sequence st

( b_{1} = 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_{2} = 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_{1} = b_{2};

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

( b

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

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

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

proof end;

:: deftheorem Def20 defines exp ORDINAL2:def 20 :

for A, B, b

( b

( b

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

proof end;

theorem Th45: :: ORDINAL2:45

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

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

proof end;

Lm1: 1 = succ {}

;

theorem :: ORDINAL2:48

proof end;

theorem Th49: :: ORDINAL2:49

proof end;

theorem Th50: :: ORDINAL2:50

proof end;

theorem Th51: :: ORDINAL2:51

proof end;

theorem Th52: :: ORDINAL2:52

proof end;

theorem Th53: :: ORDINAL2:53

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)

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

proof end;

theorem Th56: :: ORDINAL2:56

proof end;

theorem Th57: :: ORDINAL2:57

proof end;

theorem :: ORDINAL2:58

proof end;

theorem :: ORDINAL2:59

proof end;

theorem Th60: :: ORDINAL2:60

proof end;

theorem Th61: :: ORDINAL2:61

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

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

proof end;

theorem :: ORDINAL2:64

canceled;

theorem :: ORDINAL2:65

proof end;

registration

let X be set ;

let o be Ordinal;

cluster X --> o -> Ordinal-yielding ;

coherence

X --> o is Ordinal-yielding

end;
let o be Ordinal;

cluster X --> o -> Ordinal-yielding ;

coherence

X --> o is Ordinal-yielding

proof end;

registration

let O be Ordinal;

let x be set ;

cluster O --> x -> T-Sequence-like ;

coherence

O --> x is T-Sequence-like

end;
let x be set ;

cluster O --> x -> T-Sequence-like ;

coherence

O --> x is T-Sequence-like

proof 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 )

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

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

proof end;

theorem :: ORDINAL2:67

proof end;

theorem :: ORDINAL2:68

proof end;

registration
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

end;
let a, b be natural number ;

cluster IFEQ (x,y,a,b) -> natural ;

coherence

IFEQ (x,y,a,b) is natural

proof end;

scheme :: ORDINAL2:sch 18

LambdaRecEx{ F_{1}() -> set , F_{2}( set , set ) -> set } :

LambdaRecEx{ F

ex f being Function st

( dom f = omega & f . {} = F_{1}() & ( for n being natural number holds f . (succ n) = F_{2}(n,(f . n)) ) )

( dom f = omega & f . {} = F

proof end;

scheme :: ORDINAL2:sch 19

RecUn{ F_{1}() -> set , F_{2}() -> Function, F_{3}() -> Function, P_{1}[ set , set , set ] } :

provided

RecUn{ F

provided

A1:
dom F_{2}() = omega
and

A2: F_{2}() . {} = F_{1}()
and

A3: for n being natural number holds P_{1}[n,F_{2}() . n,F_{2}() . (succ n)]
and

A4: dom F_{3}() = omega
and

A5: F_{3}() . {} = F_{1}()
and

A6: for n being natural number holds P_{1}[n,F_{3}() . n,F_{3}() . (succ n)]
and

A7: for n being natural number

for x, y1, y2 being set st P_{1}[n,x,y1] & P_{1}[n,x,y2] holds

y1 = y2

A2: F

A3: for n being natural number holds P

A4: dom F

A5: F

A6: for n being natural number holds P

A7: for n being natural number

for x, y1, y2 being set st P

y1 = y2

proof end;

scheme :: ORDINAL2:sch 20

LambdaRecUn{ F_{1}() -> set , F_{2}( set , set ) -> set , F_{3}() -> Function, F_{4}() -> Function } :

provided

LambdaRecUn{ F

provided

A1:
dom F_{3}() = omega
and

A2: F_{3}() . {} = F_{1}()
and

A3: for n being natural number holds F_{3}() . (succ n) = F_{2}(n,(F_{3}() . n))
and

A4: dom F_{4}() = omega
and

A5: F_{4}() . {} = F_{1}()
and

A6: for n being natural number holds F_{4}() . (succ n) = F_{2}(n,(F_{4}() . n))

A2: F

A3: for n being natural number holds F

A4: dom F

A5: F

A6: for n being natural number holds F

proof end;