ORDINAL2: Sequences of Ordinal Numbers. Beginnings of Ordinal Arithmetics

:: Sequences of Ordinal Numbers. Beginnings of Ordinal Arithmetics
:: by Grzegorz Bancerek
::
:: Received July 18, 1989
:: Copyright (c) 1990-2012 Association of Mizar Users

begin

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

for A being Ordinal holds P₁[A]

provided

A1: P₁[ {} ] and
A2: for A being Ordinal st P₁[A] holds
P₁[ succ A] and
A3: for A being Ordinal st A <> {} & A is limit_ordinal & ( for B being Ordinal st B in A holds
P₁[B] ) holds
P₁[A]

proof end;

theorem Th1: :: ORDINAL2:1

for A, B being Ordinal holds
( A c= B iff succ A c= succ B )

proof end;

theorem Th2: :: ORDINAL2:2

for A being Ordinal holds union (succ A) = A

proof end;

theorem :: ORDINAL2:3

for A being Ordinal holds succ A c= bool A

proof end;

theorem :: ORDINAL2:4

{} is limit_ordinal

proof end;

theorem Th5: :: ORDINAL2:5

for A being Ordinal holds union A c= A

proof end;

definition

let L be T-Sequence;

func last L -> set equals :: ORDINAL2:def 1
L . (union (dom L));

end;

:: deftheorem defines last ORDINAL2:def 1 :

theorem :: ORDINAL2:6

for A being Ordinal
for L being T-Sequence st dom L = succ A holds
last L = L . A by Th2;

theorem :: ORDINAL2:7

for X being set holds On X c= X

proof end;

theorem Th8: :: ORDINAL2:8

for A being Ordinal holds On A = A

proof end;

theorem Th9: :: ORDINAL2:9

for X, Y being set st X c= Y holds
On X c= On Y

proof end;

theorem :: ORDINAL2:10

for X being set holds Lim X c= X

proof end;

theorem :: ORDINAL2:11

for X, Y being set st X c= Y holds
Lim X c= Lim Y

proof end;

theorem :: ORDINAL2:12

for X being set holds Lim X c= On X

proof end;

theorem Th13: :: ORDINAL2:13

for X being set st ( for x being set st x in X holds
x is Ordinal ) holds
meet X is Ordinal

proof end;

registration

cluster epsilon-transitive epsilon-connected ordinal limit_ordinal for set ;

proof end;

end;

definition

let X be set ;

func inf X -> Ordinal equals :: ORDINAL2:def 2
meet (On X);

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

proof end;

proof end;

end;

:: deftheorem defines inf ORDINAL2:def 2 :

:: deftheorem Def3 defines sup ORDINAL2:def 3 :

theorem :: ORDINAL2:14

for A being Ordinal
for X being set st A in X holds
inf X c= A

proof end;

theorem :: ORDINAL2:15

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

proof end;

theorem :: ORDINAL2:16

for A being Ordinal
for X, Y being set st A in X & X c= Y holds
inf Y c= inf X

proof end;

theorem :: ORDINAL2:17

for A being Ordinal
for X being set st A in X holds
inf X in X

proof end;

theorem Th18: :: ORDINAL2:18

for A being Ordinal holds sup A = A

proof end;

theorem Th19: :: ORDINAL2:19

for A being Ordinal
for X being set st A in X holds
A in sup 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

proof end;

theorem :: ORDINAL2:21

for A being Ordinal
for X being set st A in sup X holds
ex B being Ordinal st
( B in X & A c= B )

proof end;

theorem :: ORDINAL2:22

for X, Y being set st X c= Y holds
sup X c= sup Y

proof end;

theorem :: ORDINAL2:23

for A being Ordinal holds sup {A} = succ A

proof end;

theorem :: ORDINAL2:24

for X being set holds inf X c= sup X

proof end;

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

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

proof end;

definition

let f be Function;

attr f is Ordinal-yielding means :Def4: :: ORDINAL2:def 4
ex A being Ordinal st rng f c= A;

end;

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

registration

cluster T-Sequence-like Relation-like Function-like Ordinal-yielding for set ;

proof end;

end;

definition

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

end;

registration

let A be Ordinal;

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

proof end;

end;

registration

let L be Ordinal-Sequence;
let A be Ordinal;

cluster L | A -> Ordinal-yielding ;

proof end;

end;

theorem Th25: :: ORDINAL2:25

for A being Ordinal
for fi being Ordinal-Sequence st A in dom fi holds
fi . A is Ordinal

proof end;

registration

let f be Ordinal-Sequence;
let a be Ordinal;

cluster f . a -> ordinal ;

proof end;

end;

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

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

proof end;

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

F₅() = F₆()

provided

A1: dom F₅() = F₁() and
A2: ( {} in F₁() implies F₅() . {} = F₂() ) and
A3: for A being Ordinal st succ A in F₁() holds
F₅() . (succ A) = F₃(A,(F₅() . A)) and
A4: for A being Ordinal st A in F₁() & A <> {} & A is limit_ordinal holds
F₅() . A = F₄(A,(F₅() | A)) and
A5: dom F₆() = F₁() and
A6: ( {} in F₁() implies F₆() . {} = F₂() ) and
A7: for A being Ordinal st succ A in F₁() holds
F₆() . (succ A) = F₃(A,(F₆() . A)) and
A8: for A being Ordinal st A in F₁() & A <> {} & A is limit_ordinal holds
F₆() . A = F₄(A,(F₆() | A))

proof end;

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

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

proof end;

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

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

provided

A1: for A being Ordinal
for x being set holds
( x = F₂(A) iff ex L being T-Sequence st
( x = last L & dom L = succ A & L . {} = F₄() & ( for C being Ordinal st succ C in succ A holds
L . (succ C) = F₅(C,(L . C)) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
L . C = F₆(C,(L | C)) ) ) ) and
A2: dom F₁() = F₃() and
A3: ( {} in F₃() implies F₁() . {} = F₄() ) and
A4: for A being Ordinal st succ A in F₃() holds
F₁() . (succ A) = F₅(A,(F₁() . A)) and
A5: for A being Ordinal st A in F₃() & A <> {} & A is limit_ordinal holds
F₁() . A = F₆(A,(F₁() | A))

proof end;

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

( ex x being set ex L being T-Sequence st
( x = last L & dom L = succ F₁() & L . {} = F₂() & ( for C being Ordinal st succ C in succ F₁() holds
L . (succ C) = F₃(C,(L . C)) ) & ( for C being Ordinal st C in succ F₁() & C <> {} & C is limit_ordinal holds
L . C = F₄(C,(L | C)) ) ) & ( for x1, x2 being set st ex L being T-Sequence st
( x1 = last L & dom L = succ F₁() & L . {} = F₂() & ( for C being Ordinal st succ C in succ F₁() holds
L . (succ C) = F₃(C,(L . C)) ) & ( for C being Ordinal st C in succ F₁() & C <> {} & C is limit_ordinal holds
L . C = F₄(C,(L | C)) ) ) & ex L being T-Sequence st
( x2 = last L & dom L = succ F₁() & L . {} = F₂() & ( for C being Ordinal st succ C in succ F₁() holds
L . (succ C) = F₃(C,(L . C)) ) & ( for C being Ordinal st C in succ F₁() & C <> {} & C is limit_ordinal holds
L . C = F₄(C,(L | C)) ) ) holds
x1 = x2 ) )

proof end;

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

F₁({}) = F₂()

provided

A1: for A being Ordinal
for x being set holds
( x = F₁(A) iff ex L being T-Sequence st
( x = last L & dom L = succ A & L . {} = F₂() & ( for C being Ordinal st succ C in succ A holds
L . (succ C) = F₃(C,(L . C)) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
L . C = F₄(C,(L | C)) ) ) )

proof end;

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

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

provided

A1: for A being Ordinal
for x being set holds
( x = F₄(A) iff ex L being T-Sequence st
( x = last L & dom L = succ A & L . {} = F₁() & ( for C being Ordinal st succ C in succ A holds
L . (succ C) = F₂(C,(L . C)) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
L . C = F₃(C,(L | C)) ) ) )

proof end;

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

A1: for A being Ordinal
for x being set holds
( x = F₃(A) iff ex L being T-Sequence st
( x = last L & dom L = succ A & L . {} = F₄() & ( for C being Ordinal st succ C in succ A holds
L . (succ C) = F₅(C,(L . C)) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
L . C = F₆(C,(L | C)) ) ) ) and
A2: ( F₂() <> {} & F₂() is limit_ordinal ) and
A3: dom F₁() = F₂() and
A4: for A being Ordinal st A in F₂() holds
F₁() . A = F₃(A)

proof end;

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

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

proof end;

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

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

provided

A1: for A, B being Ordinal holds
( B = F₂(A) iff ex fi being Ordinal-Sequence st
( B = last fi & dom fi = succ A & fi . {} = F₄() & ( for C being Ordinal st succ C in succ A holds
fi . (succ C) = F₅(C,(fi . C)) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
fi . C = F₆(C,(fi | C)) ) ) ) and
A2: dom F₁() = F₃() and
A3: ( {} in F₃() implies F₁() . {} = F₄() ) and
A4: for A being Ordinal st succ A in F₃() holds
F₁() . (succ A) = F₅(A,(F₁() . A)) and
A5: for A being Ordinal st A in F₃() & A <> {} & A is limit_ordinal holds
F₁() . A = F₆(A,(F₁() | A))

proof end;

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

( ex A being Ordinal ex fi being Ordinal-Sequence st
( A = last fi & dom fi = succ F₁() & fi . {} = F₂() & ( for C being Ordinal st succ C in succ F₁() holds
fi . (succ C) = F₃(C,(fi . C)) ) & ( for C being Ordinal st C in succ F₁() & C <> {} & C is limit_ordinal holds
fi . C = F₄(C,(fi | C)) ) ) & ( for A1, A2 being Ordinal st ex fi being Ordinal-Sequence st
( A1 = last fi & dom fi = succ F₁() & fi . {} = F₂() & ( for C being Ordinal st succ C in succ F₁() holds
fi . (succ C) = F₃(C,(fi . C)) ) & ( for C being Ordinal st C in succ F₁() & C <> {} & C is limit_ordinal holds
fi . C = F₄(C,(fi | C)) ) ) & ex fi being Ordinal-Sequence st
( A2 = last fi & dom fi = succ F₁() & fi . {} = F₂() & ( for C being Ordinal st succ C in succ F₁() holds
fi . (succ C) = F₃(C,(fi . C)) ) & ( for C being Ordinal st C in succ F₁() & C <> {} & C is limit_ordinal holds
fi . C = F₄(C,(fi | C)) ) ) holds
A1 = A2 ) )

proof end;

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

F₁({}) = F₂()

provided

A1: for A, B being Ordinal holds
( B = F₁(A) iff ex fi being Ordinal-Sequence st
( B = last fi & dom fi = succ A & fi . {} = F₂() & ( for C being Ordinal st succ C in succ A holds
fi . (succ C) = F₃(C,(fi . C)) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
fi . C = F₄(C,(fi | C)) ) ) )

proof end;

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

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

provided

A1: for A, B being Ordinal holds
( B = F₄(A) iff ex fi being Ordinal-Sequence st
( B = last fi & dom fi = succ A & fi . {} = F₁() & ( for C being Ordinal st succ C in succ A holds
fi . (succ C) = F₂(C,(fi . C)) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
fi . C = F₃(C,(fi | C)) ) ) )

proof end;

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

A1: for A, B being Ordinal holds
( B = F₃(A) iff ex fi being Ordinal-Sequence st
( B = last fi & dom fi = succ A & fi . {} = F₄() & ( for C being Ordinal st succ C in succ A holds
fi . (succ C) = F₅(C,(fi . C)) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
fi . C = F₆(C,(fi | C)) ) ) ) and
A2: ( F₂() <> {} & F₂() is limit_ordinal ) and
A3: dom F₁() = F₂() and
A4: for A being Ordinal st A in F₂() holds
F₁() . A = F₃(A)

proof end;

definition

let L be T-Sequence;

func sup L -> Ordinal equals :: ORDINAL2:def 5
sup (rng L);

func inf L -> Ordinal equals :: ORDINAL2:def 6
inf (rng L);

end;

:: deftheorem defines sup ORDINAL2:def 5 :

:: deftheorem defines inf ORDINAL2:def 6 :

theorem :: ORDINAL2:26

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

definition

let L be T-Sequence;

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

proof end;

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

proof end;

proof end;

end;

:: deftheorem defines lim_sup ORDINAL2:def 7 :

:: deftheorem defines lim_inf ORDINAL2:def 8 :

definition

let A be Ordinal;
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 = {} ) ) 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 ) ) );

end;

:: deftheorem Def9 defines is_limes_of ORDINAL2:def 9 :

definition

let fi be Ordinal-Sequence;
given A being Ordinal such that A1: A is_limes_of fi ;

func lim fi -> Ordinal means :Def10: :: ORDINAL2:def 10
it is_limes_of fi;

existence by A1;
uniqueness

proof end;

end;

:: deftheorem Def10 defines lim ORDINAL2:def 10 :

definition

let A be Ordinal;
let fi be Ordinal-Sequence;

func lim (A,fi) -> Ordinal equals :: ORDINAL2:def 11
lim (fi | A);

end;

:: deftheorem defines lim ORDINAL2:def 11 :

definition

let L be Ordinal-Sequence;

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;

attr L is continuous means :: ORDINAL2:def 13
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;

:: deftheorem defines increasing ORDINAL2:def 12 :

:: deftheorem defines continuous ORDINAL2:def 13 :

definition

let A, B be Ordinal;

func A +^ B -> Ordinal means :Def14: :: ORDINAL2:def 14
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) ) );

proof end;

end;

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

definition

let A, B be Ordinal;

func A *^ B -> Ordinal means :Def15: :: ORDINAL2:def 15
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)) ) );

proof end;

end;

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

registration

let O be Ordinal;

cluster -> ordinal for Element of O;

end;

definition

let A, B be Ordinal;

func exp (A,B) -> Ordinal means :Def16: :: ORDINAL2:def 16
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) ) );

proof end;

end;

:: deftheorem Def16 defines exp ORDINAL2:def 16 :

theorem Th27: :: ORDINAL2:27

for A being Ordinal holds A +^ {} = A

proof end;

theorem Th28: :: ORDINAL2:28

for A, B being Ordinal holds A +^ (succ B) = succ (A +^ B)

proof end;

theorem Th29: :: ORDINAL2:29

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

proof end;

theorem Th30: :: ORDINAL2:30

for A being Ordinal holds {} +^ A = A

proof end;

Lm1: 1 = succ {}
;

theorem :: ORDINAL2:31

for A being Ordinal holds A +^ 1 = succ A

proof end;

theorem Th32: :: ORDINAL2:32

for A, B, C being Ordinal st A in B holds
C +^ A in C +^ B

proof end;

theorem Th33: :: ORDINAL2:33

for A, B, C being Ordinal st A c= B holds
C +^ A c= C +^ B

proof end;

theorem Th34: :: ORDINAL2:34

for A, B, C being Ordinal st A c= B holds
A +^ C c= B +^ C

proof end;

theorem Th35: :: ORDINAL2:35

for A being Ordinal holds {} *^ A = {}

proof end;

theorem Th36: :: ORDINAL2:36

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

proof end;

theorem Th37: :: ORDINAL2:37

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)

proof end;

theorem Th38: :: ORDINAL2:38

for A being Ordinal holds A *^ {} = {}

proof end;

theorem Th39: :: ORDINAL2:39

for A being Ordinal holds
( 1 *^ A = A & A *^ 1 = A )

proof end;

theorem Th40: :: ORDINAL2:40

for C, A, B being Ordinal st C <> {} & A in B holds
A *^ C in B *^ C

proof end;

theorem :: ORDINAL2:41

for A, B, C being Ordinal st A c= B holds
A *^ C c= B *^ C

proof end;

theorem :: ORDINAL2:42

for A, B, C being Ordinal st A c= B holds
C *^ A c= C *^ B

proof end;

theorem Th43: :: ORDINAL2:43

for A being Ordinal holds exp (A,{}) = 1

proof end;

theorem Th44: :: ORDINAL2:44

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

proof end;

theorem Th45: :: ORDINAL2:45

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

proof end;

theorem :: ORDINAL2:46

for A being Ordinal holds
( exp (A,1) = A & exp (1,A) = 1 )

proof end;

theorem :: ORDINAL2:47

for A being Ordinal ex B, C being Ordinal st
( B is limit_ordinal & C is natural & A = B +^ C )

proof end;

:: 2005.05.04, A.T.

registration

let X be set ;
let o be Ordinal;

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

proof end;

end;

registration

let O be Ordinal;
let x be set ;

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

proof end;

end;

:: from ZFREFLE1, 2007.03.14, A.T.

definition

let A, B be Ordinal;

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

proof end;

end;

:: deftheorem defines is_cofinal_with ORDINAL2:def 17 :

theorem Th48: :: ORDINAL2:48

for psi being Ordinal-Sequence
for e being set st e in rng psi holds
e is Ordinal

proof end;

theorem :: ORDINAL2:49

for psi being Ordinal-Sequence holds rng psi c= sup psi

proof end;

theorem :: ORDINAL2:50

for A being Ordinal st A is_cofinal_with {} holds
A = {}

proof end;

:: from ARYTM_3, 2007.10.23, A.T.

scheme :: ORDINAL2:sch 17
OmegaInd{ F₁() -> Nat, P₁[ set ] } :

P₁[F₁()]

provided

A1: P₁[ {} ] and
A2: for a being Nat st P₁[a] holds
P₁[ succ a]

proof end;

registration

let a, b be Nat;

cluster a +^ b -> natural ;

proof end;

end;

:: from AMI_2, 2008.02.14, A.T.

registration

let x, y be set ;
let a, b be Nat;

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

proof end;

end;

:: 2010.03.16, A.T.

scheme :: ORDINAL2:sch 18
LambdaRecEx{ F₁() -> set , F₂( set , set ) -> set } :

ex f being Function st
( dom f = omega & f . {} = F₁() & ( for n being Nat holds f . (succ n) = F₂(n,(f . n)) ) )

proof end;

scheme :: ORDINAL2:sch 19
RecUn{ F₁() -> set , F₂() -> Function, F₃() -> Function, P₁[ set , set , set ] } :

F₂() = F₃()

provided

A1: dom F₂() = omega and
A2: F₂() . {} = F₁() and
A3: for n being Nat holds P₁[n,F₂() . n,F₂() . (succ n)] and
A4: dom F₃() = omega and
A5: F₃() . {} = F₁() and
A6: for n being Nat holds P₁[n,F₃() . n,F₃() . (succ n)] and
A7: for n being Nat
for x, y1, y2 being set st P₁[n,x,y1] & P₁[n,x,y2] holds
y1 = y2

proof end;

scheme :: ORDINAL2:sch 20
LambdaRecUn{ F₁() -> set , F₂( set , set ) -> set , F₃() -> Function, F₄() -> Function } :

F₃() = F₄()

provided

A1: dom F₃() = omega and
A2: F₃() . {} = F₁() and
A3: for n being Nat holds F₃() . (succ n) = F₂(n,(F₃() . n)) and
A4: dom F₄() = omega and
A5: F₄() . {} = F₁() and
A6: for n being Nat holds F₄() . (succ n) = F₂(n,(F₄() . n))

proof end;