:: Sequences of Ordinal Numbers. Beginnings of Ordinal Arithmetics
:: by Grzegorz Bancerek
::
:: Received July 18, 1989
:: Copyright (c) 1990-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies ORDINAL1, FUNCT_1, XBOOLE_0, TARSKI, ZFMISC_1, RELAT_1, SETFAM_1,
SUBSET_1, FUNCOP_1, ORDINAL2, NAT_1, CARD_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1,
SETFAM_1, FUNCOP_1;
constructors SETFAM_1, ORDINAL1, FUNCOP_1;
registrations SUBSET_1, FUNCT_1, ORDINAL1, FUNCOP_1;
requirements SUBSET, BOOLE, NUMERALS;
definitions ORDINAL1, TARSKI, XBOOLE_0;
equalities ORDINAL1, XBOOLE_0;
expansions ORDINAL1, TARSKI, XBOOLE_0;
theorems TARSKI, ORDINAL1, SETFAM_1, ZFMISC_1, FUNCT_1, RELAT_1, XBOOLE_1,
FUNCOP_1, XTUPLE_0;
schemes XBOOLE_0, FUNCT_1, ORDINAL1;
begin
reserve A,A1,A2,B,C,D for Ordinal,
X,Y for set,
x,y,a,b,c for object,
L,L1,L2,L3 for Sequence,
f for Function;
scheme
OrdinalInd { P[Ordinal] } : for A holds P[A]
provided
A1: P[0] and
A2: for A st P[A] holds P[succ A] and
A3: for A st A <> 0 & A is limit_ordinal & for B st B in A holds P[B]
holds P[A]
proof
A4: for A st for B st B in A holds P[B] holds P[A]
proof
let A such that
A5: for B st B in A holds P[B];
A6: A <> 0 & (for B holds A <> succ B) implies thesis by A3,A5,ORDINAL1:29;
now
given B such that
A7: A = succ B;
B in A by A7,ORDINAL1:6;
hence thesis by A2,A5,A7;
end;
hence thesis by A1,A6;
end;
thus for A holds P[A] from ORDINAL1:sch 2(A4);
end;
theorem Th1:
A c= B iff succ A c= succ B
proof
A c= B iff A in succ B by ORDINAL1:22;
hence thesis by ORDINAL1:21;
end;
theorem Th2:
union succ A = A
proof
thus union succ A c= A
proof
let x be object;
assume x in union succ A;
then consider X such that
A1: x in X and
A2: X in succ A by TARSKI:def 4;
reconsider X as Ordinal by A2;
X c= A by A2,ORDINAL1:22;
hence thesis by A1;
end;
thus thesis by ORDINAL1:6,ZFMISC_1:74;
end;
theorem
succ A c= bool A
proof
let x be object;
assume
A1: x in succ A;
then reconsider B = x as Ordinal;
x in A or x = A by A1,ORDINAL1:8;
then B c= A by ORDINAL1:def 2;
hence thesis;
end;
theorem
0 is limit_ordinal
by ZFMISC_1:2;
theorem Th5:
union A c= A
proof
let x be object;
assume x in union A;
then consider Y such that
A1: x in Y and
A2: Y in A by TARSKI:def 4;
Y c= A by A2,ORDINAL1:def 2;
hence thesis by A1;
end;
definition
let L;
func last L -> set equals
L.(union dom L);
coherence;
end;
theorem
dom L = succ A implies last L = L.A by Th2;
theorem
On X c= X
by ORDINAL1:def 9;
theorem Th8:
On A = A
proof
for x being object holds x in A iff x in A & x is Ordinal;
hence thesis by ORDINAL1:def 9;
end;
theorem Th9:
X c= Y implies On X c= On Y
proof
assume
A1: X c= Y;
let x be object;
assume x in On X;
then x in X & x is Ordinal by ORDINAL1:def 9;
hence thesis by A1,ORDINAL1:def 9;
end;
theorem
Lim X c= X
by ORDINAL1:def 10;
theorem
X c= Y implies Lim X c= Lim Y
proof
assume
A1: X c= Y;
let x be object;
assume x in Lim X;
then x in X & ex A st x = A & A is limit_ordinal by ORDINAL1:def 10;
hence thesis by A1,ORDINAL1:def 10;
end;
theorem
Lim X c= On X
proof
let x be object;
assume x in Lim X;
then x in X & ex A st x = A & A is limit_ordinal by ORDINAL1:def 10;
hence thesis by ORDINAL1:def 9;
end;
theorem Th13:
(for x st x in X holds x is Ordinal) implies meet X is Ordinal
proof
assume
A1: for x st x in X holds x is Ordinal;
now
defpred P[Ordinal] means $1 in X;
set x = the Element of X;
assume
A2: X <> 0;
then x is Ordinal by A1;
then
A3: ex A st P[A] by A2;
consider A such that
A4: P[A] & for B st P[B] holds A c= B from ORDINAL1:sch 1(A3);
for x being object holds x in A iff for Y st Y in X holds x in Y
proof
let x be object;
thus x in A implies for Y st Y in X holds x in Y
proof
assume
A5: x in A;
let Y;
assume
A6: Y in X;
then reconsider B = Y as Ordinal by A1;
A c= B by A4,A6;
hence thesis by A5;
end;
assume for Y st Y in X holds x in Y;
hence thesis by A4;
end;
hence thesis by A2,SETFAM_1:def 1;
end;
hence thesis by SETFAM_1:def 1;
end;
registration
cluster limit_ordinal for Ordinal;
existence
proof
take omega;
thus thesis by ORDINAL1:def 11;
end;
end;
definition
let X;
func inf X -> Ordinal equals
meet On X;
coherence
proof
x in On X implies x is Ordinal by ORDINAL1:def 9;
hence thesis by Th13;
end;
func sup X -> Ordinal means
:Def3:
On X c= it & for A st On X c= A holds it c= A;
existence
proof
defpred P[Ordinal] means On X c= $1;
x in On X implies x is Ordinal by ORDINAL1:def 9;
then reconsider A = union On X as epsilon-transitive epsilon-connected set
by ORDINAL1:23;
On X c= succ A
proof
let x be object;
assume
A1: x in On X;
then reconsider B = x as Ordinal by ORDINAL1:def 9;
B c= A by A1,ZFMISC_1:74;
hence thesis by ORDINAL1:22;
end;
then
A2: ex A st P[A];
thus ex F being Ordinal st P[F] & for A st P[A] holds F c= A from ORDINAL1
:sch 1(A2);
end;
uniqueness;
end;
theorem
A in X implies inf X c= A
proof
assume A in X;
then A in On X by ORDINAL1:def 9;
hence thesis by SETFAM_1:3;
end;
theorem
On X <> 0 & (for A st A in X holds D c= A) implies D c= inf X
proof
assume that
A1: On X <> 0 and
A2: for A st A in X holds D c= A;
let x be object such that
A3: x in D;
for Y st Y in On X holds x in Y
proof
let Y;
assume
A4: Y in On X;
then reconsider A = Y as Ordinal by ORDINAL1:def 9;
A in X by A4,ORDINAL1:def 9;
then D c= A by A2;
hence thesis by A3;
end;
hence thesis by A1,SETFAM_1:def 1;
end;
theorem
A in X & X c= Y implies inf Y c= inf X
proof
assume A in X;
then
A1: On X <> 0 by ORDINAL1:def 9;
assume X c= Y;
then On X c= On Y by Th9;
hence thesis by A1,SETFAM_1:6;
end;
theorem
A in X implies inf X in X
proof
defpred P[Ordinal] means $1 in X;
assume A in X;
then
A1: ex A st P[A];
consider A such that
A2: P[A] & for B st P[B] holds A c= B from ORDINAL1:sch 1(A1);
A3: A in On X by A2,ORDINAL1:def 9;
A4: now
let x be object;
thus x in A implies for Y st Y in On X holds x in Y
proof
assume
A5: x in A;
let Y;
assume
A6: Y in On X;
then reconsider B = Y as Ordinal by ORDINAL1:def 9;
Y in X by A6,ORDINAL1:def 9;
then A c= B by A2;
hence thesis by A5;
end;
assume for Y st Y in On X holds x in Y;
hence x in A by A3;
end;
On X <> 0 by A2,ORDINAL1:def 9;
hence thesis by A2,A4,SETFAM_1:def 1;
end;
theorem Th18:
sup A = A
proof
On A = A & for B st On A c= B holds A c= B by Th8;
hence thesis by Def3;
end;
theorem Th19:
A in X implies A in sup X
proof
assume A in X;
then
A1: A in On X by ORDINAL1:def 9;
On X c= sup X by Def3;
hence thesis by A1;
end;
theorem Th20:
(for A st A in X holds A in D) implies sup X c= D
proof
assume
A1: for A st A in X holds A in D;
On X c= D
proof
let x be object;
assume
A2: x in On X;
then reconsider A = x as Ordinal by ORDINAL1:def 9;
A in X by A2,ORDINAL1:def 9;
hence thesis by A1;
end;
hence thesis by Def3;
end;
theorem
A in sup X implies ex B st B in X & A c= B
proof
assume that
A1: A in sup X and
A2: for B st B in X holds not A c= B;
for B st B in X holds B in A by A2,ORDINAL1:16;
then sup X c= A by Th20;
hence contradiction by A1,ORDINAL1:5;
end;
theorem
X c= Y implies sup X c= sup Y
proof
assume X c= Y;
then
A1: On X c= On Y by Th9;
On Y c= sup Y by Def3;
then On X c= sup Y by A1;
hence thesis by Def3;
end;
theorem
sup { A } = succ A
proof
A1: On { A } c= succ A
proof
let x be object;
assume x in On { A };
then x in { A } by ORDINAL1:def 9;
then x = A by TARSKI:def 1;
hence thesis by ORDINAL1:6;
end;
now
A in { A } by TARSKI:def 1;
then
A2: A in On { A } by ORDINAL1:def 9;
let B;
assume On { A } c= B;
hence succ A c= B by A2,ORDINAL1:21;
end;
hence thesis by A1,Def3;
end;
theorem
inf X c= sup X
proof
let x be object;
set y = the Element of On X;
assume
A1: x in inf X;
then reconsider y as Ordinal by ORDINAL1:def 9,SETFAM_1:1;
On X c= sup X by Def3;
then y in sup X by A1,SETFAM_1:1;
then
A2: y c= sup X by ORDINAL1:def 2;
x in y by A1,SETFAM_1:1,def 1;
hence thesis by A2;
end;
scheme
TSLambda { A()->Ordinal, F(Ordinal)->set } : ex L st dom L = A() & for A st
A in A() holds L.A = F(A) proof
deffunc G(object) = F(sup union { $1 });
consider f such that
A1: dom f = A() & for x being object st x in A() holds f.x = G(x)
from FUNCT_1:sch 3;
reconsider f as Sequence by A1,ORDINAL1:def 7;
take L = f;
thus dom L = A() by A1;
let A;
assume A in A();
hence L.A = F(sup union { A }) by A1
.= F(sup A) by ZFMISC_1:25
.= F(A) by Th18;
end;
definition
let f;
attr f is Ordinal-yielding means
:Def4:
ex A st rng f c= A;
end;
registration
cluster Ordinal-yielding for Sequence;
existence
proof
set A = the Ordinal;
set L = the Sequence of A;
take L,A;
thus thesis by RELAT_1:def 19;
end;
end;
definition
mode Ordinal-Sequence is Ordinal-yielding Sequence;
end;
registration
let A;
cluster -> Ordinal-yielding for Sequence of A;
coherence by RELAT_1:def 19;
end;
registration
let L be Ordinal-Sequence;
let A;
cluster L|A -> Ordinal-yielding;
coherence
proof
consider B such that
A1: rng L c= B by Def4;
L|A is Ordinal-yielding
proof
take B;
rng(L|A) c= rng L by RELAT_1:70;
hence thesis by A1;
end;
hence thesis;
end;
end;
reserve fi,psi for Ordinal-Sequence;
theorem Th25:
A in dom fi implies fi.A is Ordinal
proof
assume A in dom fi;
then
A1: fi.A in rng fi by FUNCT_1:def 3;
ex B st rng fi c= B by Def4;
hence thesis by A1;
end;
registration
let f be Ordinal-Sequence, a be object;
cluster f.a -> ordinal;
coherence
proof
a in dom f or not a in dom f;
hence thesis by Th25,FUNCT_1:def 2;
end;
end;
scheme
OSLambda { A()->Ordinal, F(Ordinal)->Ordinal } : ex fi st dom fi = A() & for
A st A in A() holds fi.A = F(A) proof
consider L such that
A1: dom L = A() & for A st A in A() holds L.A = F(A) from TSLambda;
L is Ordinal-yielding
proof
take sup rng L;
let x be object;
assume
A2: x in rng L;
then consider y being object such that
A3: y in dom L and
A4: x = L.y by FUNCT_1:def 3;
reconsider y as Ordinal by A3;
L.y = F(y) by A1,A3;
then
A5: x in On rng L by A2,A4,ORDINAL1:def 9;
On rng L c= sup rng L by Def3;
hence thesis by A5;
end;
then reconsider L as Ordinal-Sequence;
take fi = L;
thus dom fi = A() by A1;
let A;
assume A in A();
hence thesis by A1;
end;
scheme
TSUniq1 { A()->Ordinal, B()->object, C(Ordinal,set)->object,
D(Ordinal,Sequence)->object, L1()->Sequence, L2()->Sequence } :
L1() = L2()
provided
A1: dom L1() = A() and
A2: 0 in A() implies L1().0 = B() and
A3: for A st succ A in A() holds L1().(succ A) = C(A,L1().A) and
A4: for A st A in A() & A <> 0 & A is limit_ordinal holds L1().A = D(A,
L1()|A) and
A5: dom L2() = A() and
A6: 0 in A() implies L2().0 = B() and
A7: for A st succ A in A() holds L2().(succ A) = C(A,L2().A) and
A8: for A st A in A() & A <> 0 & A is limit_ordinal holds L2().A = D(A,
L2()|A)
proof
defpred P[object] means L1().$1 <> L2().$1;
consider X such that
A9: for Y being object holds Y in X iff Y in A() & P[Y] from XBOOLE_0:sch 1;
for b being object holds b in X implies b in A() by A9;
then
A10: X c= A();
assume L1() <> L2();
then ex a being object st a in A() & L1().a <> L2().a by A1,A5,FUNCT_1:2;
then X <> 0 by A9;
then consider B such that
A11: B in X and
A12: for C st C in X holds B c= C by A10,ORDINAL1:20;
A13: B in A() by A9,A11;
then
A14: B c= A() by ORDINAL1:def 2;
then
A15: dom(L1()|B) = B & dom(L2()|B) = B by A1,A5,RELAT_1:62;
A16: now
let C;
assume
A17: C in B;
then not C in X by A12,ORDINAL1:5;
hence L1().C = L2().C by A9,A14,A17;
end;
A18: now
let a be object;
assume
A19: a in B;
L1()|B.a = L1().a & L2()|B.a = L2().a by A15,A19,FUNCT_1:47;
hence L1()|B.a = L2()|B.a by A16,A19;
end;
A20: now
given C such that
A21: B = succ C;
A22: L1().C = L1()|B.C & L2().C = L2()|B.C by A21,FUNCT_1:49,ORDINAL1:6;
L1().B = C(C,L1().C) & L2().B = C(C,L2().C) by A3,A7,A13,A21;
hence L1().B = L2().B by A18,A21,A22,ORDINAL1:6;
end;
now
assume that
A23: B <> 0 and
A24: for C holds B <> succ C;
B is limit_ordinal by A24,ORDINAL1:29;
then L1().B = D(B,L1()|B) & L2().B = D(B,L2()|B) by A4,A8,A13,A23;
hence L1().B = L2().B by A15,A18,FUNCT_1:2;
end;
hence contradiction by A2,A6,A9,A11,A20;
end;
scheme
TSExist1 { A()->Ordinal, B()->object, C(Ordinal,set)->object,
D(Ordinal,Sequence)->object } :
ex L st dom L = A() & (0 in A() implies L.0 = B() ) & (for A st
succ A in A() holds L.(succ A) = C(A,L.A) ) & for A st A in A() & A <> 0 & A
is limit_ordinal holds L.A = D(A,L|A);
defpred P[Ordinal,Sequence] means dom $2 = $1 & (0 in $1 implies $2.0 =
B() ) & (for A1 st succ A1 in $1 holds $2.(succ A1) = C(A1,$2.A1) ) &
for A1 st A1 in $1 & A1 <> 0 & A1 is limit_ordinal holds $2.A1 = D(A1,$2|A1);
defpred R[Ordinal] means ex L st P[$1,L];
A1: for B st for C st C in B holds R[C] holds R[B]
proof
defpred R[object,object] means
$1 is Ordinal & $2 is Sequence & for A,L st A = $1 & L = $2 holds P[A,L];
let B such that
A2: for C st C in B ex L st P[C,L];
A3: for a,b,c being object st R[a,b] & R[a,c] holds b = c
proof
let a,b,c be object;
assume that
A4: a is Ordinal and
A5: b is Sequence and
A6: for A,L st A = a & L = b holds P[A,L] and
a is Ordinal and
A7: c is Sequence and
A8: for A,L st A = a & L = c holds P[ A,L];
reconsider a as Ordinal by A4;
reconsider c as Sequence by A7;
A9: dom c = a by A8;
A10: for A st A in a & A <> 0 & A is limit_ordinal holds c.A = D(A,c|A)
by A8;
A11: for A st succ A in a holds c.(succ A) = C(A,c.A) by A8;
A12: 0 in a implies c.0 = B() by A8;
reconsider b as Sequence by A5;
A13: 0 in a implies b.0 = B() by A6;
A14: for A st succ A in a holds b.(succ A) = C(A,b.A) by A6;
A15: for A st A in a & A <> 0 & A is limit_ordinal holds b.A = D(A,b|A)
by A6;
A16: dom b = a by A6;
b = c from TSUniq1(A16,A13,A14,A15,A9,A12,A11,A10);
hence thesis;
end;
consider G being Function such that
A17: for a,b being object holds [a,b] in G iff a in B & R[a,b]
from FUNCT_1:sch 1(A3);
defpred Q[object,object] means
ex A,L st A = $1 & L = G.$1 & (A = 0 & $2 = B()
or (ex B st A = succ B & $2 = C(B,L.B)) or A <> 0 & A is limit_ordinal & $2 =
D(A,L));
A18: dom G = B
proof
thus for a being object holds a in dom G implies a in B
proof let a be object;
assume a in dom G;
then ex b being object st [a,b] in G by XTUPLE_0:def 12;
hence thesis by A17;
end;
let a be object;
assume
A19: a in B;
then reconsider a9 = a as Ordinal;
consider L such that
A20: P[a9,L] by A2,A19;
for A holds for K be Sequence holds A = a9 & K = L implies P[A,K]
by A20;
then [a9,L] in G by A17,A19;
hence thesis by XTUPLE_0:def 12;
end;
A21: for a being object st a in B ex b being object st Q[a,b]
proof
let a be object;
assume
A22: a in B;
then reconsider A = a as Ordinal;
consider c being object such that
A23: [a,c] in G by A18,A22,XTUPLE_0:def 12;
reconsider L = c as Sequence by A17,A23;
A24: now
given C such that
A25: A = succ C;
thus ex b being object st Q[a,b]
proof
take C(C,L.C), A, L;
thus A = a & L = G.a by A23,FUNCT_1:1;
thus thesis by A25;
end;
end;
A26: now
assume
A27: A <> 0 & for C holds A <> succ C;
thus Q[a,D(A,L)]
proof
take A,L;
thus A = a & L = G.a by A23,FUNCT_1:1;
thus thesis by A27,ORDINAL1:29;
end;
end;
now
assume
A28: A = 0;
thus Q[a,B()]
proof
take A,L;
thus A = a & L = G.a by A23,FUNCT_1:1;
thus thesis by A28;
end;
end;
hence thesis by A24,A26;
end;
A29: for a,b,c being object st a in B & Q[a,b] & Q[a,c] holds b = c
proof
let a,b,c being object such that
a in B;
given Ab being Ordinal,Lb being Sequence such that
A30: Ab = a and
A31: Lb = G.a and
A32: Ab = 0 & b = B() or (ex B st Ab = succ B & b = C(B,Lb.B)) or
Ab <> 0 & Ab is limit_ordinal & b = D(Ab,Lb);
given Ac being Ordinal,Lc being Sequence such that
A33: Ac = a and
A34: Lc = G.a and
A35: Ac = 0 & c = B() or (ex B st Ac = succ B & c = C(B,Lc.B)) or
Ac <> 0 & Ac is limit_ordinal & c = D(Ac,Lc);
now
given C such that
A36: Ab = succ C;
consider A such that
A37: Ab = succ A and
A38: b = C(A,Lb.A) by A32,A36,ORDINAL1:29;
consider D such that
A39: Ac = succ D and
A40: c = C(D,Lc.D) by A30,A33,A35,A36,ORDINAL1:29;
A = D by A30,A33,A37,A39,ORDINAL1:7;
hence thesis by A31,A34,A38,A40;
end;
hence thesis by A30,A31,A32,A33,A34,A35;
end;
consider F being Function such that
A41: dom F = B & for a being object st a in B holds Q[a,F.a]
from FUNCT_1:sch 2(A29
,A21);
reconsider L = F as Sequence by A41,ORDINAL1:def 7;
take L;
thus dom L = B by A41;
thus 0 in B implies L.0 = B()
proof
assume 0 in B;
then ex A being Ordinal, K being Sequence st A = 0 & K = G.0 & (A =
0 & F.0 = B() or (ex B st A = succ B & F.0 = C(B,K.B)) or A <> 0 & A is
limit_ordinal & F.0 = D(A,K)) by A41;
hence thesis;
end;
A42: for A,L1 st A in B & L1 = G.A holds L|A = L1
proof
defpred Q[Ordinal] means for L1 st $1 in B & L1 = G.$1 holds L|$1 = L1;
A43: for A st for C st C in A holds Q[C] holds Q[A]
proof
let A such that
for C st C in A for L1 st C in B & L1 = G.C holds L|C = L1;
let L1;
assume that
A44: A in B and
A45: L1 = G.A;
A46: [A,L1] in G by A18,A44,A45,FUNCT_1:1;
then
A47: P[A,L1] by A17;
A48: now
let x be object;
assume
A49: x in A;
then reconsider x9 = x as Ordinal;
A50: x9 in B by A44,A49,ORDINAL1:10;
then consider A1,L2 such that
A51: A1 = x9 and
A52: L2 = G.x9 and
A53: A1 = 0 & L.x9 = B() or (ex B st A1 = succ B & L.x9 = C(B,
L2.B)) or A1 <> 0 & A1 is limit_ordinal & L.x9 = D(A1,L2) by A41;
for D,L3 st D = x9 & L3 = L1|x9 holds P[D,L3]
proof
let D,L3 such that
A54: D = x9 and
A55: L3 = L1|x9;
x9 c= A by A49,ORDINAL1:def 2;
hence dom L3 = D by A47,A54,A55,RELAT_1:62;
thus 0 in D implies L3.0 = B() by A47,A49,A54,A55,FUNCT_1:49
,ORDINAL1:10;
thus succ C in D implies L3.(succ C) = C(C,L3.C)
proof
assume
A56: succ C in D;
C in succ C by ORDINAL1:6;
then
A57: L1|x9.C = L1.C by A54,A56,FUNCT_1:49,ORDINAL1:10;
succ C in A & L1|x9.succ C = L1.succ C by A49,A54,A56,FUNCT_1:49
,ORDINAL1:10;
hence thesis by A17,A46,A55,A57;
end;
let C;
assume that
A58: C in D and
A59: C <> 0 & C is limit_ordinal;
C c= x9 by A54,A58,ORDINAL1:def 2;
then
A60: L1|C = L3|C by A55,FUNCT_1:51;
C in A by A49,A54,A58,ORDINAL1:10;
then L1.C = D(C,L3|C) by A17,A46,A59,A60;
hence thesis by A54,A55,A58,FUNCT_1:49;
end;
then [x9,L1|x9] in G by A17,A50;
then
A61: L1|x9 = L2 by A52,FUNCT_1:1;
A62: L|A.x = L.x by A49,FUNCT_1:49;
now
given D such that
A63: x9 = succ D;
A64: L1.x = C(D,L1.D) by A17,A46,A49,A63;
consider C such that
A65: A1 = succ C and
A66: L.x9 = C(C,L2.C) by A51,A53,A63,ORDINAL1:29;
C = D by A51,A63,A65,ORDINAL1:7;
hence L1.x = L|A.x by A62,A61,A63,A66,A64,FUNCT_1:49,ORDINAL1:6;
end;
hence L1.x = L|A.x by A17,A46,A49,A51,A53,A62,A61;
end;
A c= dom L by A41,A44,ORDINAL1:def 2;
then dom(L|A) = A by RELAT_1:62;
hence thesis by A47,A48,FUNCT_1:2;
end;
thus for A holds Q[A] from ORDINAL1:sch 2(A43);
end;
thus succ A in B implies L.(succ A) = C(A,L.A)
proof
assume
A67: succ A in B;
then consider C being Ordinal, K being Sequence such that
A68: C = succ A and
A69: K = G.succ A and
A70: C = 0 & F.succ A = B() or (ex B st C = succ B & F.succ A = C(B
,K.B)) or C <> 0 & C is limit_ordinal & F.succ A = D(C,K) by A41;
A71: K = L|succ A by A42,A67,A69;
consider D such that
A72: C = succ D and
A73: F.succ A = C(D,K.D) by A68,A70,ORDINAL1:29;
A = D by A68,A72,ORDINAL1:7;
hence thesis by A73,A71,FUNCT_1:49,ORDINAL1:6;
end;
let D;
assume that
A74: D in B and
A75: D <> 0 & D is limit_ordinal;
ex A being Ordinal, K being Sequence st A = D & K = G.D & (A = 0
& F.D = B() or (ex B st A = succ B & F.D = C(B,K.B)) or A <> 0 & A is
limit_ordinal & F.D = D(A,K)) by A41,A74;
hence thesis by A42,A74,A75,ORDINAL1:29;
end;
for A holds R[A] from ORDINAL1:sch 2(A1);
hence thesis;
end;
scheme
TSResult { L()->Sequence, F(Ordinal)->set, A()->Ordinal, B()->set, C(
Ordinal,set)->set, D(Ordinal,Sequence)->set } : for A st A in dom L() holds L
().A = F(A)
provided
A1: for A,x holds x = F(A) iff ex L st x = last L & dom L = succ A & L.
0 = B() & (for C st succ C in succ A holds L.succ C = C(C,L.C)) & for C st C
in succ A & C <> 0 & C is limit_ordinal holds L.C = D(C,L|C) and
A2: dom L() = A() and
A3: 0 in A() implies L().0 = B() and
A4: for A st succ A in A() holds L().(succ A) = C(A,L().A) and
A5: for A st A in A() & A <> 0 & A is limit_ordinal holds L().A = D(A,L ()|A)
proof
let A;
set L = L()|succ A;
assume A in dom L();
then
A6: succ A c= dom L() by ORDINAL1:21;
A7: for C st succ C in succ A holds L.succ C = C(C,L.C)
proof
let C such that
A8: succ C in succ A;
C in succ C by ORDINAL1:6;
then
A9: L.C = L().C by A8,FUNCT_1:49,ORDINAL1:10;
L.succ C = L().succ C by A8,FUNCT_1:49;
hence thesis by A2,A4,A6,A8,A9;
end;
A10: for C st C in succ A & C <> 0 & C is limit_ordinal holds L.C = D(C,L|C )
proof
let C;
assume that
A11: C in succ A and
A12: C <> 0 & C is limit_ordinal;
C c= succ A by A11,ORDINAL1:def 2;
then
A13: L|C = L()|C by FUNCT_1:51;
L.C = L().C by A11,FUNCT_1:49;
hence thesis by A2,A5,A6,A11,A12,A13;
end;
0 c= succ A;
then 0 c< succ A;
then
A14: 0 in succ A & L.0 = L().0 by FUNCT_1:49,ORDINAL1:11;
A15: dom L = succ A by A6,RELAT_1:62;
then A in succ A & last L = L.A by Th2,ORDINAL1:21;
then last L = L().A by FUNCT_1:49;
hence thesis by A1,A2,A3,A6,A15,A14,A7,A10;
end;
scheme
TSDef { A()->Ordinal, B()->set, C(Ordinal,set)->set, D(Ordinal,Sequence)->
set } : (ex x,L st x = last L & dom L = succ A() & L.0 = B() & (for C st succ
C in succ A() holds L.succ C = C(C,L.C)) & for C st C in succ A() & C <> 0 & C
is limit_ordinal holds L.C = D(C,L|C) ) & for x1,x2 being set st (ex L st x1 =
last L & dom L = succ A() & L.0 = B() & (for C st succ C in succ A() holds L.
succ C = C(C,L.C)) & for C st C in succ A() & C <> 0 & C is limit_ordinal
holds L.C = D(C,L|C) ) & (ex L st x2 = last L & dom L = succ A() & L.0 = B() &
(for C st succ C in succ A() holds L.succ C = C(C,L.C)) & for C st C in succ A(
) & C <> 0 & C is limit_ordinal holds L.C = D(C,L|C) ) holds x1 = x2 proof
consider L such that
A1: dom L = succ A() & (0 in succ A() implies L.0 = B() ) & (for C st
succ C in succ A() holds L.(succ C) = C(C,L.C)) & for C st C in succ A() & C <>
0 & C is limit_ordinal holds L.C = D(C,L|C) from TSExist1;
thus ex x,L st x = last L & dom L = succ A() & L.0 = B() & (for C st succ C
in succ A() holds L.succ C = C(C,L.C)) & for C st C in succ A() & C <> 0 & C
is limit_ordinal holds L.C = D(C,L|C)
proof
take x = last L, L;
thus x = last L & dom L = succ A() by A1;
0 c= succ A();
then 0 c< succ A();
hence thesis by A1,ORDINAL1:11;
end;
let x1,x2 be set;
given L1 such that
A2: x1 = last L1 and
A3: dom L1 = succ A() and
A4: L1.0 = B() and
A5: for C st succ C in succ A() holds L1.succ C = C(C,L1.C) and
A6: for C st C in succ A() & C <> 0 & C is limit_ordinal holds L1.C = D
(C,L1|C);
A7: 0 in succ A() implies L1.0 = B() by A4;
given L2 such that
A8: x2 = last L2 and
A9: dom L2 = succ A() and
A10: L2.0 = B() and
A11: for C st succ C in succ A() holds L2.succ C = C(C,L2.C) and
A12: for C st C in succ A() & C <> 0 & C is limit_ordinal holds L2.C =
D(C,L2|C);
A13: 0 in succ A() implies L2.0 = B() by A10;
L1 = L2 from TSUniq1(A3,A7,A5,A6,A9,A13,A11,A12);
hence thesis by A2,A8;
end;
scheme
TSResult0 { F(Ordinal)->set, B()->set, C(Ordinal,set)->set, D(Ordinal,
Sequence)->set } : F(0) = B()
provided
A1: for A,x holds x = F(A) iff ex L st x = last L & dom L = succ A & L.
0 = B() & (for C st succ C in succ A holds L.succ C = C(C,L.C)) & for C st C
in succ A & C <> 0 & C is limit_ordinal holds L.C = D(C,L|C)
proof
consider L such that
A2: dom L = succ 0 & (0 in succ 0 implies L.0 = B() ) & (for A st
succ A in succ 0 holds L.(succ A) = C(A,L.A) ) & for A st A in succ 0 & A <>
0 & A is limit_ordinal holds L.A = D(A,L|A) from TSExist1;
B() = last L by A2,Th2,ORDINAL1:6;
hence thesis by A1,A2,ORDINAL1:6;
end;
scheme
TSResultS { B()->set, C(Ordinal,set)->set, D(Ordinal,Sequence)->set, F(
Ordinal)->set } : for A holds F(succ A) = C(A,F(A))
provided
A1: for A,x holds x = F(A) iff ex L st x = last L & dom L = succ A & L.
0 = B() & (for C st succ C in succ A holds L.succ C = C(C,L.C)) & for C st C
in succ A & C <> 0 & C is limit_ordinal holds L.C = D(C,L|C)
proof
let A;
consider L such that
A2: dom L = succ succ A and
A3: 0 in succ succ A implies L.0 = B() and
A4: for C st succ C in succ succ A holds L.(succ C) = C(C,L.C) and
A5: for C st C in succ succ A & C <> 0 & C is limit_ordinal holds L.C =
D(C,L|C) from TSExist1;
A6: for A,x holds x = F(A) iff ex L st x = last L & dom L = succ A & L.0 =
B() & (for C st succ C in succ A holds L.succ C = C(C,L.C)) & for C st C in
succ A & C <> 0 & C is limit_ordinal holds L.C = D(C,L|C) by A1;
A7: for B st B in dom L holds L.B = F(B) from TSResult(A6,A2,A3,A4, A5);
then
A8: L.succ A = F(succ A) by A2,ORDINAL1:6;
A in succ A & succ A in succ succ A by ORDINAL1:6;
then L.A = F(A) by A2,A7,ORDINAL1:10;
hence thesis by A4,A8,ORDINAL1:6;
end;
scheme
TSResultL { L()->Sequence, A()->Ordinal, F(Ordinal)->set, B()->set, C(
Ordinal,set)->set, D(Ordinal,Sequence)->set } : F(A()) = D(A(),L())
provided
A1: for A,x holds x = F(A) iff ex L st x = last L & dom L = succ A & L.
0 = B() & (for C st succ C in succ A holds L.succ C = C(C,L.C)) & for C st C
in succ A & C <> 0 & C is limit_ordinal holds L.C = D(C,L|C) and
A2: A() <> 0 & A() is limit_ordinal and
A3: dom L() = A() and
A4: for A st A in A() holds L().A = F(A)
proof
A5: A() in succ A() by ORDINAL1:6;
consider L such that
A6: dom L = succ A() and
A7: 0 in succ A() implies L.0 = B() and
A8: for C st succ C in succ A() holds L.(succ C) = C(C,L.C) and
A9: for C st C in succ A() & C <> 0 & C is limit_ordinal holds L.C = D(
C,L|C) from TSExist1;
set L1 = L|A();
A10: for A,x holds x = F(A) iff ex L st x = last L & dom L = succ A & L.0 =
B() & (for C st succ C in succ A holds L.succ C = C(C,L.C)) & for C st C in
succ A & C <> 0 & C is limit_ordinal holds L.C = D(C,L|C) by A1;
A11: for B st B in dom L holds L.B = F(B) from TSResult(A10,A6,A7,A8, A9);
A12: now
let x be object;
assume
A13: x in A();
then reconsider x9 = x as Ordinal;
thus L1.x = L.x9 by A13,FUNCT_1:49
.= F(x9) by A6,A11,A5,A13,ORDINAL1:10
.= L().x by A4,A13;
end;
A() c= dom L by A6,A5,ORDINAL1:def 2;
then dom L1 = A() by RELAT_1:62;
then L1 = L() by A3,A12,FUNCT_1:2;
then L.A() = D(A(),L()) by A2,A9,ORDINAL1:6;
hence thesis by A6,A11,ORDINAL1:6;
end;
scheme
OSExist { A()->Ordinal, B()->Ordinal, C(Ordinal,Ordinal)->Ordinal, D(Ordinal
,Sequence)->Ordinal } : ex fi st dom fi = A() & (0 in A() implies fi.0 = B(
) ) & (for A st succ A in A() holds fi.(succ A) = C(A,fi.A) ) & for A st A in A
() & A <> 0 & A is limit_ordinal holds fi.A = D(A,fi|A) proof
deffunc CC(Ordinal,set) = C($1,sup union {$2});
consider L such that
A1: dom L = A() and
A2: 0 in A() implies L.0 = B() and
A3: for A st succ A in A() holds L.(succ A) = CC(A,L.A) and
A4: for A st A in A() & A <> 0 & A is limit_ordinal holds L.A = D(A,L|A
) from TSExist1;
L is Ordinal-yielding
proof
take sup rng L;
let x be object;
assume
A5: x in rng L;
then consider y being object such that
A6: y in dom L and
A7: x = L.y by FUNCT_1:def 3;
reconsider y as Ordinal by A6;
A8: now
assume that
A9: y <> 0 and
A10: for B holds y <> succ B;
y is limit_ordinal by A10,ORDINAL1:29;
then L.y = D(y,L|y) by A1,A4,A6,A9;
hence x is Ordinal by A7;
end;
A11: On rng L c= sup rng L by Def3;
now
given B such that
A12: y = succ B;
L.y = C(B,sup union {L.B}) by A1,A3,A6,A12;
hence x is Ordinal by A7;
end;
then x in On rng L by A1,A2,A5,A6,A7,A8,ORDINAL1:def 9;
hence thesis by A11;
end;
then reconsider L as Ordinal-Sequence;
take fi = L;
thus dom fi = A() & (0 in A() implies fi.0 = B() ) by A1,A2;
thus for A st succ A in A() holds fi.(succ A) = C(A,fi.A)
proof
let A;
reconsider B = fi.A as Ordinal;
sup union {B} = sup B by ZFMISC_1:25
.= B by Th18;
hence thesis by A3;
end;
thus thesis by A4;
end;
scheme
OSResult { fi()->Ordinal-Sequence, F(Ordinal)->Ordinal, A()->Ordinal, B()->
Ordinal, C(Ordinal,Ordinal)->Ordinal, D(Ordinal,Sequence)->Ordinal } : for A
st A in dom fi() holds fi().A = F(A)
provided
A1: for A,B holds B = F(A) iff ex fi st B = last fi & dom fi = succ A &
fi.0 = B() & (for C st succ C in succ A holds fi.succ C = C(C,fi.C)) & for C
st C in succ A & C <> 0 & C is limit_ordinal holds fi.C = D(C,fi|C) and
A2: dom fi() = A() and
A3: 0 in A() implies fi().0 = B() and
A4: for A st succ A in A() holds fi().(succ A) = C(A,fi().A) and
A5: for A st A in A() & A <> 0 & A is limit_ordinal holds fi().A = D(A,
fi()|A)
proof
let A;
set fi = fi()|succ A;
assume A in dom fi();
then
A6: succ A c= dom fi() by ORDINAL1:21;
A7: for C st succ C in succ A holds fi.succ C = C(C,fi.C)
proof
let C such that
A8: succ C in succ A;
C in succ C by ORDINAL1:6;
then
A9: fi.C = fi().C by A8,FUNCT_1:49,ORDINAL1:10;
fi.succ C = fi().succ C by A8,FUNCT_1:49;
hence thesis by A2,A4,A6,A8,A9;
end;
A10: for C st C in succ A & C <> 0 & C is limit_ordinal holds fi.C = D(C,fi
|C)
proof
let C;
assume that
A11: C in succ A and
A12: C <> 0 & C is limit_ordinal;
C c= succ A by A11,ORDINAL1:def 2;
then
A13: fi|C = fi()|C by FUNCT_1:51;
fi.C = fi().C by A11,FUNCT_1:49;
hence thesis by A2,A5,A6,A11,A12,A13;
end;
0 c= succ A;
then 0 c< succ A;
then
A14: 0 in succ A & fi.0 = fi().0 by FUNCT_1:49,ORDINAL1:11;
A15: dom fi = succ A by A6,RELAT_1:62;
then A in succ A & last fi = fi.A by Th2,ORDINAL1:21;
then last fi = fi().A by FUNCT_1:49;
hence thesis by A1,A2,A3,A6,A15,A14,A7,A10;
end;
scheme
OSDef { A()->Ordinal, B()->Ordinal, C(Ordinal,Ordinal)->Ordinal, D(Ordinal,
Sequence)->Ordinal } : (ex A,fi st A = last fi & dom fi = succ A() & fi.0 =
B() & (for C st succ C in succ A() holds fi.succ C = C(C,fi.C)) & for C st C in
succ A() & C <> 0 & C is limit_ordinal holds fi.C = D(C,fi|C) ) & for A1,A2 st
(ex fi st A1 = last fi & dom fi = succ A() & fi.0 = B() & (for C st succ C in
succ A() holds fi.succ C = C(C,fi.C)) & for C st C in succ A() & C <> 0 & C is
limit_ordinal holds fi.C = D(C,fi|C) ) & (ex fi st A2 = last fi & dom fi = succ
A() & fi.0 = B() & (for C st succ C in succ A() holds fi.succ C = C(C,fi.C)) &
for C st C in succ A() & C <> 0 & C is limit_ordinal holds fi.C = D(C,fi|C) )
holds A1 = A2 proof
consider fi such that
A1: dom fi = succ A() & (0 in succ A() implies fi.0 = B() ) & (for C
st succ C in succ A() holds fi.(succ C) = C(C,fi.C)) & for C st C in succ A() &
C <> 0 & C is limit_ordinal holds fi.C = D(C,fi|C) from OSExist;
reconsider A = last fi as Ordinal;
thus ex A,fi st A = last fi & dom fi = succ A() & fi.0 = B() & (for C st
succ C in succ A() holds fi.succ C = C(C,fi.C)) & for C st C in succ A() & C <>
0 & C is limit_ordinal holds fi.C = D(C,fi|C)
proof
take A, fi;
thus A = last fi & dom fi = succ A() by A1;
0 c= succ A();
then 0 c< succ A();
hence thesis by A1,ORDINAL1:11;
end;
deffunc CD(Ordinal,Ordinal) = C($1,sup union { $2 });
let A1,A2 be Ordinal;
given L1 being Ordinal-Sequence such that
A2: A1 = last L1 and
A3: dom L1 = succ A() and
A4: L1.0 = B() and
A5: for C st succ C in succ A() holds L1.succ C = C(C,L1.C) and
A6: for C st C in succ A() & C <> 0 & C is limit_ordinal holds L1.C = D
(C,L1|C);
A7: 0 in succ A() implies L1.0 = B() by A4;
A8: for C st succ C in succ A() holds L1.(succ C) = CD(C,L1.C)
proof
let C such that
A9: succ C in succ A();
reconsider x9 = L1.C as Ordinal;
sup union { L1.C } = sup x9 by ZFMISC_1:25
.= x9 by Th18;
hence thesis by A5,A9;
end;
given L2 being Ordinal-Sequence such that
A10: A2 = last L2 and
A11: dom L2 = succ A() and
A12: L2.0 = B() and
A13: for C st succ C in succ A() holds L2.succ C = C(C,L2.C) and
A14: for C st C in succ A() & C <> 0 & C is limit_ordinal holds L2.C =
D(C,L2|C);
A15: for C st C in succ A() & C <> 0 & C is limit_ordinal holds L2.C = D(C,
L2|C) by A14;
A16: for C st C in succ A() & C <> 0 & C is limit_ordinal holds L1.C = D(C,
L1|C) by A6;
A17: for C st succ C in succ A() holds L2.(succ C) = CD(C,L2.C)
proof
let C such that
A18: succ C in succ A();
reconsider x9 = L2.C as Ordinal;
sup union { L2.C } = sup x9 by ZFMISC_1:25
.= x9 by Th18;
hence thesis by A13,A18;
end;
A19: 0 in succ A() implies L2.0 = B() by A12;
L1 = L2 from TSUniq1(A3,A7,A8,A16,A11,A19,A17,A15);
hence thesis by A2,A10;
end;
scheme
OSResult0 { F(Ordinal)->Ordinal, B()->Ordinal, C(Ordinal,Ordinal)->Ordinal,
D(Ordinal,Sequence)->Ordinal } : F(0) = B()
provided
A1: for A,B holds B = F(A) iff ex fi st B = last fi & dom fi = succ A &
fi.0 = B() & (for C st succ C in succ A holds fi.succ C = C(C,fi.C)) & for C
st C in succ A & C <> 0 & C is limit_ordinal holds fi.C = D(C,fi|C)
proof
consider fi such that
A2: dom fi = succ 0 & (0 in succ 0 implies fi.0 = B() ) & (for A st
succ A in succ 0 holds fi.(succ A) = C(A,fi.A) ) & for A st A in succ 0 & A
<> 0 & A is limit_ordinal holds fi.A = D(A,fi|A) from OSExist;
B() = last fi by A2,Th2,ORDINAL1:6;
hence thesis by A1,A2,ORDINAL1:6;
end;
scheme
OSResultS { B()->Ordinal, C(Ordinal,Ordinal)->Ordinal, D(Ordinal,Sequence)
->Ordinal, F(Ordinal)->Ordinal } : for A holds F(succ A) = C(A,F(A))
provided
A1: for A,B holds B = F(A) iff ex fi st B = last fi & dom fi = succ A &
fi.0 = B() & (for C st succ C in succ A holds fi.succ C = C(C,fi.C)) & for C
st C in succ A & C <> 0 & C is limit_ordinal holds fi.C = D(C,fi|C)
proof
let A;
consider fi such that
A2: dom fi = succ succ A and
A3: 0 in succ succ A implies fi.0 = B() and
A4: for C st succ C in succ succ A holds fi.(succ C) = C(C,fi.C) and
A5: for C st C in succ succ A & C <> 0 & C is limit_ordinal holds fi.C
= D(C,fi|C) from OSExist;
A6: for A,B holds B = F(A) iff ex fi st B = last fi & dom fi = succ A & fi.
0 = B() & (for C st succ C in succ A holds fi.succ C = C(C,fi.C)) & for C st C
in succ A & C <> 0 & C is limit_ordinal holds fi.C = D(C,fi|C) by A1;
A7: for B st B in dom fi holds fi.B = F(B) from OSResult(A6,A2,A3,A4, A5);
then
A8: fi.succ A = F(succ A) by A2,ORDINAL1:6;
A in succ A & succ A in succ succ A by ORDINAL1:6;
then fi.A = F(A) by A2,A7,ORDINAL1:10;
hence thesis by A4,A8,ORDINAL1:6;
end;
scheme
OSResultL { fi()->Ordinal-Sequence, A()->Ordinal, F(Ordinal)->Ordinal, B()->
Ordinal, C(Ordinal,Ordinal)->Ordinal, D(Ordinal,Sequence)->Ordinal } : F(A())
= D(A(),fi())
provided
A1: for A,B holds B = F(A) iff ex fi st B = last fi & dom fi = succ A &
fi.0 = B() & (for C st succ C in succ A holds fi.succ C = C(C,fi.C)) & for C
st C in succ A & C <> 0 & C is limit_ordinal holds fi.C = D(C,fi|C) and
A2: A() <> 0 & A() is limit_ordinal and
A3: dom fi() = A() and
A4: for A st A in A() holds fi().A = F(A)
proof
A5: A() in succ A() by ORDINAL1:6;
consider fi such that
A6: dom fi = succ A() and
A7: 0 in succ A() implies fi.0 = B() and
A8: for C st succ C in succ A() holds fi.(succ C) = C(C,fi.C) and
A9: for C st C in succ A() & C <> 0 & C is limit_ordinal holds fi.C = D
(C,fi|C) from OSExist;
set psi = fi|A();
A10: for A,B holds B = F(A) iff ex fi st B = last fi & dom fi = succ A & fi.
0 = B() & (for C st succ C in succ A holds fi.succ C = C(C,fi.C)) & for C st C
in succ A & C <> 0 & C is limit_ordinal holds fi.C = D(C,fi|C) by A1;
A11: for B st B in dom fi holds fi.B = F(B) from OSResult(A10,A6,A7,A8, A9);
A12: now
let x be object;
assume
A13: x in A();
then reconsider x9 = x as Ordinal;
thus psi.x = fi.x9 by A13,FUNCT_1:49
.= F(x9) by A6,A11,A5,A13,ORDINAL1:10
.= fi().x by A4,A13;
end;
A() c= dom fi by A6,A5,ORDINAL1:def 2;
then dom psi = A() by RELAT_1:62;
then psi = fi() by A3,A12,FUNCT_1:2;
then fi.A() = D(A(),fi()) by A2,A9,ORDINAL1:6;
hence thesis by A6,A11,ORDINAL1:6;
end;
definition
let L;
func sup L -> Ordinal equals
sup rng L;
correctness;
func inf L -> Ordinal equals
inf rng L;
correctness;
end;
theorem
sup L = sup rng L & inf L = inf rng L;
definition
let L;
func lim_sup L -> Ordinal means
ex fi st it = inf fi & dom fi = dom L &
for A st A in dom L holds fi.A = sup rng (L|(dom L \ A));
existence
proof
deffunc F(Ordinal) = sup rng (L|(dom L \ $1));
consider fi such that
A1: dom fi = dom L & for A st A in dom L holds fi.A = F(A) from
OSLambda;
take inf fi, fi;
thus thesis by A1;
end;
uniqueness
proof
let A1,A2 be Ordinal;
given fi such that
A2: A1 = inf fi & dom fi = dom L and
A3: for A st A in dom L holds fi.A = sup rng (L|(dom L \ A));
given psi such that
A4: A2 = inf psi & dom psi = dom L and
A5: for A st A in dom L holds psi.A = sup rng (L|(dom L \ A));
now
let x be object;
assume
A6: x in dom L;
then reconsider A = x as Ordinal;
fi.A = sup rng (L|(dom L \ A)) by A3,A6;
hence fi.x = psi.x by A5,A6;
end;
hence thesis by A2,A4,FUNCT_1:2;
end;
func lim_inf L -> Ordinal means
ex fi st it = sup fi & dom fi = dom L &
for A st A in dom L holds fi.A = inf rng (L|(dom L \ A));
existence
proof
deffunc F(Ordinal) = inf rng (L|(dom L \ $1));
consider fi such that
A7: dom fi = dom L & for A st A in dom L holds fi.A = F(A) from
OSLambda;
take sup fi, fi;
thus thesis by A7;
end;
uniqueness
proof
let A1,A2 be Ordinal;
given fi such that
A8: A1 = sup fi & dom fi = dom L and
A9: for A st A in dom L holds fi.A = inf rng (L|(dom L \ A));
given psi such that
A10: A2 = sup psi & dom psi = dom L and
A11: for A st A in dom L holds psi.A = inf rng (L|(dom L \ A));
now
let x be object;
assume
A12: x in dom L;
then reconsider A = x as Ordinal;
fi.A = inf rng (L|(dom L \ A)) by A9,A12;
hence fi.x = psi.x by A11,A12;
end;
hence thesis by A8,A10,FUNCT_1:2;
end;
end;
definition
let A,fi;
pred A is_limes_of fi means
:Def9:
ex B st B in dom fi & for C st B c= C & C in dom fi holds fi.C = 0 if A = 0
otherwise for B,C st B in A & A in C
ex D 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;
consistency;
end;
definition
let fi;
given A such that
A1: A is_limes_of fi;
func lim fi -> Ordinal means
:Def10:
it is_limes_of fi;
existence by A1;
uniqueness
proof
let A1,A2 be Ordinal such that
A2: (A1 = 0 & ex B st B in dom fi & for C st B c= C & C in dom fi
holds fi.C = 0) or (A1 <> 0 & for B,C st B in A1 & A1 in C ex D 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)
and
A3: (A2 = 0 & ex B st B in dom fi & for C st B c= C & C in dom fi
holds fi.C = 0) or (A2 <> 0 & for B,C st B in A2 & A2 in C ex D 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);
A4: now
set x = the Element of A1;
reconsider x as Ordinal;
assume A1 in A2;
then consider D such that
A5: D in dom fi and
A6: for A st D c= A & A in dom fi holds A1 in fi.A & fi.A in succ A2
by A3,ORDINAL1:6;
now
assume A1 = 0;
then consider B such that
A7: B in dom fi and
A8: for C st B c= C & C in dom fi holds fi.C = 0 by A2;
B c= D or D c= B;
then consider E being Ordinal such that
A9: E = D & B c= D or E = B & D c= B;
fi.E = 0 by A5,A7,A8,A9;
hence contradiction by A5,A6,A7,A9;
end;
then consider C such that
A10: C in dom fi and
A11: for A st C c= A & A in dom fi holds x in fi.A & fi.A in succ A1
by A2,ORDINAL1:6;
C c= D or D c= C;
then consider E being Ordinal such that
A12: E = D & C c= D or E = C & D c= C;
fi.E in succ A1 by A5,A10,A11,A12;
then
A13: fi.E in A1 or fi.E = A1 by ORDINAL1:8;
A1 in fi.E by A5,A6,A10,A12;
hence contradiction by A13;
end;
set x = the Element of A2;
reconsider x as Ordinal;
assume A1 <> A2;
then A1 in A2 or A2 in A1 by ORDINAL1:14;
then consider D such that
A14: D in dom fi and
A15: for A st D c= A & A in dom fi holds A2 in fi.A & fi.A in succ A1
by A2,A4,ORDINAL1:6;
now
assume A2 = 0;
then consider B such that
A16: B in dom fi and
A17: for C st B c= C & C in dom fi holds fi.C = 0 by A3;
B c= D or D c= B;
then consider E being Ordinal such that
A18: E = D & B c= D or E = B & D c= B;
fi.E = 0 by A14,A16,A17,A18;
hence contradiction by A14,A15,A16,A18;
end;
then consider C such that
A19: C in dom fi and
A20: for A st C c= A & A in dom fi holds x in fi.A & fi.A in succ A2
by A3,ORDINAL1:6;
C c= D or D c= C;
then consider E being Ordinal such that
A21: E = D & C c= D or E = C & D c= C;
fi.E in succ A2 by A14,A19,A20,A21;
then
A22: fi.E in A2 or fi.E = A2 by ORDINAL1:8;
A2 in fi.E by A14,A15,A19,A21;
hence contradiction by A22;
end;
end;
definition
let A,fi;
func lim(A,fi) -> Ordinal equals
lim(fi|A);
correctness;
end;
definition
let L be Ordinal-Sequence;
attr L is increasing means
for A,B st A in B & B in dom L holds L.A in L.B;
attr L is continuous means
for A,B st A in dom L & A <> 0 & A is
limit_ordinal & B = L.A holds B is_limes_of L|A;
end;
definition
let A,B be Ordinal;
func A +^ B -> Ordinal means
:Def14:
ex fi st it = last fi & dom fi = succ B & fi.0 = A &
(for C st succ C in succ B holds fi.succ C = succ(fi.C)) &
for C st C in succ B & C <> 0 & C is limit_ordinal holds fi.C = sup(fi|C);
correctness
proof
deffunc D(Ordinal,Sequence) = sup $2;
deffunc C(Ordinal,Ordinal) = succ $2;
(ex F being Ordinal,fi st F = last fi & dom fi = succ B & fi.0 = A &
(for C st succ C in succ B holds fi.succ C = C(C,fi.C)) & for C st C in succ B
& C <> 0 & C is limit_ordinal holds fi.C = D(C,fi|C) ) & for A1,A2 st (ex fi
st A1 = last fi & dom fi = succ B & fi.0 = A & (for C st succ C in succ B
holds fi.succ C = C(C,fi.C)) & for C st C in succ B & C <> 0 & C is
limit_ordinal holds fi.C = D(C,fi|C) ) & (ex fi st A2 = last fi & dom fi = succ
B & fi.0 = A & (for C st succ C in succ B holds fi.succ C = C(C,fi.C)) & for C
st C in succ B & C <> 0 & C is limit_ordinal holds fi.C = D(C,fi|C) ) holds A1
= A2 from OSDef;
hence thesis;
end;
end;
definition
let A,B;
func A *^ B -> Ordinal means
:Def15:
ex fi st it = last fi & dom fi = succ A & fi.0 = 0 &
(for C st succ C in succ A holds fi.succ C = (fi.C)+^B) &
for C st C in succ A & C <> 0 & C is limit_ordinal
holds fi.C = union sup(fi|C);
correctness
proof
deffunc D(Ordinal,Ordinal-Sequence) = union sup $2;
deffunc C(Ordinal,Ordinal) = $2+^B;
(ex F being Ordinal,fi st F = last fi & dom fi = succ A & fi.0 = 0 &
(for C st succ C in succ A holds fi.succ C = C(C,fi.C)) & for C st C in succ A
& C <> 0 & C is limit_ordinal holds fi.C = D(C,fi|C) ) & for A1,A2 st (ex fi
st A1 = last fi & dom fi = succ A & fi.0 = 0 & (for C st succ C in succ A
holds fi.succ C = C(C,fi.C)) & for C st C in succ A & C <> 0 & C is
limit_ordinal holds fi.C = D(C,fi|C) ) & (ex fi st A2 = last fi & dom fi = succ
A & fi.0 = 0 & (for C st succ C in succ A holds fi.succ C = C(C,fi.C)) & for
C st C in succ A & C <> 0 & C is limit_ordinal holds fi.C = D(C,fi|C) ) holds
A1 = A2 from OSDef;
hence thesis;
end;
end;
registration
let O be Ordinal;
cluster -> ordinal for Element of O;
coherence;
end;
definition
let A,B;
func exp(A,B) -> Ordinal means
:Def16:
ex fi st it = last fi & dom fi = succ B & fi.0 = 1 &
(for C st succ C in succ B holds fi.succ C = A*^(fi.C)) &
for C st C in succ B & C <> 0 & C is limit_ordinal holds fi.C = lim(fi|C);
correctness
proof
deffunc D(Ordinal,Ordinal-Sequence) = lim $2;
deffunc C(Ordinal,Ordinal) = A*^$2;
(ex F being Ordinal,fi st F = last fi & dom fi = succ B & fi.0 = 1 &
(for C st succ C in succ B holds fi.succ C = C(C,fi.C)) & for C st C in succ B
& C <> 0 & C is limit_ordinal holds fi.C = D(C,fi|C) ) & for A1,A2 st (ex fi
st A1 = last fi & dom fi = succ B & fi.0 = 1 & (for C st succ C in succ B
holds fi.succ C = C(C,fi.C)) & for C st C in succ B & C <> 0 & C is
limit_ordinal holds fi.C = D(C,fi|C) ) & (ex fi st A2 = last fi & dom fi = succ
B & fi.0 = 1 & (for C st succ C in succ B holds fi.succ C = C(C,fi.C)) & for C
st C in succ B & C <> 0 & C is limit_ordinal holds fi.C = D(C,fi|C) ) holds A1
= A2 from OSDef;
hence thesis;
end;
end;
theorem Th27:
A+^0 = A
proof
deffunc C(Ordinal,Ordinal) = succ $2;
deffunc D(Ordinal,Sequence) = sup $2;
deffunc F(Ordinal) = A+^$1;
A1: for B,C holds C = F(B) iff ex fi st C = last fi & dom fi = succ B & fi.
0 = A & (for C st succ C in succ B holds fi.succ C = C(C,fi.C)) & for C st C
in succ B & C <> 0 & C is limit_ordinal holds fi.C = D(C,fi|C) by Def14;
thus F(0) = A from OSResult0(A1);
end;
theorem Th28:
A+^succ B = succ(A+^B)
proof
deffunc C(Ordinal,Ordinal) = succ $2;
deffunc D(Ordinal,Sequence) = sup $2;
deffunc F(Ordinal) = A+^$1;
A1: for B,C holds C = F(B) iff ex fi st C = last fi & dom fi = succ B & fi.
0 = A & (for C st succ C in succ B holds fi.succ C = C(C,fi.C)) & for C st C
in succ B & C <> 0 & C is limit_ordinal holds fi.C = D(C,fi|C) by Def14;
for B holds F(succ B) = C(B,F(B)) from OSResultS(A1);
hence thesis;
end;
theorem Th29:
B <> 0 & B is limit_ordinal implies for fi st dom fi = B & for
C st C in B holds fi.C = A+^C holds A+^B = sup fi
proof
deffunc C(Ordinal,Ordinal) = succ $2;
deffunc D(Ordinal,Ordinal-Sequence) = sup $2;
assume
A1: B <> 0 & B is limit_ordinal;
deffunc F(Ordinal) = A+^$1;
let fi such that
A2: dom fi = B and
A3: for C st C in B holds fi.C = F(C);
A4: for B,C holds C = F(B) iff ex fi st C = last fi & dom fi = succ B & fi.
0 = A & (for C st succ C in succ B holds fi.succ C = C(C,fi.C)) & for C st C
in succ B & C <> 0 & C is limit_ordinal holds fi.C = D(C,fi|C) by Def14;
thus F(B) = D(B,fi) from OSResultL(A4,A1,A2,A3);
end;
theorem Th30:
0+^A = A
proof
defpred P[Ordinal] means 0+^$1 = $1;
A1: for A holds P[A] implies P[succ A] by Th28;
A2: for A st A <> 0 & A is limit_ordinal & for B st B in A holds P[B] holds
P[A]
proof
deffunc F(Ordinal) = 0+^$1;
let A;
assume that
A3: A <> 0 & A is limit_ordinal and
A4: for B st B in A holds 0+^B = B;
consider fi such that
A5: dom fi = A & for B st B in A holds fi.B = F(B) from OSLambda;
A6: rng fi = A
proof
thus for x being object holds x in rng fi implies x in A
proof let x be object;
assume x in rng fi;
then consider y being object such that
A7: y in dom fi and
A8: x = fi.y by FUNCT_1:def 3;
reconsider y as Ordinal by A7;
x = 0+^y by A5,A7,A8
.= y by A4,A5,A7;
hence thesis by A5,A7;
end;
let x be object;
assume
A9: x in A;
then reconsider B = x as Ordinal;
0+^B = B & fi.B = 0+^B by A4,A5,A9;
hence thesis by A5,A9,FUNCT_1:def 3;
end;
0+^A = sup fi by A3,A5,Th29
.= sup rng fi;
hence thesis by A6,Th18;
end;
A10: P[0] by Th27;
for A holds P[A] from OrdinalInd(A10,A1,A2);
hence thesis;
end;
Lm1: 1 = succ 0;
theorem
A+^1 = succ A
proof
thus A+^1 = succ(A+^0) by Lm1,Th28
.= succ A by Th27;
end;
theorem Th32:
A in B implies C +^ A in C +^ B
proof
defpred P[Ordinal] means A in $1 implies C +^ A in C +^ $1;
A1: for B st for D st D in B holds P[D] holds P[B]
proof
let B such that
A2: for D st D in B holds A in D implies C +^ A in C +^ D and
A3: A in B;
A4: now
given D such that
A5: B = succ D;
A6: now
assume A in D;
then
A7: C +^ A in C +^ D by A2,A5,ORDINAL1:6;
succ(C +^ D) = C +^ succ D & C +^ D in succ(C +^ D) by Th28,ORDINAL1:6;
hence thesis by A5,A7,ORDINAL1:10;
end;
now
assume
A8: not A in D;
A c< D iff A c= D & A <> D;
then C +^ A in succ(C +^ D) by A3,A5,A8,ORDINAL1:11,22;
hence thesis by A5,Th28;
end;
hence thesis by A6;
end;
now
deffunc F(Ordinal) = C+^$1;
consider fi such that
A9: dom fi = B & for D st D in B holds fi.D = F(D) from OSLambda;
fi.A = C+^A by A3,A9;
then
A10: C+^A in rng fi by A3,A9,FUNCT_1:def 3;
assume for D holds B <> succ D;
then B is limit_ordinal by ORDINAL1:29;
then C+^B = sup fi by A3,A9,Th29
.= sup rng fi;
hence thesis by A10,Th19;
end;
hence thesis by A4;
end;
for B holds P[B] from ORDINAL1:sch 2(A1);
hence thesis;
end;
theorem Th33:
A c= B implies C +^ A c= C +^ B
proof
assume
A1: A c= B;
now
assume A <> B;
then A c< B by A1;
then C +^ A in C +^ B by Th32,ORDINAL1:11;
hence thesis by ORDINAL1:def 2;
end;
hence thesis;
end;
theorem Th34:
A c= B implies A +^ C c= B +^ C
proof
defpred P[Ordinal] means A +^ $1 c= B +^ $1;
assume
A1: A c= B;
A2: for C st for D st D in C holds P[D] holds P[C]
proof
let C such that
A3: for D st D in C holds A +^ D c= B +^ D;
A4: now
given D such that
A5: C = succ D;
A6: B +^ C = succ(B +^ D) by A5,Th28;
A +^ D c= B +^ D & A +^ C = succ(A +^ D) by A3,A5,Th28,ORDINAL1:6;
hence thesis by A6,Th1;
end;
A7: now
deffunc F(Ordinal) = A+^$1;
assume that
A8: C <> 0 and
A9: for D holds C <> succ D;
consider fi such that
A10: dom fi = C & for D st D in C holds fi.D = F(D) from OSLambda;
A11: now
let D;
assume D in rng fi;
then consider x being object such that
A12: x in dom fi and
A13: D = fi.x by FUNCT_1:def 3;
reconsider x as Ordinal by A12;
A14: B +^ x in B +^ C by A10,A12,Th32;
D = A+^x & A +^ x c= B +^ x by A3,A10,A12,A13;
hence D in B +^ C by A14,ORDINAL1:12;
end;
C is limit_ordinal by A9,ORDINAL1:29;
then A+^C = sup fi by A8,A10,Th29
.= sup rng fi;
hence thesis by A11,Th20;
end;
now
assume
A15: C = 0;
then A +^ C = A by Th27;
hence thesis by A1,A15,Th27;
end;
hence thesis by A4,A7;
end;
for C holds P[C] from ORDINAL1:sch 2(A2);
hence thesis;
end;
theorem Th35:
0*^A = 0
proof
deffunc D(Ordinal,Sequence) = union sup $2;
deffunc F(Ordinal) = $1*^A;
deffunc C(Ordinal,Ordinal) = $2+^A;
A1: for B,C holds C = F(B) iff ex fi st C = last fi & dom fi = succ B & fi.
0 = 0 & (for C st succ C in succ B holds fi.succ C = C(C,fi.C)) & for C st C
in succ B & C <> 0 & C is limit_ordinal holds fi.C = D(C,fi|C) by Def15;
thus F(0) = 0 from OSResult0(A1);
end;
theorem Th36:
(succ B)*^A = B*^A +^ A
proof
deffunc D(Ordinal,Sequence) = union sup $2;
deffunc F(Ordinal) = $1*^A;
deffunc C(Ordinal,Ordinal) = $2 +^ A;
A1: for B,C holds C = F(B) iff ex fi st C = last fi & dom fi = succ B & fi.
0 = 0 & (for C st succ C in succ B holds fi.succ C = C(C,fi.C)) & for C st C
in succ B & C <> 0 & C is limit_ordinal holds fi.C = D(C,fi|C) by Def15;
for B holds F(succ B) = C(B,F(B)) from OSResultS(A1);
hence thesis;
end;
theorem Th37:
B <> 0 & B is limit_ordinal implies for fi st dom fi = B & for
C st C in B holds fi.C = C*^A holds B*^A = union sup fi
proof
deffunc D(Ordinal,Ordinal-Sequence) = union sup $2;
assume
A1: B <> 0 & B is limit_ordinal;
deffunc C(Ordinal,Ordinal) = $2+^A;
deffunc F(Ordinal) = $1*^A;
let fi such that
A2: dom fi = B and
A3: for C st C in B holds fi.C = F(C);
A4: for B,C holds C = F(B) iff ex fi st C = last fi & dom fi = succ B & fi.
0 = 0 & (for C st succ C in succ B holds fi.succ C = C(C,fi.C)) & for C st C
in succ B & C <> 0 & C is limit_ordinal holds fi.C = D(C,fi|C) by Def15;
thus F(B) = D(B,fi) from OSResultL(A4,A1,A2,A3);
end;
theorem Th38:
A*^0 = 0
proof
defpred P[Ordinal] means $1*^0 = 0;
A1: for A st P[A] holds P[succ A]
proof
let A;
assume A*^0 = 0;
hence (succ A)*^0 = 0+^0 by Th36
.= 0 by Th27;
end;
A2: for A st A <> 0 & A is limit_ordinal & for B st B in A holds P[B] holds
P[A]
proof
deffunc F(Ordinal) = $1*^0;
let A;
assume that
A3: A <> 0 and
A4: A is limit_ordinal and
A5: for B st B in A holds B*^0 = 0;
consider fi such that
A6: dom fi = A & for B st B in A holds fi.B = F(B) from OSLambda;
rng fi = succ 0
proof
thus for x being object holds x in rng fi implies x in succ 0
proof let x be object;
assume x in rng fi;
then consider y being object such that
A7: y in dom fi and
A8: x = fi.y by FUNCT_1:def 3;
reconsider y as Ordinal by A7;
x = y*^0 by A6,A7,A8
.= 0 by A5,A6,A7;
hence thesis by TARSKI:def 1;
end;
let x be object;
assume x in succ 0;
then
A9: x = 0 by TARSKI:def 1;
0 c= A;
then
A10: 0 c< A by A3;
then
A11: 0 in A by ORDINAL1:11;
0 *^ 0 = 0 by Th35;
then fi.x = x by A6,A10,A9,ORDINAL1:11;
hence thesis by A6,A11,A9,FUNCT_1:def 3;
end;
then
A12: sup rng fi = succ 0 by Th18;
A*^0 = union sup fi by A3,A4,A6,Th37
.= union sup rng fi;
hence thesis by A12,Th2;
end;
A13: P[0] by Th35;
for A holds P[A] from OrdinalInd(A13,A1,A2);
hence thesis;
end;
theorem Th39:
1*^A = A & A*^1 = A
proof
defpred P[Ordinal] means $1*^succ 0 = $1;
thus 1*^A = 0*^A +^ A by Lm1,Th36
.= 0 +^ A by Th35
.= A by Th30;
A1: for A st for B st B in A holds P[B] holds P[A]
proof
let A such that
A2: for B st B in A holds B*^(succ 0) = B;
A3: now
deffunc F(Ordinal) = $1*^succ 0;
assume that
A4: A <> 0 and
A5: for B holds A <> succ B;
consider fi such that
A6: dom fi = A & for D st D in A holds fi.D = F(D) from OSLambda;
A7: A = rng fi
proof
thus A c= rng fi
proof
let x be object;
assume
A8: x in A;
then reconsider B = x as Ordinal;
x = B*^succ 0 by A2,A8
.= fi.x by A6,A8;
hence thesis by A6,A8,FUNCT_1:def 3;
end;
let x be object;
assume x in rng fi;
then consider y being object such that
A9: y in dom fi and
A10: x = fi.y by FUNCT_1:def 3;
reconsider y as Ordinal by A9;
fi.y = y*^succ 0 by A6,A9
.= y by A2,A6,A9;
hence thesis by A6,A9,A10;
end;
A11: A is limit_ordinal by A5,ORDINAL1:29;
then A*^succ 0 = union sup fi by A4,A6,Th37
.= union sup rng fi;
hence A*^succ 0 = union A by A7,Th18
.= A by A11;
end;
now
given B such that
A12: A = succ B;
thus A*^(succ 0) = B*^(succ 0) +^ succ 0 by A12,Th36
.= B +^ succ 0 by A2,A12,ORDINAL1:6
.= succ(B +^ 0) by Th28
.= A by A12,Th27;
end;
hence thesis by A3,Th35;
end;
for A holds P[A] from ORDINAL1:sch 2(A1);
hence thesis;
end;
theorem Th40:
C <> 0 & A in B implies A*^C in B*^C
proof
A1: 0 c= C;
defpred P[Ordinal] means A in $1 implies A*^C in $1*^C;
assume C <> 0;
then
A2: 0 c< C by A1;
then
A3: 0 in C by ORDINAL1:11;
A4: for B st for D st D in B holds P[D] holds P[B]
proof
let B such that
A5: for D st D in B holds A in D implies A *^ C in D *^ C and
A6: A in B;
A7: now
given D such that
A8: B = succ D;
A9: now
assume A in D;
then
A10: A*^C in D*^C by A5,A8,ORDINAL1:6;
A11: D*^C +^ 0 in D*^C +^ C by A2,Th32,ORDINAL1:11;
D*^C +^ C = (succ D)*^C & D*^C +^ 0 = D*^C by Th27,Th36;
hence thesis by A8,A10,A11,ORDINAL1:10;
end;
now
A12: A*^C +^ 0 = A*^C by Th27;
assume
A13: not A in D;
A c< D iff A c= D & A <> D;
then A*^C +^ 0 in D*^C +^ C by A3,A6,A8,A13,Th32,ORDINAL1:11,22;
hence thesis by A8,A12,Th36;
end;
hence thesis by A9;
end;
now
A14: A*^C +^ 0 = A*^C & A*^C +^ 0 in A*^C +^ C by A2,Th27,Th32,ORDINAL1:11;
A15: (succ A)*^C = A*^C +^ C by Th36;
deffunc F(Ordinal) = $1*^C;
consider fi such that
A16: dom fi = B & for D st D in B holds fi.D = F(D) from OSLambda;
assume for D holds B <> succ D;
then
A17: B is limit_ordinal by ORDINAL1:29;
then
A18: succ A in B by A6,ORDINAL1:28;
then fi.(succ A) = (succ A)*^C by A16;
then (succ A)*^C in rng fi by A16,A18,FUNCT_1:def 3;
then
A19: (succ A)*^C c= union sup rng fi by Th19,ZFMISC_1:74;
B*^C = union sup fi by A6,A17,A16,Th37
.= union sup rng fi;
hence thesis by A19,A14,A15;
end;
hence thesis by A7;
end;
for B holds P[B] from ORDINAL1:sch 2(A4);
hence thesis;
end;
theorem
A c= B implies A*^C c= B*^C
proof
assume
A1: A c= B;
A2: now
assume
A3: C <> 0;
now
assume A <> B;
then A c< B by A1;
then A*^C in B*^C by A3,Th40,ORDINAL1:11;
hence thesis by ORDINAL1:def 2;
end;
hence thesis;
end;
C = 0 implies thesis by Th38;
hence thesis by A2;
end;
theorem
A c= B implies C*^A c= C*^B
proof
assume
A1: A c= B;
now
defpred P[Ordinal] means $1*^A c= $1*^B;
assume
A2: B <> 0;
A3: for C st for D st D in C holds P[D] holds P[C]
proof
let C such that
A4: for D st D in C holds D*^A c= D*^B;
A5: now
given D such that
A6: C = succ D;
D*^A c= D*^B by A4,A6,ORDINAL1:6;
then
A7: D*^A +^ A c= D*^B +^ A by Th34;
A8: C*^A = D*^A +^ A & C*^B = D*^B +^ B by A6,Th36;
D*^B +^ A c= D*^B +^ B by A1,Th33;
hence thesis by A7,A8,XBOOLE_1:1;
end;
A9: now
deffunc F(Ordinal) = $1*^A;
assume that
A10: C <> 0 and
A11: for D holds C <> succ D;
consider fi such that
A12: dom fi = C & for D st D in C holds fi.D = F(D) from OSLambda;
now
let D;
assume D in rng fi;
then consider x being object such that
A13: x in dom fi and
A14: D = fi.x by FUNCT_1:def 3;
reconsider x as Ordinal by A13;
A15: x*^B in C*^B by A2,A12,A13,Th40;
D = x*^A & x*^A c= x*^B by A4,A12,A13,A14;
hence D in C*^B by A15,ORDINAL1:12;
end;
then
A16: sup rng fi c= C*^B by Th20;
C is limit_ordinal by A11,ORDINAL1:29;
then
A17: C*^A = union sup fi by A10,A12,Th37
.= union sup rng fi;
union sup rng fi c= sup rng fi by Th5;
hence thesis by A17,A16,XBOOLE_1:1;
end;
now
assume C = 0;
then C*^A = 0 by Th35;
hence thesis;
end;
hence thesis by A5,A9;
end;
for C holds P[C] from ORDINAL1:sch 2(A3);
hence thesis;
end;
hence thesis by A1;
end;
theorem Th43:
exp(A,0) = 1
proof
deffunc D(Ordinal,Ordinal-Sequence) = lim $2;
deffunc F(Ordinal) = exp(A,$1);
deffunc C(Ordinal,Ordinal) = A*^$2;
A1: for B,C holds C = F(B) iff ex fi st C = last fi & dom fi = succ B & fi.
0 = 1 & (for C st succ C in succ B holds fi.succ C = C(C,fi.C)) & for C st C
in succ B & C <> 0 & C is limit_ordinal holds fi.C = D(C,fi|C) by Def16;
thus F(0) = 1 from OSResult0(A1);
end;
theorem Th44:
exp(A,succ B) = A*^exp(A,B)
proof
deffunc D(Ordinal,Ordinal-Sequence) = lim $2;
deffunc F(Ordinal) = exp(A,$1);
deffunc C(Ordinal,Ordinal) = A *^ $2;
A1: for B,C holds C = F(B) iff ex fi st C = last fi & dom fi = succ B & fi.
0 = 1 & (for C st succ C in succ B holds fi.succ C = C(C,fi.C)) & for C st C
in succ B & C <> 0 & C is limit_ordinal holds fi.C = D(C,fi|C) by Def16;
for B holds F(succ B) = C(B,F(B)) from OSResultS(A1);
hence thesis;
end;
theorem Th45:
B <> 0 & B is limit_ordinal implies for fi st dom fi = B & for
C st C in B holds fi.C = exp(A,C) holds exp(A,B) = lim fi
proof
deffunc D(Ordinal,Ordinal-Sequence) = lim $2;
assume
A1: B <> 0 & B is limit_ordinal;
deffunc C(Ordinal,Ordinal) = A*^$2;
deffunc F(Ordinal) = exp(A,$1);
let fi such that
A2: dom fi = B and
A3: for C st C in B holds fi.C = F(C);
A4: for B,C holds C = F(B) iff ex fi st C = last fi & dom fi = succ B & fi.
0 = 1 & (for C st succ C in succ B holds fi.succ C = C(C,fi.C)) & for C st C
in succ B & C <> 0 & C is limit_ordinal holds fi.C = D(C,fi|C) by Def16;
thus F(B) = D(B,fi) from OSResultL(A4,A1,A2,A3);
end;
theorem
exp(A,1) = A & exp(1,A) = 1
proof
defpred P[Ordinal] means exp(1,$1) = 1;
A1: for A st P[A] holds P[succ A]
proof
let A;
assume exp(1,A) = 1;
hence exp(1,succ A) = 1*^1 by Th44
.= 1 by Th39;
end;
thus exp(A,1) = A*^exp(A,0) by Lm1,Th44
.= A*^1 by Th43
.= A by Th39;
A2: for A st A <> 0 & A is limit_ordinal & for B st B in A holds P[B] holds
P[A]
proof
deffunc F(Ordinal) = exp(1,$1);
let A such that
A3: A <> 0 and
A4: A is limit_ordinal and
A5: for B st B in A holds exp(1,B) = 1;
consider fi such that
A6: dom fi = A & for B st B in A holds fi.B = F(B) from OSLambda;
A7: rng fi c= { 1 }
proof
let x be object;
assume x in rng fi;
then consider y being object such that
A8: y in dom fi and
A9: x = fi.y by FUNCT_1:def 3;
reconsider y as Ordinal by A8;
x = exp(1,y) by A6,A8,A9
.= 1 by A5,A6,A8;
hence thesis by TARSKI:def 1;
end;
now
set x = the Element of A;
thus 0 <> 1;
let B,C such that
A10: B in 1 & 1 in C;
reconsider x as Ordinal;
take D = x;
thus D in dom fi by A3,A6;
let E be Ordinal;
assume that
D c= E and
A11: E in dom fi;
fi.E in rng fi by A11,FUNCT_1:def 3;
hence B in fi.E & fi.E in C by A7,A10,TARSKI:def 1;
end;
then
A12: 1 is_limes_of fi by Def9;
exp(1,A) = lim fi by A3,A4,A6,Th45;
hence thesis by A12,Def10;
end;
A13: P[0] by Th43;
for A holds P[A] from OrdinalInd(A13,A1,A2);
hence thesis;
end;
theorem
for A ex B,C st B is limit_ordinal & C is natural & A = B +^ C
proof
defpred Th[Ordinal] means
ex A1,A2 st A1 is limit_ordinal & A2 is natural & $1 = A1 +^ A2;
A1: for A st for B st B in A holds Th[B] holds Th[A]
proof
let A such that
A2: for B st B in A holds Th[B];
A3: (ex B st A = succ B) implies Th[A]
proof
given B such that
A4: A = succ B;
consider C,D such that
A5: C is limit_ordinal and
A6: D is natural and
A7: B = C +^ D by A2,A4,ORDINAL1:6;
take C, E = succ D;
thus C is limit_ordinal by A5;
thus E in omega by A6,ORDINAL1:def 12;
thus thesis by A4,A7,Th28;
end;
(for B holds A <> succ B) implies Th[A]
proof
assume
A8: for D holds A <> succ D;
take B = A, C = 0;
thus B is limit_ordinal by A8,ORDINAL1:29;
thus C in omega by ORDINAL1:def 11;
thus thesis by Th27;
end;
hence thesis by A3;
end;
thus for A holds Th[A] from ORDINAL1:sch 2(A1);
end;
:: 2005.05.04, A.T.
registration
let X be set, o be Ordinal;
cluster X --> o -> Ordinal-yielding;
coherence
proof
rng(X --> o) c= {o} & {o} c= succ o by FUNCOP_1:13,XBOOLE_1:7;
then rng(X --> o) c= succ o;
hence thesis;
end;
end;
registration
let O be Ordinal, x be object;
cluster O --> x -> Sequence-like;
coherence;
end;
:: from ZFREFLE1, 2007.03.14, A.T.
definition
let A,B be Ordinal;
pred A is_cofinal_with B means
ex xi being Ordinal-Sequence st dom xi = B &
rng xi c= A & xi is increasing & A = sup xi;
reflexivity
proof
let A;
A1: dom id A = A by RELAT_1:45;
then reconsider xi = id A as Sequence by ORDINAL1:def 7;
A2: rng id A = A by RELAT_1:45;
then reconsider xi as Ordinal-Sequence by Def4;
take xi;
thus dom xi = A & rng xi c= A by RELAT_1:45;
thus xi is increasing
proof
let B,C;
assume that
A3: B in C and
A4: C in dom xi;
xi.C = C by A1,A4,FUNCT_1:18;
hence thesis by A1,A3,A4,FUNCT_1:18,ORDINAL1:10;
end;
thus thesis by A2,Th18;
end;
end;
reserve e,u for set;
theorem Th48:
e in rng psi implies e is Ordinal
proof
assume e in rng psi;
then ex u being object st u in dom psi & e = psi.u by FUNCT_1:def 3;
hence thesis;
end;
theorem
rng psi c= sup psi
proof
let e be object;
assume
A1: e in rng psi;
then e is Ordinal by Th48;
hence thesis by A1,Th19;
end;
theorem
A is_cofinal_with 0 implies A = 0
proof
given psi such that
A1: dom psi = 0 and
rng psi c= A and
psi is increasing and
A2: A = sup psi;
thus A = sup 0 by A1,A2,RELAT_1:42
.= 0 by Th18;
end;
:: from ARYTM_3, 2007.10.23, A.T.
scheme
OmegaInd {a()-> Nat, P[object]}:
P[a()]
provided
A1: P[0] and
A2: for a being Nat st P[a] holds P[succ a]
proof
defpred P[Ordinal] means $1 is natural implies P[$1];
A3: now
let A;
assume
A4: P[A];
now
assume succ A is natural;
then
A5: succ A in omega;
A in succ A by ORDINAL1:6;
then A is Element of omega by A5,ORDINAL1:10;
hence P[succ A] by A2,A4;
end;
hence P[succ A];
end;
A6: now
let A;
assume
A7: A <> 0;
0 c= A;
then 0 c< A by A7;
then
A8: 0 in A by ORDINAL1:11;
A9: not A in A;
assume A is limit_ordinal;
then omega c= A by A8,ORDINAL1:def 11;
then not A in omega by A9;
hence (for B st B in A holds P[B]) implies P[A] by ORDINAL1:def 12;
end;
A10: P[0] by A1;
for A holds P[A] from OrdinalInd(A10,A3,A6);
hence thesis;
end;
registration
let a, b be Nat;
cluster a +^ b -> natural;
coherence
proof
defpred P[Nat] means a+^$1 is natural;
A1: now
let b be Nat;
assume P[b];
then reconsider c = a+^b as Nat;
a+^succ b = succ c by Th28;
hence P[succ b];
end;
A2: P[0] by Th27;
thus P[b] from OmegaInd(A2,A1);
end;
end;
:: from AMI_2, 2008.02.14, A.T.
registration
let x,y be set, a,b be Nat;
cluster IFEQ(x,y,a,b) -> natural;
coherence
proof
per cases;
suppose
x = y;
hence thesis by FUNCOP_1:def 8;
end;
suppose
x <> y;
hence thesis by FUNCOP_1:def 8;
end;
end;
end;
:: 2010.03.16, A.T.
scheme LambdaRecEx{A() -> set,G(set,set) -> set}:
ex f being Function st dom f = omega & f.0 = A() &
for n being Nat holds f.succ n = G(n,f.n)
proof
deffunc D(set,set) = 0;
consider L being Sequence such that
A1: dom L = omega and
A2: 0 in omega implies L.0 = A() and
A3: for A being Ordinal st succ A in omega holds L.(succ A) = G(A,L.A) and
for A being Ordinal st A in omega & A <> 0 & A is limit_ordinal holds L.A
= D(A,L|A) from TSExist1;
take L;
thus dom L = omega by A1;
0 in omega by ORDINAL1:def 12;
hence L.0 = A() by A2;
let n be Nat;
succ n in omega by ORDINAL1:def 12;
hence thesis by A3;
end;
reserve n for Nat;
scheme RecUn{A() -> set, F, G() -> Function, P[set,set,set]}:
F() = G()
provided
A1: dom F() = omega and
A2: F().0 = A() and
A3: for n holds P[n,F().n,F().(succ n)] and
A4: dom G() = omega and
A5: G().0 = A() and
A6: for n holds P[n,G().n,G().(succ n)] and
A7: for n for x,y1,y2 being set st P[n,x,y1] & P[n,x,y2] holds y1 = y2
proof
defpred P[Nat] means F().$1 = G().$1;
A8: for n st P[n] holds P[succ n]
proof
let n;
assume F().n = G().n;
then
A9: P[n,F().n,G().(succ n)] by A6;
P[n,F().n,F().(succ n)] by A3;
hence thesis by A7,A9;
end;
A10: P[0] by A2,A5;
for n holds P[n] proof let n;
thus thesis from OmegaInd(A10,A8);
end;
then for x being object st x in omega holds F().x = G().x;
hence thesis by A1,A4,FUNCT_1:2;
end;
scheme LambdaRecUn{A() -> set, F(set,set) -> set, F, G() -> Function}:
F() = G()
provided
A1: dom F() = omega and
A2: F().0 = A() and
A3: for n holds F().(succ n) = F(n,F().n) and
A4: dom G() = omega and
A5: G().0 = A() and
A6: for n holds G().(succ n) = F(n,G().n)
proof
defpred P[Nat,set,set] means $3=F($1,$2);
A7: for n holds P[n,G().n,G().(succ n)] by A6;
A8: for n being Nat,x,y1,y2 being set st P[n,x,y1] & P[n,x,y2]
holds y1=y2;
A9: for n holds P[n,F().n,F().(succ n)] by A3;
thus F() = G() from RecUn(A1,A2,A9,A4,A5,A7,A8);
end;