:: by Grzegorz Bancerek

::

:: Received July 18, 1989

:: Copyright (c) 1990-2021 Association of Mizar Users

:: deftheorem defines last ORDINAL2:def 1 :

for L being Sequence holds last L = L . (union (dom L));

for L being Sequence holds last L = L . (union (dom L));

theorem :: ORDINAL2:6

definition

let X be set ;

coherence

meet (On X) is Ordinal

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

meet (On X) is Ordinal

proof end;

func sup X -> Ordinal means :Def3: :: ORDINAL2:def 3

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

it c= A ) );

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

it c= A ) );

ex b

( On X c= b

b

proof end;

uniqueness for b

b

b

b

:: deftheorem Def3 defines sup ORDINAL2:def 3 :

for X being set

for b_{2} being Ordinal holds

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

b_{2} c= A ) ) );

for X being set

for b

( b

b

theorem :: ORDINAL2:15

for D being Ordinal

for X being set st On X <> 0 & ( for A being Ordinal st A in X holds

D c= A ) holds

D c= inf X

for X being set st On X <> 0 & ( for A being Ordinal st A in X holds

D c= A ) holds

D c= inf X

proof end;

theorem Th20: :: ORDINAL2:20

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;

:: deftheorem Def4 defines Ordinal-yielding ORDINAL2:def 4 :

for f being Function holds

( f is Ordinal-yielding iff ex A being Ordinal st rng f c= A );

for f being Function holds

( f is Ordinal-yielding iff ex A being Ordinal st rng f c= A );

registration

let A be Ordinal;

coherence

for b_{1} being Sequence of A holds b_{1} is Ordinal-yielding
by RELAT_1:def 19;

end;
coherence

for b

registration
end;

scheme :: ORDINAL2:sch 4

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

provided

TSUniq1{ F

provided

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

A2: ( 0 in F_{1}() implies F_{5}() . 0 = 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 <> 0 & A is limit_ordinal holds

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

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

A6: ( 0 in F_{1}() implies F_{6}() . 0 = 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 <> 0 & A is limit_ordinal holds

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

A2: ( 0 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: ( 0 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}() -> object , F_{3}( Ordinal, set ) -> object , F_{4}( Ordinal, Sequence) -> object } :

TSExist1{ F

ex L being Sequence st

( dom L = F_{1}() & ( 0 in F_{1}() implies L . 0 = 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 <> 0 & 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}() -> Sequence, F_{2}( Ordinal) -> set , F_{3}() -> Ordinal, F_{4}() -> set , F_{5}( Ordinal, set ) -> set , F_{6}( Ordinal, Sequence) -> set } :

provided

TSResult{ F

provided

A1:
for A being Ordinal

for x being object holds

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

( x = last L & dom L = succ A & L . 0 = 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 <> 0 & C is limit_ordinal holds

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

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

A3: ( 0 in F_{3}() implies F_{1}() . 0 = 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 <> 0 & A is limit_ordinal holds

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

for x being object holds

( x = F

( x = last L & dom L = succ A & L . 0 = F

L . (succ C) = F

L . C = F

A2: dom F

A3: ( 0 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, Sequence) -> set } :

TSDef{ F

( ex x being object ex L being Sequence st

( x = last L & dom L = succ F_{1}() & L . 0 = 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 <> 0 & C is limit_ordinal holds

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

( x1 = last L & dom L = succ F_{1}() & L . 0 = 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 <> 0 & C is limit_ordinal holds

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

( x2 = last L & dom L = succ F_{1}() & L . 0 = 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 <> 0 & 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, Sequence) -> set } :

provided

TSResult0{ F

provided

A1:
for A being Ordinal

for x being object holds

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

( x = last L & dom L = succ A & L . 0 = 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 <> 0 & C is limit_ordinal holds

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

for x being object holds

( x = F

( x = last L & dom L = succ A & L . 0 = 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, Sequence) -> set , F_{4}( Ordinal) -> set } :

provided

TSResultS{ F

provided

A1:
for A being Ordinal

for x being object holds

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

( x = last L & dom L = succ A & L . 0 = 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 <> 0 & C is limit_ordinal holds

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

for x being object holds

( x = F

( x = last L & dom L = succ A & L . 0 = F

L . (succ C) = F

L . C = F

proof end;

scheme :: ORDINAL2:sch 10

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

provided

TSResultL{ F

provided

A1:
for A being Ordinal

for x being object holds

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

( x = last L & dom L = succ A & L . 0 = 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 <> 0 & C is limit_ordinal holds

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

A2: ( F_{2}() <> 0 & 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 object holds

( x = F

( x = last L & dom L = succ A & L . 0 = 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, Sequence) -> Ordinal } :

OSExist{ F

ex fi being Ordinal-Sequence st

( dom fi = F_{1}() & ( 0 in F_{1}() implies fi . 0 = 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 <> 0 & 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, 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 . 0 = 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 <> 0 & C is limit_ordinal holds

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

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

A3: ( 0 in F_{3}() implies F_{1}() . 0 = 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 <> 0 & A is limit_ordinal holds

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

( B = F

( B = last fi & dom fi = succ A & fi . 0 = F

fi . (succ C) = F

fi . C = F

A2: dom F

A3: ( 0 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, Sequence) -> Ordinal } :

OSDef{ F

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

( A = last fi & dom fi = succ F_{1}() & fi . 0 = 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 <> 0 & 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 . 0 = 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 <> 0 & 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 . 0 = 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 <> 0 & 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, 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 . 0 = 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 <> 0 & C is limit_ordinal holds

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

( B = F

( B = last fi & dom fi = succ A & fi . 0 = 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, 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 . 0 = 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 <> 0 & C is limit_ordinal holds

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

( B = F

( B = last fi & dom fi = succ A & fi . 0 = 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, 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 . 0 = 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 <> 0 & C is limit_ordinal holds

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

A2: ( F_{2}() <> 0 & 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 . 0 = 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 Sequence;

correctness

coherence

sup (rng L) is Ordinal;

;

correctness

coherence

inf (rng L) is Ordinal;

;

end;
correctness

coherence

sup (rng L) is Ordinal;

;

correctness

coherence

inf (rng L) is Ordinal;

;

definition

let L be Sequence;

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

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

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 8

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

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

for L being Sequence

for b_{2} being Ordinal holds

( b_{2} = lim_sup L iff 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))) ) ) );

for L being Sequence

for b

( b

( b

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

:: deftheorem defines lim_inf ORDINAL2:def 8 :

for L being Sequence

for b_{2} being Ordinal holds

( b_{2} = lim_inf L iff 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))) ) ) );

for L being Sequence

for b

( b

( b

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

definition

let A be Ordinal;

let fi be Ordinal-Sequence;

verum ;

end;
let fi be Ordinal-Sequence;

pred A is_limes_of fi means :Def9: :: ORDINAL2:def 9

ex B being Ordinal st

( B in dom fi & ( for C being Ordinal st B c= C & C in dom fi holds

fi . C = 0 ) ) if A = 0

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 ex B being Ordinal st

( B in dom fi & ( for C being Ordinal st B c= C & C in dom fi holds

fi . C = 0 ) ) if A = 0

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

verum ;

:: deftheorem Def9 defines is_limes_of ORDINAL2:def 9 :

for A being Ordinal

for fi being Ordinal-Sequence holds

( ( A = 0 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 = 0 ) ) ) ) & ( not A = 0 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 ) ) ) ) ) );

for A being Ordinal

for fi being Ordinal-Sequence holds

( ( A = 0 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 = 0 ) ) ) ) & ( not A = 0 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 ;

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 ;

existence

ex b

uniqueness

for b

b

proof end;

:: deftheorem Def10 defines lim ORDINAL2:def 10 :

for fi being Ordinal-Sequence st ex A being Ordinal st A is_limes_of fi holds

for b_{2} being Ordinal holds

( b_{2} = lim fi iff b_{2} is_limes_of fi );

for fi being Ordinal-Sequence st ex A being Ordinal st A is_limes_of fi holds

for b

( b

definition
end;

:: deftheorem defines lim ORDINAL2:def 11 :

for A being Ordinal

for fi being Ordinal-Sequence holds lim (A,fi) = lim (fi | A);

for A being Ordinal

for fi being Ordinal-Sequence holds lim (A,fi) = lim (fi | A);

definition

let L be Ordinal-Sequence;

end;
attr L is increasing means :: ORDINAL2:def 12

for A, B being Ordinal st A in B & B in dom L holds

L . A in L . B;

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 13

for A, B being Ordinal st A in dom L & A <> 0 & A is limit_ordinal & B = L . A holds

B is_limes_of L | A;

for A, B being Ordinal st A in dom L & A <> 0 & A is limit_ordinal & B = L . A holds

B is_limes_of L | A;

:: deftheorem defines increasing ORDINAL2:def 12 :

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

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

for L being Ordinal-Sequence holds

( L is continuous iff for A, B being Ordinal st A in dom L & A <> 0 & A is limit_ordinal & B = L . A holds

B is_limes_of L | A );

for L being Ordinal-Sequence holds

( L is continuous iff for A, B being Ordinal st A in dom L & A <> 0 & A is limit_ordinal & B = L . A holds

B is_limes_of L | A );

definition

let A, B be Ordinal;

existence

ex b_{1} being Ordinal ex fi being Ordinal-Sequence st

( b_{1} = last fi & dom fi = succ B & fi . 0 = 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 <> 0 & 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 . 0 = 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 <> 0 & 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 . 0 = 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 <> 0 & C is limit_ordinal holds

fi . C = sup (fi | C) ) ) holds

b_{1} = b_{2};

end;
func A +^ B -> Ordinal means :Def14: :: ORDINAL2:def 14

ex fi being Ordinal-Sequence st

( it = last fi & dom fi = succ B & fi . 0 = 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 <> 0 & C is limit_ordinal holds

fi . C = sup (fi | C) ) );

correctness ex fi being Ordinal-Sequence st

( it = last fi & dom fi = succ B & fi . 0 = 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 <> 0 & C is limit_ordinal holds

fi . C = sup (fi | C) ) );

existence

ex b

( b

fi . (succ C) = succ (fi . C) ) & ( for C being Ordinal st C in succ B & C <> 0 & 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 <> 0 & 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 <> 0 & C is limit_ordinal holds

fi . C = sup (fi | C) ) ) holds

b

proof end;

:: deftheorem Def14 defines +^ ORDINAL2:def 14 :

for A, B, b_{3} being Ordinal holds

( b_{3} = A +^ B iff ex fi being Ordinal-Sequence st

( b_{3} = last fi & dom fi = succ B & fi . 0 = 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 <> 0 & C is limit_ordinal holds

fi . C = sup (fi | C) ) ) );

for A, B, b

( b

( b

fi . (succ C) = succ (fi . C) ) & ( for C being Ordinal st C in succ B & C <> 0 & C is limit_ordinal holds

fi . C = sup (fi | C) ) ) );

definition

let A, B be Ordinal;

existence

ex b_{1} being Ordinal ex fi being Ordinal-Sequence st

( b_{1} = last fi & dom fi = succ A & fi . 0 = 0 & ( 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 <> 0 & 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 . 0 = 0 & ( 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 <> 0 & 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 . 0 = 0 & ( 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 <> 0 & C is limit_ordinal holds

fi . C = union (sup (fi | C)) ) ) holds

b_{1} = b_{2};

end;
func A *^ B -> Ordinal means :Def15: :: ORDINAL2:def 15

ex fi being Ordinal-Sequence st

( it = last fi & dom fi = succ A & fi . 0 = 0 & ( 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 <> 0 & C is limit_ordinal holds

fi . C = union (sup (fi | C)) ) );

correctness ex fi being Ordinal-Sequence st

( it = last fi & dom fi = succ A & fi . 0 = 0 & ( 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 <> 0 & C is limit_ordinal holds

fi . C = union (sup (fi | C)) ) );

existence

ex b

( b

fi . (succ C) = (fi . C) +^ B ) & ( for C being Ordinal st C in succ A & C <> 0 & 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 <> 0 & 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 <> 0 & C is limit_ordinal holds

fi . C = union (sup (fi | C)) ) ) holds

b

proof end;

:: deftheorem Def15 defines *^ ORDINAL2:def 15 :

for A, B, b_{3} being Ordinal holds

( b_{3} = A *^ B iff ex fi being Ordinal-Sequence st

( b_{3} = last fi & dom fi = succ A & fi . 0 = 0 & ( 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 <> 0 & C is limit_ordinal holds

fi . C = union (sup (fi | C)) ) ) );

for A, B, b

( b

( b

fi . (succ C) = (fi . C) +^ B ) & ( for C being Ordinal st C in succ A & C <> 0 & C is limit_ordinal holds

fi . C = union (sup (fi | C)) ) ) );

definition

let A, B be Ordinal;

existence

ex b_{1} being Ordinal ex fi being Ordinal-Sequence st

( b_{1} = last fi & dom fi = succ B & fi . 0 = 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 <> 0 & 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 . 0 = 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 <> 0 & 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 . 0 = 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 <> 0 & C is limit_ordinal holds

fi . C = lim (fi | C) ) ) holds

b_{1} = b_{2};

end;
func exp (A,B) -> Ordinal means :Def16: :: ORDINAL2:def 16

ex fi being Ordinal-Sequence st

( it = last fi & dom fi = succ B & fi . 0 = 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 <> 0 & C is limit_ordinal holds

fi . C = lim (fi | C) ) );

correctness ex fi being Ordinal-Sequence st

( it = last fi & dom fi = succ B & fi . 0 = 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 <> 0 & C is limit_ordinal holds

fi . C = lim (fi | C) ) );

existence

ex b

( b

fi . (succ C) = A *^ (fi . C) ) & ( for C being Ordinal st C in succ B & C <> 0 & 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 <> 0 & 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 <> 0 & C is limit_ordinal holds

fi . C = lim (fi | C) ) ) holds

b

proof end;

:: deftheorem Def16 defines exp ORDINAL2:def 16 :

for A, B, b_{3} being Ordinal holds

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

( b_{3} = last fi & dom fi = succ B & fi . 0 = 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 <> 0 & C is limit_ordinal holds

fi . C = lim (fi | C) ) ) );

for A, B, b

( b

( b

fi . (succ C) = A *^ (fi . C) ) & ( for C being Ordinal st C in succ B & C <> 0 & C is limit_ordinal holds

fi . C = lim (fi | C) ) ) );

theorem Th29: :: ORDINAL2:29

for A, B being Ordinal st B <> 0 & 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;

Lm1: 1 = succ 0

;

theorem Th37: :: ORDINAL2:37

for A, B being Ordinal st B <> 0 & 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 Th45: :: ORDINAL2:45

for A, B being Ordinal st B <> 0 & 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;

:: 2005.05.04, A.T.

:: from ZFREFLE1, 2007.03.14, A.T.

definition

let A, B be Ordinal;

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 17

ex xi being Ordinal-Sequence st

( dom xi = B & rng xi c= A & xi is increasing & A = sup xi );

reflexivity ex xi being Ordinal-Sequence st

( dom xi = B & rng xi c= A & xi is increasing & A = sup xi );

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

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

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

:: from ARYTM_3, 2007.10.23, A.T.

registration
end;

:: from AMI_2, 2008.02.14, A.T.

:: 2010.03.16, A.T.

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}() . 0 = F_{1}()
and

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

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

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

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

A7: for n being Nat

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 Nat holds P

A4: dom F

A5: F

A6: for n being Nat holds P

A7: for n being Nat

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}() . 0 = F_{1}()
and

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

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

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

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

A2: F

A3: for n being Nat holds F

A4: dom F

A5: F

A6: for n being Nat holds F

proof end;