:: Increasing and Continuous Ordinal Sequences
:: 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

let L be Ordinal-Sequence;

cluster last L -> ordinal ;

coherence
last L is ordinal ;

end;

theorem :: ORDINAL4:1

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

proof end;

definition

let fi, psi be Sequence;

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
ex b₁ being Sequence st
( dom b₁ = (dom fi) +^ (dom psi) & ( for A being Ordinal st A in dom fi holds
b₁ . A = fi . A ) & ( for A being Ordinal st A in dom psi holds
b₁ . ((dom fi) +^ A) = psi . A ) )

proof end;

uniqueness
for b₁, b₂ being Sequence st dom b₁ = (dom fi) +^ (dom psi) & ( for A being Ordinal st A in dom fi holds
b₁ . A = fi . A ) & ( for A being Ordinal st A in dom psi holds
b₁ . ((dom fi) +^ A) = psi . A ) & dom b₂ = (dom fi) +^ (dom psi) & ( for A being Ordinal st A in dom fi holds
b₂ . A = fi . A ) & ( for A being Ordinal st A in dom psi holds
b₂ . ((dom fi) +^ A) = psi . A ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines ^ ORDINAL4:def 1 :
for fi, psi, b₃ being Sequence holds
( b₃ = fi ^ psi iff ( dom b₃ = (dom fi) +^ (dom psi) & ( for A being Ordinal st A in dom fi holds
b₃ . A = fi . A ) & ( for A being Ordinal st A in dom psi holds
b₃ . ((dom fi) +^ A) = psi . A ) ) );

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;

theorem Th2: :: ORDINAL4:2

for A, B being Sequence holds rng (A ^ B) = (rng A) \/ (rng B)

proof end;

registration

let fi, psi be Ordinal-Sequence;

cluster fi ^ psi -> Ordinal-yielding ;

coherence
fi ^ psi is Ordinal-yielding

proof end;

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

proof end;

theorem :: ORDINAL4:4

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

proof end;

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

proof end;

theorem Th6: :: ORDINAL4:6

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

proof end;

theorem :: ORDINAL4:7

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

proof end;

theorem Th8: :: ORDINAL4:8

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

proof end;

theorem Th9: :: ORDINAL4:9

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

proof end;

theorem Th10: :: ORDINAL4:10

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

proof end;

theorem Th11: :: ORDINAL4:11

for phi being Ordinal-Sequence
for A being Ordinal st phi is increasing holds
phi " A is epsilon-transitive epsilon-connected set

proof end;

theorem Th12: :: ORDINAL4:12

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

proof end;

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

proof end;

theorem Th14: :: ORDINAL4:14

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

proof end;

theorem Th15: :: ORDINAL4:15

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

proof end;

theorem Th16: :: ORDINAL4:16

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

proof end;

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

proof end;

theorem :: ORDINAL4:18

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

proof end;

theorem Th19: :: ORDINAL4:19

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

proof end;

theorem Th20: :: ORDINAL4:20

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

proof end;

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

proof end;

theorem Th22: :: ORDINAL4:22

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

proof end;

theorem Th23: :: ORDINAL4:23

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

proof end;

theorem Th24: :: ORDINAL4:24

for A, B, C being Ordinal st 1 in C & A in B holds
exp (C,A) in exp (C,B)

proof end;

theorem Th25: :: ORDINAL4:25

for fi being Ordinal-Sequence
for C being Ordinal st 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

proof end;

theorem :: ORDINAL4:27

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

proof end;

theorem :: ORDINAL4:28

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

proof end;

theorem :: ORDINAL4:29

for A, C being Ordinal st 1 in C & A <> {} holds
1 in exp (C,A)

proof end;

theorem Th30: :: ORDINAL4:30

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

proof end;

theorem :: ORDINAL4:31

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

proof end;

theorem :: ORDINAL4:32

for A, C being Ordinal st 1 in C holds
A c= exp (C,A)

proof end;

:: Fixed-point lemma for normal functions

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

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

provided

A1: for A, B being Ordinal st A in B holds
F₁(A) in F₁(B) and
A2: for 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₁(B) ) holds
F₁(A) is_limes_of phi

proof end;

registration

let W be Universe;

cluster ordinal for Element of W;

existence
ex b₁ being Element of W st b₁ is ordinal

proof end;

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;

Lm9: 0 = {}
;

registration

let W be Universe;

cluster epsilon-transitive epsilon-connected ordinal non empty for Element of W;

existence
not for b₁ being Ordinal of W holds b₁ is empty

proof end;

end;

registration

let W be Universe;

cluster On W -> non empty ;

coherence
not On W is empty by CLASSES2:51;

end;

registration

let W be Universe;

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

coherence
for b₁ being Ordinal-Sequence of W holds
( b₁ is Sequence-like & b₁ is Ordinal-yielding )

proof end;

end;

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

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

proof end;

definition

let W be Universe;

func 0-element_of W -> Ordinal of W equals :: ORDINAL4:def 2
{} ;

correctness
coherence
{} is Ordinal of W;

proof end;

func 1-element_of W -> non empty Ordinal of W equals :: ORDINAL4:def 3
1;

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;

end;

:: deftheorem defines 0-element_of ORDINAL4:def 2 :
for W being Universe holds 0-element_of W = {} ;

:: deftheorem defines 1-element_of ORDINAL4:def 3 :
for W being Universe holds 1-element_of W = 1;

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

proof end;

end;

theorem :: ORDINAL4:33

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

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

proof end;

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

proof end;

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

proof end;

theorem Th35: :: ORDINAL4:35

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

proof end;

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

proof end;

theorem :: ORDINAL4:37

for A, B, C being Ordinal st A is_cofinal_with B & B is_cofinal_with C holds
A is_cofinal_with C

proof end;

theorem :: ORDINAL4:38

for A, B being Ordinal st A is_cofinal_with B holds
( A is limit_ordinal iff B is limit_ordinal )

proof end;

:: from 2009.09.28, A.T.

registration

let D be Ordinal;
let f, g be Sequence of D;

cluster f ^ g -> D -valued ;

coherence
f ^ g is D -valued

proof end;

end;

theorem :: ORDINAL4:39

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

theorem :: ORDINAL4:40

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