:: Increasing and Continuous Ordinal Sequences
:: by Grzegorz Bancerek
::
:: Copyright (c) 1990-2021 Association of Mizar Users

Lm1:
by ORDINAL1:def 11;

Lm2:
by ORDINAL1:def 11;

Lm3:
;

registration
let L be Ordinal-Sequence;
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 b1 being Sequence st
( dom b1 = (dom fi) +^ (dom psi) & ( for A being Ordinal st A in dom fi holds
b1 . A = fi . A ) & ( for A being Ordinal st A in dom psi holds
b1 . ((dom fi) +^ A) = psi . A ) )
proof end;
uniqueness
for b1, b2 being Sequence st dom b1 = (dom fi) +^ (dom psi) & ( for A being Ordinal st A in dom fi holds
b1 . A = fi . A ) & ( for A being Ordinal st A in dom psi holds
b1 . ((dom fi) +^ A) = psi . A ) & dom b2 = (dom fi) +^ (dom psi) & ( for A being Ordinal st A in dom fi holds
b2 . A = fi . A ) & ( for A being Ordinal st A in dom psi holds
b2 . ((dom fi) +^ A) = psi . A ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines ^ ORDINAL4:def 1 :
for fi, psi, b3 being Sequence holds
( b3 = fi ^ psi iff ( dom b3 = (dom fi) +^ (dom psi) & ( for A being Ordinal st A in dom fi holds
b3 . A = fi . A ) & ( for A being Ordinal st A in dom psi holds
b3 . ((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{ F1( Ordinal) -> Ordinal } :
ex A being Ordinal st F1(A) = A
provided
A1: for A, B being Ordinal st A in B holds
F1(A) in F1(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 = F1(B) ) holds
F1(A) is_limes_of phi
proof end;

registration
let W be Universe;
cluster ordinal for Element of W;
existence
ex b1 being Element of W st b1 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:
;

registration
let W be Universe;
existence
not for b1 being Ordinal of W holds b1 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 b1 being Ordinal-Sequence of W holds
( b1 is Sequence-like & b1 is Ordinal-yielding )
proof end;
end;

scheme :: ORDINAL4:sch 2
UOSLambda{ F1() -> Universe, F2( set ) -> Ordinal of F1() } :
ex phi being Ordinal-Sequence of F1() st
for a being Ordinal of F1() holds phi . a = F2(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;