:: Increasing and Continuous Ordinal Sequences
:: by Grzegorz Bancerek
::
:: Received May 31, 1990
:: Copyright (c) 1990-2012 Association of Mizar Users


begin

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

definition
let fi, psi be T-Sequence;
funcfi ^ psi ->  T-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 T-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 ) )
proofend;
uniqueness
 for b1, b2 being T-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
proofend;
end;

:: deftheorem Def1 defines ^ ORDINAL4:def_1_:_
 for fi, psi, b3 being T-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 ) ) );

theorem Th2: :: ORDINAL4:2
for fi, psi being Ordinal-Sequence holds rng (fi ^ psi) c= (rng fi) \/ (rng psi)
proofend;

registration
let fi, psi be Ordinal-Sequence;
clusterfi ^ psi ->  Ordinal-yielding ;
coherence
 fi ^ psi is Ordinal-yielding
proofend;
end;

theorem Th3: :: ORDINAL4:3
for psi, fi being Ordinal-Sequence
for A being Ordinal st A is_limes_of psi holds
A is_limes_of fi ^ psi
proofend;

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

Lm4:  for fi being Ordinal-Sequence
for A being Ordinal st A is_limes_of fi holds
dom fi <> {}
proofend;

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

theorem Th6: :: ORDINAL4:6
for fi, psi being Ordinal-Sequence
for B, C being Ordinal st dom fi = dom psi &amp; B is_limes_of fi &amp; C is_limes_of psi &amp; ( 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
proofend;

theorem :: ORDINAL4:7
for fi being Ordinal-Sequence
for A being Ordinal
for f1, f2 being Ordinal-Sequence st dom f1 = dom fi &amp; dom fi = dom f2 &amp; A is_limes_of f1 &amp; A is_limes_of f2 &amp; ( for A being Ordinal st A in dom fi holds
( f1 . A c= fi . A &amp; fi . A c= f2 . A ) ) holds
A is_limes_of fi
proofend;

theorem Th8: :: ORDINAL4:8
for fi being Ordinal-Sequence st dom fi <> {} &amp; dom fi is limit_ordinal &amp; fi is increasing holds
( sup fi is_limes_of fi &amp; lim fi = sup fi )
proofend;

theorem Th9: :: ORDINAL4:9
for fi being Ordinal-Sequence
for A, B being Ordinal st fi is increasing &amp; A c= B &amp; B in dom fi holds
fi . A c= fi . B
proofend;

theorem Th10: :: ORDINAL4:10
for fi being Ordinal-Sequence
for A being Ordinal st fi is increasing &amp; A in dom fi holds
A c= fi . A
proofend;

theorem Th11: :: ORDINAL4:11
for phi being Ordinal-Sequence
for A being Ordinal st phi is increasing holds
phi " A is Ordinal
proofend;

theorem Th12: :: ORDINAL4:12
for f1, f2 being Ordinal-Sequence st f1 is increasing holds
f2 * f1 is Ordinal-Sequence
proofend;

theorem Th13: :: ORDINAL4:13
for f1, f2 being Ordinal-Sequence st f1 is increasing &amp; f2 is increasing holds
ex phi being Ordinal-Sequence st
( phi = f1 * f2 &amp; phi is increasing )
proofend;

theorem Th14: :: ORDINAL4:14
for fi being Ordinal-Sequence
for A being Ordinal
for f1, f2 being Ordinal-Sequence st f1 is increasing &amp; A is_limes_of f2 &amp; sup (rng f1) = dom f2 &amp; fi = f2 * f1 holds
A is_limes_of fi
proofend;

theorem Th15: :: ORDINAL4:15
for phi being Ordinal-Sequence
for A being Ordinal st phi is increasing holds
phi | A is increasing
proofend;

theorem Th16: :: ORDINAL4:16
for phi being Ordinal-Sequence st phi is increasing &amp; dom phi is limit_ordinal holds
sup phi is limit_ordinal
proofend;

Lm5:  for f, g being Function
for X being set st rng f c= X holds
(g | X) * f = g * f
proofend;

theorem :: ORDINAL4:17
for fi, psi, phi being Ordinal-Sequence st fi is increasing &amp; fi is continuous &amp; psi is continuous &amp; phi = psi * fi holds
phi is continuous
proofend;

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

theorem Th19: :: ORDINAL4:19
for fi being Ordinal-Sequence
for C being Ordinal st C <> {} &amp; ( for A being Ordinal st A in dom fi holds
fi . A = A *^ C ) holds
fi is increasing
proofend;

theorem Th20: :: ORDINAL4:20
for A being Ordinal st A <> {} holds
exp ({},A) = {}
proofend;

Lm6:  for A being Ordinal st A <> {} &amp; A is limit_ordinal holds
for fi being Ordinal-Sequence st dom fi = A &amp; ( for B being Ordinal st B in A holds
fi . B = exp ({},B) ) holds
{} is_limes_of fi
proofend;

Lm7:  for A being Ordinal st A <> {} holds
for fi being Ordinal-Sequence st dom fi = A &amp; ( for B being Ordinal st B in A holds
fi . B = exp (1,B) ) holds
1 is_limes_of fi
proofend;

Lm8:  for C, A being Ordinal st A <> {} &amp; A is limit_ordinal holds
ex fi being Ordinal-Sequence st
( dom fi = A &amp; ( for B being Ordinal st B in A holds
fi . B = exp (C,B) ) &amp; ex D being Ordinal st D is_limes_of fi )
proofend;

theorem Th21: :: ORDINAL4:21
for A, C being Ordinal st A <> {} &amp; A is limit_ordinal holds
for fi being Ordinal-Sequence st dom fi = A &amp; ( for B being Ordinal st B in A holds
fi . B = exp (C,B) ) holds
exp (C,A) is_limes_of fi
proofend;

theorem Th22: :: ORDINAL4:22
for C, A being Ordinal st C <> {} holds
exp (C,A) <> {}
proofend;

theorem Th23: :: ORDINAL4:23
for C, A being Ordinal st 1 in C holds
exp (C,A) in exp (C,(succ A))
proofend;

theorem Th24: :: ORDINAL4:24
for C, A, B being Ordinal st 1 in C &amp; A in B holds
exp (C,A) in exp (C,B)
proofend;

theorem Th25: :: ORDINAL4:25
for fi being Ordinal-Sequence
for C being Ordinal st 1 in C &amp; ( for A being Ordinal st A in dom fi holds
fi . A = exp (C,A) ) holds
fi is increasing
proofend;

theorem :: ORDINAL4:26
for C, A being Ordinal st 1 in C &amp; A <> {} &amp; A is limit_ordinal holds
for fi being Ordinal-Sequence st dom fi = A &amp; ( for B being Ordinal st B in A holds
fi . B = exp (C,B) ) holds
exp (C,A) = sup fi
proofend;

theorem :: ORDINAL4:27
for C, A, B being Ordinal st C <> {} &amp; A c= B holds
exp (C,A) c= exp (C,B)
proofend;

theorem :: ORDINAL4:28
for A, B, C being Ordinal st A c= B holds
exp (A,C) c= exp (B,C)
proofend;

theorem :: ORDINAL4:29
for C, A being Ordinal st 1 in C &amp; A <> {} holds
1 in exp (C,A)
proofend;

theorem Th30: :: ORDINAL4:30
for C, A, B being Ordinal holds exp (C,(A +^ B)) = (exp (C,B)) *^ (exp (C,A))
proofend;

theorem :: ORDINAL4:31
for C, A, B being Ordinal holds exp ((exp (C,A)),B) = exp (C,(B *^ A))
proofend;

theorem :: ORDINAL4:32
for C, A being Ordinal st 1 in C holds
A c= exp (C,A)
proofend;

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 <> {} &amp; A is limit_ordinal holds
for phi being Ordinal-Sequence st dom phi = A &amp; ( for B being Ordinal st B in A holds
phi . B = F1(B) ) holds
F1(A) is_limes_of phi
proofend;

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

registration
let W be Universe;
cluster epsilon-transitive epsilon-connected ordinal non empty for Element of W;
existence
 not for b1 being Ordinal of W holds b1 is empty
proofend;
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 V25( On W, On W)  ->  T-Sequence-like Ordinal-yielding for Element of bool [:(On W),(On W):];
coherence
 for b1 being Ordinal-Sequence of W holds
( b1 is T-Sequence-like &amp; b1 is Ordinal-yielding )
proofend;
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)
proofend;

definition
let W be Universe;
func 0-element_of W ->  Ordinal of W equals :: ORDINAL4:def 2
 {} ;
correctness
coherence
{} is Ordinal of W;
proofend;
func 1-element_of W ->  non empty Ordinal of W equals :: ORDINAL4:def 3
1;
correctness
coherence
1 is non empty Ordinal of W;
proofend;
let phi be Ordinal-Sequence of W;
let A1 be Ordinal of W;
:: original:.
redefine funcphi . A1 ->  Ordinal of W;
coherence
 phi . A1 is Ordinal of W
proofend;
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 funcp1 * p2 ->  Ordinal-Sequence of W;
coherence
 p2 * p1 is Ordinal-Sequence of W
proofend;
end;

theorem :: ORDINAL4:33
for W being Universe holds
( 0-element_of W = {} &amp; 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 funcA1 +^ B1 ->  Ordinal of W;
coherence
 A1 +^ B1 is Ordinal of W
proofend;
end;

definition
let W be Universe;
let A1, B1 be Ordinal of W;
:: original:*^
redefine funcA1 *^ B1 ->  Ordinal of W;
coherence
 A1 *^ B1 is Ordinal of W
proofend;
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
proofend;

theorem Th35: :: ORDINAL4:35
for fi being Ordinal-Sequence
for W being Universe st dom fi in W &amp; rng fi c= W holds
sup fi in W
proofend;

theorem :: ORDINAL4:36
for W being Universe
for phi being Ordinal-Sequence of W st phi is increasing &amp; phi is continuous &amp; omega in W holds
ex A being Ordinal st
( A in dom phi &amp; phi . A = A )
proofend;

begin

theorem :: ORDINAL4:37
for A, B, C being Ordinal st A is_cofinal_with B &amp; B is_cofinal_with C holds
A is_cofinal_with C
proofend;

theorem :: ORDINAL4:38
for A, B being Ordinal st A is_cofinal_with B holds
( A is limit_ordinal iff B is limit_ordinal )
proofend;

:: from 2009.09.28, A.T.
registration
let D be Ordinal;
let f, g be T-Sequence of D;
clusterf ^ g -> D -valued ;
coherence
 f ^ g is D -valued
proofend;
end;