:: by Grzegorz Bancerek

::

:: Received May 31, 1990

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

Lm1: {} in omega

by ORDINAL1:def 11;

Lm2: omega is limit_ordinal

by ORDINAL1:def 11;

Lm3: 1 = succ {}

;

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

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

ex b_{1} being Sequence st

( dom b_{1} = (dom fi) +^ (dom psi) & ( for A being Ordinal st A in dom fi holds

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

b_{1} . ((dom fi) +^ A) = psi . A ) )

for b_{1}, b_{2} being Sequence st dom b_{1} = (dom fi) +^ (dom psi) & ( for A being Ordinal st A in dom fi holds

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

b_{1} . ((dom fi) +^ A) = psi . A ) & dom b_{2} = (dom fi) +^ (dom psi) & ( for A being Ordinal st A in dom fi holds

b_{2} . A = fi . A ) & ( for A being Ordinal st A in dom psi holds

b_{2} . ((dom fi) +^ A) = psi . A ) holds

b_{1} = b_{2}

end;
func fi ^ psi -> 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 ( 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 ) );

ex b

( dom b

b

b

proof end;

uniqueness for b

b

b

b

b

b

proof end;

:: deftheorem Def1 defines ^ ORDINAL4:def 1 :

for fi, psi, b_{3} being Sequence holds

( b_{3} = fi ^ psi iff ( dom b_{3} = (dom fi) +^ (dom psi) & ( for A being Ordinal st A in dom fi holds

b_{3} . A = fi . A ) & ( for A being Ordinal st A in dom psi holds

b_{3} . ((dom fi) +^ A) = psi . A ) ) );

for fi, psi, b

( b

b

b

Th2Lem: for fi, psi being Sequence holds rng (fi ^ psi) c= (rng fi) \/ (rng psi)

proof end;

Th7A: for A, B being Sequence holds rng A c= rng (A ^ B)

proof end;

Th8A: for A, B being Sequence holds rng B c= rng (A ^ B)

proof end;

registration
end;

theorem Th3: :: ORDINAL4:3

for fi, psi being Ordinal-Sequence

for A being Ordinal st A is_limes_of psi holds

A is_limes_of fi ^ psi

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

for A, B being Ordinal st A is_limes_of fi holds

B +^ A is_limes_of B +^ fi

proof end;

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

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

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

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 )

( 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

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

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 epsilon-transitive epsilon-connected set

for A being Ordinal st phi is increasing holds

phi " A is epsilon-transitive epsilon-connected set

proof end;

theorem Th13: :: 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 )

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

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 Th16: :: ORDINAL4:16

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

sup phi is limit_ordinal

sup phi is limit_ordinal

proof end;

Lm5: 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 phi, fi, psi being Ordinal-Sequence st fi is increasing & fi is continuous & psi is continuous & phi = psi * fi holds

phi is continuous

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

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

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;

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

0 is_limes_of fi

proof end;

Lm7: for A being Ordinal st A <> {} holds

for fi being Ordinal-Sequence st dom fi = A & ( for B being Ordinal st B in A holds

fi . B = exp (1,B) ) holds

1 is_limes_of fi

proof end;

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

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 Th25: :: ORDINAL4:25

for fi being Ordinal-Sequence

for C being Ordinal st 1 in C & ( for A being Ordinal st A in dom fi holds

fi . A = exp (C,A) ) holds

fi is increasing

for C being Ordinal st 1 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 A, C being Ordinal st 1 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

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;

:: Fixed-point lemma for normal functions

scheme :: ORDINAL4:sch 1

CriticalNumber{ F_{1}( Ordinal) -> Ordinal } :

provided

CriticalNumber{ F

provided

A1:
for A, B being Ordinal st A in B holds

F_{1}(A) in F_{1}(B)
and

A2: for A being Ordinal st A <> {} & A is limit_ordinal holds

for phi being Ordinal-Sequence st dom phi = A & ( for B being Ordinal st B in A holds

phi . B = F_{1}(B) ) holds

F_{1}(A) is_limes_of phi

F

A2: for A being Ordinal st A <> {} & A is limit_ordinal holds

for phi being Ordinal-Sequence st dom phi = A & ( for B being Ordinal st B in A holds

phi . B = F

F

proof end;

registration
end;

definition

let W be Universe;

mode Ordinal of W is ordinal Element of W;

mode Ordinal-Sequence of W is Function of (On W),(On W);

end;
mode Ordinal of W is ordinal Element of W;

mode Ordinal-Sequence of W is Function of (On W),(On W);

Lm9: 0 = {}

;

registration
end;

registration
end;

registration

let W be Universe;

for b_{1} being Ordinal-Sequence of W holds

( b_{1} is Sequence-like & b_{1} is Ordinal-yielding )

end;
cluster Function-like V28( On W, On W) -> Sequence-like Ordinal-yielding for Element of bool [:(On W),(On W):];

coherence for b

( b

proof end;

scheme :: ORDINAL4:sch 2

UOSLambda{ F_{1}() -> Universe, F_{2}( set ) -> Ordinal of F_{1}() } :

UOSLambda{ F

proof end;

definition

let W be Universe;

correctness

coherence

{} is Ordinal of W;

coherence

1 is non empty Ordinal of W;

let A1 be Ordinal of W;

:: original: .

redefine func phi . A1 -> Ordinal of W;

coherence

phi . A1 is Ordinal of W

end;
correctness

coherence

{} is Ordinal of W;

proof end;

correctness coherence

1 is non empty Ordinal of W;

proof end;

let phi be Ordinal-Sequence of W;let A1 be Ordinal of W;

:: original: .

redefine func phi . A1 -> Ordinal of W;

coherence

phi . A1 is Ordinal of W

proof end;

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

for W being Universe holds 0-element_of W = {} ;

for W being Universe holds 0-element_of W = {} ;

definition

let W be Universe;

let p2, p1 be Ordinal-Sequence of W;

:: original: *

redefine func p1 * p2 -> Ordinal-Sequence of W;

coherence

p2 * p1 is Ordinal-Sequence of W

end;
let p2, p1 be Ordinal-Sequence of W;

:: original: *

redefine func p1 * p2 -> Ordinal-Sequence of W;

coherence

p2 * p1 is Ordinal-Sequence of W

proof end;

definition

let W be Universe;

let A1 be Ordinal of W;

:: original: succ

redefine func succ A1 -> non empty Ordinal of W;

coherence

succ A1 is non empty Ordinal of W by CLASSES2:5;

let B1 be Ordinal of W;

:: original: +^

redefine func A1 +^ B1 -> Ordinal of W;

coherence

A1 +^ B1 is Ordinal of W

end;
let A1 be Ordinal of W;

:: original: succ

redefine func succ A1 -> non empty Ordinal of W;

coherence

succ A1 is non empty Ordinal of W by CLASSES2:5;

let B1 be Ordinal of W;

:: original: +^

redefine func A1 +^ B1 -> Ordinal of W;

coherence

A1 +^ B1 is Ordinal of W

proof end;

definition

let W be Universe;

let A1, B1 be Ordinal of W;

:: original: *^

redefine func A1 *^ B1 -> Ordinal of W;

coherence

A1 *^ B1 is Ordinal of W

end;
let A1, B1 be Ordinal of W;

:: original: *^

redefine func A1 *^ B1 -> Ordinal of W;

coherence

A1 *^ B1 is Ordinal of W

proof end;

theorem Th34: :: ORDINAL4:34

for W being Universe

for A1 being Ordinal of W

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

for A1 being Ordinal of W

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

proof end;

theorem :: ORDINAL4:36

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 )

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;

:: from 2009.09.28, A.T.

registration
end;