:: Increasing and Continuous Ordinal Sequences
:: by Grzegorz Bancerek
::
:: Received May 31, 1990
:: 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 ORDINAL2, ORDINAL1, FUNCT_1, XBOOLE_0, RELAT_1, TARSKI, ORDINAL3,
SUBSET_1, CLASSES2, ZFMISC_1, CARD_1, ORDINAL4;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2,
ORDINAL1, ORDINAL2, ORDINAL3, CARD_1, CLASSES2;
constructors WELLORD2, FUNCOP_1, ORDINAL3, CARD_1, CLASSES1, CLASSES2,
RELSET_1;
registrations XBOOLE_0, FUNCT_1, ORDINAL1, ORDINAL2, ORDINAL3, CARD_1,
CLASSES2, RELSET_1;
requirements SUBSET, BOOLE, NUMERALS;
definitions ORDINAL1, TARSKI, ORDINAL2, XBOOLE_0, RELAT_1;
equalities ORDINAL1, ORDINAL2;
expansions TARSKI, ORDINAL2, XBOOLE_0;
theorems ZFMISC_1, FUNCT_1, GRFUNC_1, ORDINAL1, ORDINAL2, ORDINAL3, CARD_2,
CLASSES2, RELAT_1, CLASSES1, XBOOLE_0, XBOOLE_1, FUNCT_2, RELSET_1,
CARD_1;
schemes ORDINAL1, ORDINAL2, FINSET_1;
begin
reserve phi,fi,psi for Ordinal-Sequence,
A,A1,B,C,D for Ordinal,
f,g for Function,
X for set,
x,y,z for object;
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;
end;
theorem
dom fi = succ A implies last fi is_limes_of fi & lim fi = last fi
proof
assume
A1: dom fi = succ A;
then
A2: last fi = fi.A by ORDINAL2:6;
thus last fi is_limes_of fi
proof
per cases;
case
A3: last fi = 0;
take A;
thus A in dom fi by A1,ORDINAL1:6;
let B;
assume that
A4: A c= B and
A5: B in dom fi;
B c= A by A1,A5,ORDINAL1:22;
hence thesis by A2,A3,A4,XBOOLE_0:def 10;
end;
case
last fi <> 0;
let B,C such that
A6: B in last fi and
A7: last fi in C;
take A;
thus A in dom fi by A1,ORDINAL1:6;
let D;
assume that
A8: A c= D and
A9: D in dom fi;
D c= A by A1,A9,ORDINAL1:22;
hence thesis by A2,A6,A7,A8,XBOOLE_0:def 10;
end;
end;
hence thesis by ORDINAL2:def 10;
end;
definition
let fi,psi be Sequence;
func fi^psi -> Sequence means
: Def1:
dom it = (dom fi)+^(dom psi) &
(for A st A in dom fi holds it.A = fi.A) &
for A st A in dom psi holds it.((dom fi)+^A) = psi.A;
existence
proof
defpred P[set] means $1 in dom fi;
deffunc G(Ordinal) = psi.(($1)-^dom fi);
deffunc F(set) = fi.$1;
consider f such that
A1: dom f = (dom fi)+^(dom psi) and
A2: for x being Ordinal st x in (dom fi)+^(dom psi) holds (P[x]
implies f.x = F(x)) & (not P[x] implies f.x = G(x)) from FINSET_1:sch 1;
reconsider f as Sequence by A1,ORDINAL1:def 7;
take f;
thus dom f = (dom fi)+^(dom psi) by A1;
thus for A st A in dom fi holds f.A = fi.A
proof
A3: dom fi c= dom f by A1,ORDINAL3:24;
let A;
assume A in dom fi;
hence thesis by A1,A2,A3;
end;
let A;
dom fi c= (dom fi)+^A by ORDINAL3:24;
then
A4: not (dom fi)+^A in dom fi by ORDINAL1:5;
assume A in dom psi;
then (dom fi)+^A in dom f by A1,ORDINAL2:32;
then f.((dom fi)+^A) = psi.((((dom fi)+^A))-^dom fi) by A1,A2,A4;
hence thesis by ORDINAL3:52;
end;
uniqueness
proof
let f1,f2 be Sequence such that
A5: dom f1 = (dom fi)+^(dom psi) and
A6: for A st A in dom fi holds f1.A = fi.A and
A7: for A st A in dom psi holds f1.((dom fi)+^A) = psi.A and
A8: dom f2 = (dom fi)+^(dom psi) and
A9: for A st A in dom fi holds f2.A = fi.A and
A10: for A st A in dom psi holds f2.((dom fi)+^A) = psi.A;
now
let x be object;
assume
A11: x in (dom fi)+^(dom psi);
then reconsider A = x as Ordinal;
now
per cases;
suppose
A12: x in dom fi;
then f1.A = fi.A by A6;
hence f1.x = f2.x by A9,A12;
end;
suppose
not x in dom fi;
then dom fi c= A by ORDINAL1:16;
then
A13: (dom fi)+^(A-^dom fi) = A by ORDINAL3:def 5;
then f1.A = psi.(A-^dom fi) by A7,A11,ORDINAL3:22;
hence f1.x = f2.x by A10,A11,A13,ORDINAL3:22;
end;
end;
hence f1.x = f2.x;
end;
hence thesis by A5,A8,FUNCT_1:2;
end;
end;
Th2Lem:
for fi, psi being Sequence holds rng(fi^psi) c= rng fi \/ rng psi
proof
let fi,psi be Sequence;
set f = fi^psi, A1 = rng fi, A2 = rng psi;
A1: dom(fi^psi) = (dom fi)+^(dom psi) by Def1;
let y be object;
assume y in rng f;
then consider x being object such that
A2: x in dom f and
A3: y = f.x by FUNCT_1:def 3;
reconsider x as Ordinal by A2;
per cases;
suppose
A4: x in dom fi;
then
A5: fi.x in rng fi by FUNCT_1:def 3;
y = fi.x by A3,A4,Def1;
then y in A1 by A5;
hence thesis by XBOOLE_0:def 3;
end;
suppose
not x in dom fi;
then dom fi c= x by ORDINAL1:16;
then
A6: (dom fi)+^(x-^dom fi) = x by ORDINAL3:def 5;
then
A7: x-^dom fi in dom psi by A1,A2,ORDINAL3:22;
then y = psi.(x-^dom fi) by A3,A6,Def1;
then y in rng psi by A7,FUNCT_1:def 3;
then y in A2;
hence thesis by XBOOLE_0:def 3;
end;
end;
Th7A:
for A, B being Sequence holds rng A c= rng(A^B)
proof
let A, B be Sequence;
let y be object;
assume y in rng A;
then consider x being object such that
A1: x in dom A & A.x = y by FUNCT_1:def 3;
A2: (A^B).x = y by A1, Def1;
dom A c= dom A +^ dom B by ORDINAL3:24;
then dom A c= dom(A^B) by Def1;
hence y in rng(A^B) by A1, A2, FUNCT_1:3;
end;
Th8A:
for A, B being Sequence holds rng B c= rng(A^B)
proof
let A, B be Sequence;
let y be object;
assume y in rng B;
then consider x being object such that
A1: x in dom B & B.x = y by FUNCT_1:def 3;
reconsider x as Ordinal by A1;
A2: (A^B).(dom A +^ x) = y by A1, Def1;
dom A +^ x in dom A +^ dom B by A1, ORDINAL2:32;
then dom A +^ x in dom(A^B) by Def1;
hence y in rng(A^B) by A2, FUNCT_1:3;
end;
theorem Th2:
for A, B being Sequence holds rng(A^B) = rng A \/ rng B
proof
let A, B be Sequence;
rng A c= rng(A^B) & rng B c= rng(A^B) by Th7A, Th8A;
then A1: rng A \/ rng B c= rng(A^B) by XBOOLE_1:8;
rng(A^B) c= rng A \/ rng B by Th2Lem;
hence thesis by A1;
end;
registration
let fi,psi;
cluster fi^psi -> Ordinal-yielding;
coherence
proof
set f = fi^psi;
consider A1 being Ordinal such that
A1: rng fi c= A1 by ORDINAL2:def 4;
consider A2 being Ordinal such that
A2: rng psi c= A2 by ORDINAL2:def 4;
A3: A2 c= A1+^A2 by ORDINAL3:24;
A1 c= A1+^A2 by ORDINAL3:24;
then
A4: A1 \/ A2 c= A1+^A2 by A3,XBOOLE_1:8;
A5: rng f c= rng fi \/ rng psi by Th2;
rng fi \/ rng psi c= A1 \/ A2 by A1,A2,XBOOLE_1:13;
then rng f c= A1 \/ A2 by A5;
then rng f c= A1+^A2 by A4;
hence thesis;
end;
end;
theorem Th3:
A is_limes_of psi implies A is_limes_of fi^psi
proof
assume that
A1: A = 0 & (ex B st B in dom psi & for C st B c= C & C in dom psi
holds psi.C = 0) or A <> 0 & for B,C st B in A & A in C ex D st D in dom psi
& for E being Ordinal st D c= E & E in dom psi holds B in psi.E & psi.E in C;
A2: dom(fi^psi) = (dom fi)+^(dom psi) by Def1;
per cases;
case
A = 0;
then consider B such that
A3: B in dom psi and
A4: for C st B c= C & C in dom psi holds psi.C = {} by A1;
take B1 = (dom fi)+^B;
thus B1 in dom(fi^psi) by A2,A3,ORDINAL2:32;
let C;
assume that
A5: B1 c= C and
A6: C in dom(fi^psi);
A7: C = B1+^(C-^B1) by A5,ORDINAL3:def 5
.= (dom fi)+^(B+^(C-^B1)) by ORDINAL3:30;
then
A8: B+^(C-^B1) in dom psi by A2,A6,ORDINAL3:22;
B c= B+^(C-^B1) by ORDINAL3:24;
then psi.(B+^(C-^B1)) = {} by A2,A4,A6,A7,ORDINAL3:22;
hence thesis by A7,A8,Def1;
end;
case
A <> 0;
let B,C;
assume that
A9: B in A and
A10: A in C;
consider D such that
A11: D in dom psi and
A12: for E being Ordinal st D c= E & E in dom psi holds B in psi.E &
psi.E in C by A1,A9,A10;
take D1 = (dom fi)+^D;
thus D1 in dom(fi^psi) by A2,A11,ORDINAL2:32;
let E be Ordinal;
assume that
A13: D1 c= E and
A14: E in dom(fi^psi);
A15: D c= D+^(E-^D1) by ORDINAL3:24;
A16: E = D1+^(E-^D1) by A13,ORDINAL3:def 5
.= (dom fi)+^(D+^(E-^D1)) by ORDINAL3:30;
then
A17: D+^(E-^D1) in dom psi by A2,A14,ORDINAL3:22;
then (fi^psi).E = psi.(D+^(E-^D1)) by A16,Def1;
hence thesis by A12,A15,A17;
end;
end;
theorem
A is_limes_of fi implies B+^A is_limes_of B+^fi
proof
assume that
A1: A = 0 & (ex B st B in dom fi & for C st B c= C & C in dom fi holds
fi.C = 0) or A <> 0 & 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;
A2: dom fi = dom(B+^fi) by ORDINAL3:def 1;
per cases;
case
A3: B+^A = 0;
then consider A1 such that
A4: A1 in dom fi and
A5: for C st A1 c= C & C in dom fi holds fi.C = {} by A1,ORDINAL3:26;
take A1;
thus A1 in dom(B+^fi) by A4,ORDINAL3:def 1;
let C;
assume that
A6: A1 c= C and
A7: C in dom(B+^fi);
A8: (B+^fi).C = B+^(fi.C) by A2,A7,ORDINAL3:def 1;
fi.C = {} by A2,A5,A6,A7;
hence thesis by A3,A8,ORDINAL3:26;
end;
case
B+^A <> 0;
now
per cases;
suppose
A9: A = {};
then consider A1 such that
A10: A1 in dom fi and
A11: for C st A1 c= C & C in dom fi holds fi.C = {} by A1;
let B1,B2 be Ordinal such that
A12: B1 in B+^A and
A13: B+^A in B2;
take A1;
thus A1 in dom(B+^fi) by A10,ORDINAL3:def 1;
let C;
assume that
A14: A1 c= C and
A15: C in dom(B+^fi);
(B+^fi).C = B+^(fi.C) by A2,A15,ORDINAL3:def 1;
hence B1 in (B+^fi).C & (B+^fi).C in B2 by A2,A9,A11,A12,A13,A14,A15;
end;
suppose
A16: A <> {};
let B1,B2 be Ordinal;
assume that
A17: B1 in B+^A and
A18: B+^A in B2;
B1-^B in A by A16,A17,ORDINAL3:60;
then consider A1 such that
A19: A1 in dom fi and
A20: for C st A1 c= C & C in dom fi holds B1-^B in fi.C & fi.C in
B2-^B by A1,A18,ORDINAL3:61;
A21: B1 c= B+^(B1-^B) by ORDINAL3:62;
A22: B c= B+^A by ORDINAL3:24;
B+^A c= B2 by A18,ORDINAL1:def 2;
then B c= B2 by A22;
then
A23: B+^(B2-^B) = B2 by ORDINAL3:def 5;
take A1;
thus A1 in dom(B+^fi) by A19,ORDINAL3:def 1;
let C;
assume that
A24: A1 c= C and
A25: C in dom(B+^fi);
A26: (B+^fi).C = B+^(fi.C) by A2,A25,ORDINAL3:def 1;
reconsider E = fi.C as Ordinal;
B1-^B in E by A2,A20,A24,A25;
then
A27: B+^(B1-^B) in B+^E by ORDINAL2:32;
E in B2-^B by A2,A20,A24,A25;
hence B1 in (B+^fi).C & (B+^fi).C in B2 by A21,A26,A23,A27,ORDINAL1:12
,ORDINAL2:32;
end;
end;
hence thesis;
end;
end;
Lm4: A is_limes_of fi implies dom fi <> {}
proof
assume that
A1: A = 0 & (ex B st B in dom fi & for C st B c= C & C in dom fi holds
fi.C = 0) or A <> 0 & 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;
now
per cases;
suppose
A = {};
hence thesis by A1;
end;
suppose
A <> {};
then {} in A by ORDINAL3:8;
then
ex B st B in dom fi & for C st B c= C & C in dom fi holds {} in fi.C
& fi.C in succ A by A1,ORDINAL1:6;
hence thesis;
end;
end;
hence thesis;
end;
theorem Th5:
A is_limes_of fi implies A*^B is_limes_of fi*^B
proof
A1: dom fi = dom(fi*^B) by ORDINAL3:def 4;
assume
A2: A is_limes_of fi;
then
A3: dom fi <> {} by Lm4;
per cases;
case
A*^B = 0;
then
A4: B = {} or A = {} by ORDINAL3:31;
now
per cases;
suppose
A5: B = {};
set x = the Element of dom fi;
reconsider x as Ordinal;
take A1 = x;
thus A1 in dom(fi*^B) by A1,A3;
let C;
assume that
A1 c= C and
A6: C in dom(fi*^B);
thus (fi*^B).C = (fi.C)*^B by A1,A6,ORDINAL3:def 4
.= {} by A5,ORDINAL2:38;
end;
suppose
B <> {};
then consider A1 such that
A7: A1 in dom fi and
A8: for C st A1 c= C & C in dom fi holds fi.C = {} by A2,A4,ORDINAL2:def 9;
take A1;
thus A1 in dom(fi*^B) by A7,ORDINAL3:def 4;
let C;
assume that
A9: A1 c= C and
A10: C in dom(fi*^B);
A11: (fi*^B).C = (fi.C)*^B by A1,A10,ORDINAL3:def 4;
fi.C = {} by A1,A8,A9,A10;
hence (fi*^B).C = {} by A11,ORDINAL2:35;
end;
end;
hence thesis;
end;
case
A12: A*^B <> 0;
let B1,B2 be Ordinal such that
A13: B1 in A*^B and
A14: A*^B in B2;
A15: B <> {} by A12,ORDINAL2:38;
A16: now
assume not ex A1 st A = succ A1;
then A is limit_ordinal by ORDINAL1:29;
then consider C such that
A17: C in A and
A18: B1 in C*^B by A13,ORDINAL3:41;
A in succ A by ORDINAL1:6;
then consider D such that
A19: D in dom fi and
A20: for A1 st D c= A1 & A1 in dom fi holds C in fi.A1 & fi.A1 in
succ A by A2,A17,ORDINAL2:def 9;
take D;
thus D in dom(fi*^B) by A19,ORDINAL3:def 4;
let A1;
assume that
A21: D c= A1 and
A22: A1 in dom(fi*^B);
reconsider E = fi.A1 as Ordinal;
fi.A1 in succ A by A1,A20,A21,A22;
then
A23: E c= A by ORDINAL1:22;
C in fi.A1 by A1,A20,A21,A22;
then C*^B in E*^B by A15,ORDINAL2:40;
then
A24: B1 in E*^B by A18,ORDINAL1:10;
(fi*^B).A1 = (fi.A1)*^B by A1,A22,ORDINAL3:def 4;
hence B1 in (fi*^B).A1 & (fi*^B).A1 in B2 by A14,A23,A24,ORDINAL1:12
,ORDINAL2:41;
end;
now
A25: A in succ A by ORDINAL1:6;
given A1 such that
A26: A = succ A1;
A1 in A by A26,ORDINAL1:6;
then consider D such that
A27: D in dom fi and
A28: for C st D c= C & C in dom fi holds A1 in fi.C & fi.C in succ A
by A2,A25,ORDINAL2:def 9;
take D;
thus D in dom(fi*^B) by A27,ORDINAL3:def 4;
let C;
assume that
A29: D c= C and
A30: C in dom(fi*^B);
reconsider E = fi.C as Ordinal;
A1 in E by A1,A28,A29,A30;
then
A31: A c= E by A26,ORDINAL1:21;
E in succ A by A1,A28,A29,A30;
then
A32: E c= A by ORDINAL1:22;
(fi*^B).C = E*^B by A1,A30,ORDINAL3:def 4;
hence B1 in (fi*^B).C & (fi*^B).C in B2 by A13,A14,A31,A32,
XBOOLE_0:def 10;
end;
hence thesis by A16;
end;
end;
theorem Th6:
dom fi = dom psi & B is_limes_of fi & C is_limes_of psi & ((for A
st A in dom fi holds fi.A c= psi.A) or for A st A in dom fi holds fi.A in psi.A
) implies B c= C
proof
assume that
A1: dom fi = dom psi and
A2: B = 0 & (ex A1 st A1 in dom fi & for C st A1 c= C & C in dom fi
holds fi.C = 0) or B <> 0 & for A1,C st A1 in B & B in C ex D st D in dom fi
& for E being Ordinal st D c= E & E in dom fi holds A1 in fi.E & fi.E in C
and
A3: C = 0 & (ex B st B in dom psi & for A1 st B c= A1 & A1 in dom psi
holds psi.A1 = 0) or C <> 0 & for B,A1 st B in C & C in A1 ex D st D in dom
psi & for E being Ordinal st D c= E & E in dom psi holds B in psi.E & psi.E in
A1 and
A4: (for A st A in dom fi holds fi.A c= psi.A) or for A st A in dom fi
holds fi.A in psi.A;
A5: for A st A in dom fi holds fi.A c= psi.A by A4,ORDINAL1:def 2;
now
per cases;
suppose
B = {} & C = {};
hence thesis;
end;
suppose
B = {} & C <> {};
then B in C by ORDINAL3:8;
hence thesis by ORDINAL1:def 2;
end;
suppose
A6: B <> {} & C = {};
then {} in B by ORDINAL3:8;
then consider A2 being Ordinal such that
A7: A2 in dom fi and
A8: for A st A2 c= A & A in dom fi holds {} in fi.A & fi.A in succ
B by A2,ORDINAL1:6;
consider A1 such that
A9: A1 in dom psi and
A10: for A st A1 c= A & A in dom psi holds psi.A = {} by A3,A6;
A11: A1 \/ A2 = A1 or A1 \/ A2 = A2 by ORDINAL3:12;
then
A12: fi.(A1 \/ A2) c= psi.(A1 \/ A2) by A1,A5,A9,A7;
A2 c= A1 \/ A2 by XBOOLE_1:7;
then {} in fi.(A1 \/ A2) by A1,A9,A7,A8,A11;
hence thesis by A1,A9,A10,A7,A11,A12,XBOOLE_1:7;
end;
suppose
A13: B <> {} & C <> {};
assume not B c= C;
then C in B by ORDINAL1:16;
then consider A1 such that
A14: A1 in dom fi and
A15: for A st A1 c= A & A in dom fi holds C in fi.A & fi.A in succ B
by A2,ORDINAL1:6;
{} in C by A13,ORDINAL3:8;
then consider A2 being Ordinal such that
A16: A2 in dom psi and
A17: for A st A2 c= A & A in dom psi holds {} in psi.A & psi.A in
succ C by A3,ORDINAL1:6;
A18: A1 \/ A2 = A1 or A1 \/ A2 = A2 by ORDINAL3:12;
reconsider A3 = psi.(A1 \/ A2) as Ordinal;
A2 c= A1 \/ A2 by XBOOLE_1:7;
then psi.(A1 \/ A2) in succ C by A1,A14,A16,A17,A18;
then
A19: A3 c= C by ORDINAL1:22;
A1 c= A1 \/ A2 by XBOOLE_1:7;
then
A20: C in fi.(A1 \/ A2) by A1,A14,A15,A16,A18;
fi.(A1 \/ A2) c= psi.(A1 \/ A2) by A1,A5,A14,A16,A18;
hence contradiction by A20,A19,ORDINAL1:5;
end;
end;
hence thesis;
end;
reserve f1,f2 for Ordinal-Sequence;
theorem
dom f1 = dom fi & dom fi = dom f2 & A is_limes_of f1 & A is_limes_of
f2 & (for A st A in dom fi holds f1.A c= fi.A & fi.A c= f2.A) implies A
is_limes_of fi
proof
assume that
A1: dom f1 = dom fi and
A2: dom fi = dom f2 and
A3: A = 0 & (ex B st B in dom f1 & for C st B c= C & C in dom f1 holds
f1.C = 0) or A <> 0 & for B,C st B in A & A in C ex D st D in dom f1 & for E
being Ordinal st D c= E & E in dom f1 holds B in f1.E & f1.E in C and
A4: A = 0 & (ex B st B in dom f2 & for C st B c= C & C in dom f2 holds
f2.C = 0) or A <> 0 & for B,C st B in A & A in C ex D st D in dom f2 & for E
being Ordinal st D c= E & E in dom f2 holds B in f2.E & f2.E in C and
A5: for A st A in dom fi holds f1.A c= fi.A & fi.A c= f2.A;
per cases;
case
A = 0;
then consider B being Ordinal such that
A6: B in dom f2 and
A7: for C st B c= C & C in dom f2 holds f2.C = {} by A4;
take B;
thus B in dom fi by A2,A6;
let C;
assume that
A8: B c= C and
A9: C in dom fi;
f2.C = {} by A2,A7,A8,A9;
hence thesis by A5,A9,XBOOLE_1:3;
end;
case
A <> 0;
let B,C;
assume that
A10: B in A and
A11: A in C;
consider D2 being Ordinal such that
A12: D2 in dom f2 and
A13: for A1 st D2 c= A1 & A1 in dom f2 holds B in f2.A1 & f2.A1 in C
by A4,A10,A11;
consider D1 being Ordinal such that
A14: D1 in dom f1 and
A15: for A1 st D1 c= A1 & A1 in dom f1 holds B in f1.A1 & f1.A1 in C
by A3,A10,A11;
take D = D1 \/ D2;
thus D in dom fi by A1,A2,A14,A12,ORDINAL3:12;
let A1;
assume that
A16: D c= A1 and
A17: A1 in dom fi;
reconsider B1 = fi.A1, B2 = f2.A1 as Ordinal;
A18: B1 c= B2 by A5,A17;
D2 c= D by XBOOLE_1:7;
then D2 c= A1 by A16;
then
A19: B2 in C by A2,A13,A17;
D1 c= D by XBOOLE_1:7;
then D1 c= A1 by A16;
then
A20: B in f1.A1 by A1,A15,A17;
f1.A1 c= fi.A1 by A5,A17;
hence thesis by A20,A18,A19,ORDINAL1:12;
end;
end;
theorem Th8:
dom fi <> {} & dom fi is limit_ordinal & fi is increasing implies
sup fi is_limes_of fi & lim fi = sup fi
proof
assume that
A1: dom fi <> {} & dom fi is limit_ordinal and
A2: A in B & B in dom fi implies fi.A in fi.B;
reconsider x = fi.{} as Ordinal;
{} in dom fi by A1,ORDINAL3:8;
then
A3: x in rng fi by FUNCT_1:def 3;
thus sup fi is_limes_of fi
proof
per cases;
case
sup fi = 0;
hence thesis by A3,ORDINAL2:19;
end;
case
sup fi <> 0;
let A,B;
assume that
A4: A in sup fi and
A5: sup fi in B;
consider C such that
A6: C in rng fi and
A7: A c= C by A4,ORDINAL2:21;
consider x being object such that
A8: x in dom fi and
A9: C = fi.x by A6,FUNCT_1:def 3;
reconsider x as Ordinal by A8;
take M = succ x;
thus M in dom fi by A1,A8,ORDINAL1:28;
let D;
assume that
A10: M c= D and
A11: D in dom fi;
reconsider E = fi.D as Ordinal;
x in M by ORDINAL1:6;
then C in E by A2,A9,A10,A11;
hence A in fi.D by A7,ORDINAL1:12;
fi.D in rng fi by A11,FUNCT_1:def 3;
then E in sup fi by ORDINAL2:19;
hence thesis by A5,ORDINAL1:10;
end;
end;
hence thesis by ORDINAL2:def 10;
end;
theorem Th9:
fi is increasing & A c= B & B in dom fi implies fi.A c= fi.B
proof
assume that
A1: for A,B st A in B & B in dom fi holds fi.A in fi.B and
A2: A c= B and
A3: B in dom fi;
reconsider C = fi.B as Ordinal;
now
per cases;
suppose
A = B;
hence thesis;
end;
suppose
A <> B;
then A c< B by A2;
then A in B by ORDINAL1:11;
then fi.A in C by A1,A3;
hence thesis by ORDINAL1:def 2;
end;
end;
hence thesis;
end;
theorem Th10:
fi is increasing & A in dom fi implies A c= fi.A
proof
assume that
A1: for A,B st A in B & B in dom fi holds fi.A in fi.B and
A2: A in dom fi and
A3: not A c= fi.A;
defpred P[set] means $1 in dom fi & not $1 c= fi.$1;
A4: ex A st P[A] by A2,A3;
consider A such that
A5: P[A] and
A6: for B st P[B] holds A c= B from ORDINAL1:sch 1(A4);
reconsider B = fi.A as Ordinal;
A7: B in A by A5,ORDINAL1:16;
then not B c= fi.B by A1,A5,ORDINAL1:5;
hence contradiction by A5,A6,A7,ORDINAL1:10;
end;
theorem Th11:
phi is increasing implies phi"A is epsilon-transitive epsilon-connected set
proof
assume
A1: for A,B st A in B & B in dom phi holds phi.A in phi.B;
now
let X;
assume
A2: X in phi"A;
then
A3: X in dom phi by FUNCT_1:def 7;
hence X is Ordinal;
reconsider B = X as Ordinal by A3;
A4: phi.X in A by A2,FUNCT_1:def 7;
thus X c= phi"A
proof
let x be object;
assume
A5: x in X;
then x in B;
then reconsider C = x, D = phi.B as Ordinal;
reconsider E = phi.C as Ordinal;
E in D by A1,A3,A5;
then
A6: phi.x in A by A4,ORDINAL1:10;
C in dom phi by A3,A5,ORDINAL1:10;
hence thesis by A6,FUNCT_1:def 7;
end;
end;
hence thesis by ORDINAL1:19;
end;
theorem Th12:
f1 is increasing implies f2*f1 is Ordinal-Sequence
proof
A1: dom(f2*f1) = f1"dom f2 by RELAT_1:147;
assume f1 is increasing;
then dom(f2*f1) is Ordinal by A1,Th11;
then reconsider f = f2*f1 as Sequence by ORDINAL1:def 7;
consider A such that
A2: rng f2 c= A by ORDINAL2:def 4;
rng f c= rng f2 by RELAT_1:26;
then rng f c= A by A2;
hence thesis by ORDINAL2:def 4;
end;
theorem Th13:
f1 is increasing & f2 is increasing implies ex phi st phi = f1*
f2 & phi is increasing
proof
assume that
A1: f1 is increasing and
A2: f2 is increasing;
reconsider f = f1*f2 as Ordinal-Sequence by A2,Th12;
take f;
thus f = f1*f2;
let A,B;
assume that
A3: A in B and
A4: B in dom f;
reconsider A1 = f2.A, B1 = f2.B as Ordinal;
A5: B1 in dom f1 by A4,FUNCT_1:11;
dom f c= dom f2 by RELAT_1:25;
then
A6: A1 in B1 by A2,A3,A4;
A7: f.B = f1.B1 by A4,FUNCT_1:12;
f.A = f1.A1 by A3,A4,FUNCT_1:12,ORDINAL1:10;
hence thesis by A1,A6,A5,A7;
end;
theorem Th14:
f1 is increasing & A is_limes_of f2 & sup rng f1 = dom f2 & fi =
f2*f1 implies A is_limes_of fi
proof
assume that
A1: f1 is increasing and
A2: A = 0 & (ex B st B in dom f2 & for C st B c= C & C in dom f2 holds
f2.C = 0) or A <> 0 & for B,C st B in A & A in C ex D st D in dom f2 & for E
being Ordinal st D c= E & E in dom f2 holds B in f2.E & f2.E in C and
A3: sup rng f1 = dom f2 and
A4: fi = f2*f1;
per cases;
case
A = 0;
then consider B such that
A5: B in dom f2 and
A6: for C st B c= C & C in dom f2 holds f2.C = {} by A2;
consider B1 being Ordinal such that
A7: B1 in rng f1 and
A8: B c= B1 by A3,A5,ORDINAL2:21;
consider x being object such that
A9: x in dom f1 and
A10: B1 = f1.x by A7,FUNCT_1:def 3;
reconsider x as Ordinal by A9;
take x;
B1 in dom f2 by A3,A7,ORDINAL2:19;
hence x in dom fi by A4,A9,A10,FUNCT_1:11;
let C such that
A11: x c= C and
A12: C in dom fi;
reconsider C1 = f1.C as Ordinal;
A13: dom fi c= dom f1 by A4,RELAT_1:25;
then B1 c= C1 by A1,A10,A11,A12,Th9;
then
A14: B c= C1 by A8;
C1 in rng f1 by A12,A13,FUNCT_1:def 3;
then f2.C1 = {} by A3,A6,A14,ORDINAL2:19;
hence thesis by A4,A12,FUNCT_1:12;
end;
case
A <> 0;
let B,C;
assume that
A15: B in A and
A16: A in C;
consider D such that
A17: D in dom f2 and
A18: for A1 st D c= A1 & A1 in dom f2 holds B in f2.A1 & f2.A1 in C by A2,A15
,A16;
consider B1 being Ordinal such that
A19: B1 in rng f1 and
A20: D c= B1 by A3,A17,ORDINAL2:21;
consider x being object such that
A21: x in dom f1 and
A22: B1 = f1.x by A19,FUNCT_1:def 3;
reconsider x as Ordinal by A21;
take x;
B1 in dom f2 by A3,A19,ORDINAL2:19;
hence x in dom fi by A4,A21,A22,FUNCT_1:11;
let E be Ordinal such that
A23: x c= E and
A24: E in dom fi;
reconsider E1 = f1.E as Ordinal;
A25: dom fi c= dom f1 by A4,RELAT_1:25;
then E1 in rng f1 by A24,FUNCT_1:def 3;
then
A26: E1 in dom f2 by A3,ORDINAL2:19;
B1 c= E1 by A1,A22,A23,A24,A25,Th9;
then
A27: D c= E1 by A20;
then
A28: f2.E1 in C by A18,A26;
B in f2.E1 by A18,A27,A26;
hence thesis by A4,A24,A28,FUNCT_1:12;
end;
end;
theorem Th15:
phi is increasing implies phi|A is increasing
proof
assume
A1: for A,B st A in B & B in dom phi holds phi.A in phi.B;
let B,C such that
A2: B in C and
A3: C in dom (phi|A);
A4: phi.B = (phi|A).B by A2,A3,FUNCT_1:47,ORDINAL1:10;
dom (phi|A) c= dom phi by RELAT_1:60;
then phi.B in phi.C by A1,A2,A3;
hence thesis by A3,A4,FUNCT_1:47;
end;
theorem Th16:
phi is increasing & dom phi is limit_ordinal implies sup phi is limit_ordinal
proof
assume that
A1: phi is increasing and
A2: dom phi is limit_ordinal;
now
let A;
assume A in sup phi;
then consider B such that
A3: B in rng phi and
A4: A c= B by ORDINAL2:21;
consider x being object such that
A5: x in dom phi and
A6: B = phi.x by A3,FUNCT_1:def 3;
reconsider x as Ordinal by A5;
A7: succ x in dom phi by A2,A5,ORDINAL1:28;
reconsider C = phi.succ x as Ordinal;
x in succ x by ORDINAL1:6;
then B in C by A1,A6,A7;
then
A8: succ B c= C by ORDINAL1:21;
A9: succ A c= succ B by A4,ORDINAL2:1;
C in rng phi by A7,FUNCT_1:def 3;
then C in sup phi by ORDINAL2:19;
then succ B in sup phi by A8,ORDINAL1:12;
hence succ A in sup phi by A9,ORDINAL1:12;
end;
hence thesis by ORDINAL1:28;
end;
Lm5: rng f c= X implies (g|X)*f = g*f
proof
A1: f"rng f = dom f by RELAT_1:134;
assume rng f c= X;
then
A2: f"rng f c= f"X by RELAT_1:143;
f"X c= dom f by RELAT_1:132;
then
A3: f"X = dom f by A2,A1;
dom ((g|X)*f) = f"(dom (g|X)) by RELAT_1:147
.= f"(dom g /\ X) by RELAT_1:61
.= f"(dom g) /\ f"X by FUNCT_1:68
.= f"(dom g) by A3,RELAT_1:132,XBOOLE_1:28
.= dom (g*f) by RELAT_1:147;
hence thesis by GRFUNC_1:3,RELAT_1:64;
end;
theorem
fi is increasing & fi is continuous & psi is continuous & phi = psi*fi
implies phi is continuous
proof
assume that
A1: fi is increasing and
A2: for A,B st A in dom fi & A <> 0 & A is limit_ordinal & B = fi.A
holds B is_limes_of fi|A and
A3: for A,B st A in dom psi & A <> 0 & A is limit_ordinal & B = psi.A
holds B is_limes_of psi|A and
A4: phi = psi*fi;
let A,B such that
A5: A in dom phi and
A6: A <> 0 and
A7: A is limit_ordinal and
A8: B = phi.A;
reconsider A1 = fi.A as Ordinal;
A9: fi|A is increasing by A1,Th15;
A10: dom phi c= dom fi by A4,RELAT_1:25;
then A c= dom fi by A5,ORDINAL1:def 2;
then
A11: dom (fi|A) = A by RELAT_1:62;
A1 is_limes_of fi|A by A2,A5,A6,A7,A10;
then lim (fi|A) = A1 by ORDINAL2:def 10;
then
A12: sup (fi|A) = A1 by A6,A7,A11,A9,Th8;
A13: B = psi.A1 by A4,A5,A8,FUNCT_1:12;
A14: {} in A by A6,ORDINAL3:8;
A15: A1 in dom psi by A4,A5,FUNCT_1:11;
then A1 c= dom psi by ORDINAL1:def 2;
then
A16: dom (psi|A1) = A1 by RELAT_1:62;
A17: rng (fi|A) c= sup rng (fi|A)
proof
let x be object;
assume
A18: x in rng (fi|A);
then ex y being object st y in dom (fi|A) & x = (fi|A).y by FUNCT_1:def 3;
hence thesis by A18,ORDINAL2:19;
end;
phi|A = psi*(fi| A ) by A4,RELAT_1:83;
then
A19: phi|A = (psi|A1)*(fi|A) by A17,A12,Lm5;
A c= A1 by A1,A5,A10,Th10;
then B is_limes_of psi|A1 by A3,A7,A13,A15,A11,A14,A9,A12,Th16;
hence thesis by A9,A16,A12,A19,Th14;
end;
theorem
(for A st A in dom fi holds fi.A = C+^A) implies fi is increasing
proof
assume
A1: for A st A in dom fi holds fi.A = C+^A;
let A,B;
assume that
A2: A in B and
A3: B in dom fi;
A4: fi.B = C+^B by A1,A3;
fi.A = C+^A by A1,A2,A3,ORDINAL1:10;
hence thesis by A2,A4,ORDINAL2:32;
end;
theorem Th19:
C <> {} & (for A st A in dom fi holds fi.A = A*^C) implies fi is increasing
proof
assume that
A1: C <> {} and
A2: for A st A in dom fi holds fi.A = A*^C;
let A,B;
assume that
A3: A in B and
A4: B in dom fi;
A5: fi.B = B*^C by A2,A4;
fi.A = A*^C by A2,A3,A4,ORDINAL1:10;
hence thesis by A1,A3,A5,ORDINAL2:40;
end;
theorem Th20:
A <> {} implies exp({},A) = {}
proof
defpred FF[Ordinal] means $1 <> {} implies exp({},$1) = {};
A1: FF[B] implies FF[succ B]
proof
assume that
FF[B] and
succ B <> {};
thus exp({},succ B) = {}*^exp({},B) by ORDINAL2:44
.= {} by ORDINAL2:35;
end;
A2: for B st B <> 0 & B is limit_ordinal & for C st C in B holds FF[C]
holds FF[B]
proof
deffunc F(Ordinal) = exp({},$1);
let A such that
A3: A <> 0 and
A4: A is limit_ordinal and
A5: for C st C in A holds FF[C] and
A <> {};
consider fi such that
A6: dom fi = A & for B st B in A holds fi.B = F(B) from ORDINAL2:sch 3;
0 is_limes_of fi
proof
per cases;
case
0 = 0;
take B = 1;
{} in A by A3,ORDINAL3:8;
hence B in dom fi by A4,A6,Lm3,ORDINAL1:28;
let D;
assume
A7: B c= D;
assume
A8: D in dom fi;
then FF[D] by A5,A6;
hence thesis by A6,A7,A8,Lm3,ORDINAL1:21;
end;
case
0 <> 0;
thus thesis;
end;
end;
then lim fi = {} by ORDINAL2:def 10;
hence thesis by A3,A4,A6,ORDINAL2:45;
end;
A9: FF[0];
FF[B] from ORDINAL2:sch 1(A9,A1,A2);
hence thesis;
end;
Lm6: A <> {} & A is limit_ordinal implies for fi st dom fi = A & for B st B in
A holds fi.B = exp({},B) holds 0 is_limes_of fi
proof
assume that
A1: A <> {} and
A2: A is limit_ordinal;
let fi;
assume that
A3: dom fi = A and
A4: for B st B in A holds fi.B = exp({},B);
per cases;
case
0 = 0;
take B = 1;
{} in A by A1,ORDINAL3:8;
hence B in dom fi by A2,A3,Lm3,ORDINAL1:28;
let D;
assume that
A5: B c= D and
A6: D in dom fi;
A7: D <> {} by A5,Lm3,ORDINAL1:21;
exp({},D) = fi.D by A3,A4,A6;
hence thesis by A7,Th20;
end;
case
0 <> 0;
thus thesis;
end;
end;
Lm7: A <> {} implies for fi st dom fi = A & for B st B in A holds fi.B = exp(1
,B) holds 1 is_limes_of fi
proof
assume that
A1: A <> {};
let fi;
assume that
A2: dom fi = A and
A3: for B st B in A holds fi.B = exp(1,B);
per cases;
case
1 = 0;
hence thesis;
end;
case
1 <> 0;
let A1,A2 be Ordinal such that
A4: A1 in 1 and
A5: 1 in A2;
take B = {};
thus B in dom fi by A1,A2,ORDINAL3:8;
let D;
assume that
B c= D and
A6: D in dom fi;
exp(1,D) = fi.D by A2,A3,A6;
hence thesis by A4,A5,ORDINAL2:46;
end;
end;
Lm8: for A st A <> {} & A is limit_ordinal holds ex fi st dom fi = A & (for B
st B in A holds fi.B = exp(C,B)) & ex D st D is_limes_of fi
proof
defpred P[Ordinal] means $1 <> {} & $1 is limit_ordinal & for fi st dom fi =
$1 & for B st B in $1 holds fi.B = exp(C,B) for D holds not D is_limes_of fi;
let A such that
A1: A <> {} and
A2: A is limit_ordinal and
A3: for fi st dom fi = A & for B st B in A holds fi.B = exp(C,B) for D
holds not D is_limes_of fi;
deffunc F(Ordinal) = exp(C,$1);
A4: ex A st P[A] by A1,A2,A3;
consider A such that
A5: P[A] and
A6: for A1 st P[A1] holds A c= A1 from ORDINAL1:sch 1(A4);
consider fi such that
A7: dom fi = A & for B st B in A holds fi.B = F(B) from ORDINAL2:sch 3;
A8: C <> {} & C <> 1 by A5,A7,Lm6,Lm7;
then {} in C by ORDINAL3:8;
then 1 c= C by Lm3,ORDINAL1:21;
then
A9: 1 c< C by A8;
A10: for B2,B1 being Ordinal st B1 in B2 & B2 in A holds exp(C,B1) in exp(C,
B2)
proof
defpred V[Ordinal] means for B1 being Ordinal st B1 in $1 & $1 in A holds
exp(C,B1) in exp(C,$1);
A11: V[B] implies V[succ B]
proof
assume
A12: for B1 being Ordinal st B1 in B & B in A holds exp(C,B1) in exp (C,B);
let B1 be Ordinal such that
A13: B1 in succ B and
A14: succ B in A;
A15: B1 c= B by A13,ORDINAL1:22;
B in succ B by ORDINAL1:6;
then
A16: B in A by A14,ORDINAL1:10;
A17: 1*^exp(C,B) = exp(C,B) by ORDINAL2:39;
A18: exp(C,B) <> {}
proof
now
per cases;
suppose
B = {};
hence thesis by ORDINAL2:43;
end;
suppose
A19: B <> {};
B in succ B by ORDINAL1:6;
then B in A by A14,ORDINAL1:10;
hence thesis by A12,A19,ORDINAL3:8;
end;
end;
hence thesis;
end;
A20: exp(C,succ B) = C*^exp(C,B) by ORDINAL2:44;
then
A21: exp(C,B) in exp(C,succ B) by A9,A18,A17,ORDINAL1:11,ORDINAL2:40;
now
assume B1 <> B;
then B1 c< B by A15;
then B1 in B by ORDINAL1:11;
then exp(C,B1) in exp(C,B) by A12,A16;
hence thesis by A21,ORDINAL1:10;
end;
hence thesis by A9,A18,A20,A17,ORDINAL1:11,ORDINAL2:40;
end;
A22: for B st B <> 0 & B is limit_ordinal & for D st D in B holds V[D]
holds V[B]
proof
let B such that
A23: B <> 0 and
A24: B is limit_ordinal and
A25: for D st D in B holds V[D];
let B1 be Ordinal;
assume that
A26: B1 in B and
A27: B in A;
consider psi such that
A28: dom psi = B and
A29: for D st D in B holds psi.D = exp(C,D) and
ex D st D is_limes_of psi by A6,A24,A26,A27,ORDINAL1:5;
psi.B1 = exp(C,B1) by A26,A29;
then
A30: exp(C,B1) in rng psi by A26,A28,FUNCT_1:def 3;
psi is increasing
proof
let B1,B2 be Ordinal;
assume that
A31: B1 in B2 and
A32: B2 in dom psi;
B2 in A by A27,A28,A32,ORDINAL1:10;
then
A33: exp(C,B1) in exp(C,B2) by A25,A28,A31,A32;
psi.B1 = exp(C,B1) by A28,A29,A31,A32,ORDINAL1:10;
hence thesis by A28,A29,A32,A33;
end;
then
A34: lim psi = sup psi by A23,A24,A28,Th8;
exp(C,B) = lim psi by A23,A24,A28,A29,ORDINAL2:45;
hence thesis by A34,A30,ORDINAL2:19;
end;
A35: V[0];
thus for B holds V[B] from ORDINAL2:sch 1(A35,A11,A22);
end;
fi is increasing
proof
let B1,B2 be Ordinal;
assume that
A36: B1 in B2 and
A37: B2 in dom fi;
A38: fi.B1 = exp(C,B1) by A7,A36,A37,ORDINAL1:10;
exp(C,B1) in exp(C,B2) by A7,A10,A36,A37;
hence thesis by A7,A37,A38;
end;
then sup fi is_limes_of fi by A5,A7,Th8;
hence contradiction by A5,A7;
end;
theorem Th21:
A <> {} & A is limit_ordinal implies for fi st dom fi = A & for
B st B in A holds fi.B = exp(C,B) holds exp(C,A) is_limes_of fi
proof
assume that
A1: A <> {} and
A2: A is limit_ordinal;
consider psi such that
A3: dom psi = A and
A4: for B st B in A holds psi.B = exp(C,B) and
A5: ex D st D is_limes_of psi by A1,A2,Lm8;
let fi such that
A6: dom fi = A and
A7: for B st B in A holds fi.B = exp(C,B);
now
let x be object;
assume
A8: x in A;
then reconsider B = x as Ordinal;
thus fi.x = exp(C,B) by A7,A8
.= psi.x by A4,A8;
end;
then fi = psi by A6,A3,FUNCT_1:2;
then consider D such that
A9: D is_limes_of fi by A5;
D = lim fi by A9,ORDINAL2:def 10
.= exp(C,A) by A1,A2,A6,A7,ORDINAL2:45;
hence thesis by A9;
end;
theorem Th22:
C <> {} implies exp(C,A) <> {}
proof
defpred P[Ordinal] means exp(C,$1) <> {};
assume
A1: C <> {};
A2: for A st P[A] holds P[succ A]
proof
let A such that
A3: exp(C,A) <> {};
exp(C,succ A) = C*^exp(C,A) by ORDINAL2:44;
hence thesis by A1,A3,ORDINAL3:31;
end;
A4: for A st A <> 0 & A is limit_ordinal & for B st B in A holds P[B] holds
P[A]
proof
let A such that
A5: A <> 0 and
A6: A is limit_ordinal and
A7: for B st B in A holds exp(C,B) <> {};
consider fi such that
A8: dom fi = A and
A9: for B st B in A holds fi.B = exp(C,B) and
A10: ex D st D is_limes_of fi by A5,A6,Lm8;
A11: exp(C,A) = lim fi by A5,A6,A8,A9,ORDINAL2:45;
assume
A12: exp(C,A) = {};
consider D such that
A13: D is_limes_of fi by A10;
lim fi = D by A13,ORDINAL2:def 10;
then consider B such that
A14: B in dom fi and
A15: for D st B c= D & D in dom fi holds fi.D = {} by A11,A13,A12,
ORDINAL2:def 9;
fi.B = exp(C,B) by A8,A9,A14;
hence contradiction by A7,A8,A14,A15;
end;
A16: P[0] by ORDINAL2:43;
for A holds P[A] from ORDINAL2:sch 1(A16,A2,A4);
hence thesis;
end;
theorem Th23:
1 in C implies exp(C,A) in exp(C,succ A)
proof
A1: 1*^exp(C,A) = exp(C,A) by ORDINAL2:39;
assume 1 in C;
then exp(C,A) in C*^exp(C,A) by A1,Th22,ORDINAL2:40;
hence thesis by ORDINAL2:44;
end;
theorem Th24:
1 in C & A in B implies exp(C,A) in exp(C,B)
proof
defpred OO[Ordinal] means for A st A in $1 holds exp(C,A) in exp(C,$1);
A1: for B st B <> 0 & B is limit_ordinal & for D st D in B holds OO[D]
holds OO[B]
proof
deffunc F(Ordinal) = exp(C,$1);
let B such that
A2: B <> 0 and
A3: B is limit_ordinal and
A4: for D st D in B holds OO[D];
consider fi such that
A5: dom fi = B & for D st D in B holds fi.D = F(D) from ORDINAL2:sch
3;
fi is increasing
proof
let B1,B2 be Ordinal;
assume that
A6: B1 in B2 and
A7: B2 in dom fi;
A8: fi.B1 = exp(C,B1) by A5,A6,A7,ORDINAL1:10;
exp(C,B1) in exp(C,B2) by A4,A5,A6,A7;
hence thesis by A5,A7,A8;
end;
then
A9: sup fi = lim fi by A2,A3,A5,Th8;
let A such that
A10: A in B;
fi.A = exp(C,A) by A10,A5;
then
A11: exp(C,A) in rng fi by A10,A5,FUNCT_1:def 3;
exp(C,B) = lim fi by A2,A3,A5,ORDINAL2:45;
hence thesis by A9,A11,ORDINAL2:19;
end;
assume
A12: 1 in C;
A13: for B st OO[B] holds OO[succ B]
proof
let B such that
A14: for A st A in B holds exp(C,A) in exp(C,B);
let A;
assume A in succ B;
then
A15: A c= B by ORDINAL1:22;
A16: now
assume A <> B;
then A c< B by A15;
hence exp(C,A) in exp(C,B) by A14,ORDINAL1:11;
end;
exp(C,B) in exp(C,succ B) by A12,Th23;
hence thesis by A16,ORDINAL1:10;
end;
A17: OO[0];
for B holds OO[B] from ORDINAL2:sch 1(A17,A13,A1);
hence thesis;
end;
theorem Th25:
1 in C & (for A st A in dom fi holds fi.A = exp(C,A)) implies fi
is increasing
proof
assume that
A1: 1 in C and
A2: for A st A in dom fi holds fi.A = exp(C,A);
let A,B;
assume that
A3: A in B and
A4: B in dom fi;
A5: fi.B = exp(C,B) by A2,A4;
fi.A = exp(C,A) by A2,A3,A4,ORDINAL1:10;
hence thesis by A1,A3,A5,Th24;
end;
theorem
1 in C & A <> {} & A is limit_ordinal implies for fi st dom fi = A &
for B st B in A holds fi.B = exp(C,B) holds exp(C,A) = sup fi
proof
assume that
A1: 1 in C and
A2: A <> {} and
A3: A is limit_ordinal;
let fi;
assume that
A4: dom fi = A and
A5: for B st B in A holds fi.B = exp(C,B);
fi is increasing by A1,A4,A5,Th25;
then lim fi = sup fi by A2,A3,A4,Th8;
hence thesis by A2,A3,A4,A5,ORDINAL2:45;
end;
theorem
C <> {} & A c= B implies exp(C,A) c= exp(C,B)
proof
A1: A c< B iff A c= B & A <> B;
assume C <> {};
then {} in C by ORDINAL3:8;
then
A2: 1 c= C by Lm3,ORDINAL1:21;
assume A c= B;
then
A3: A in B or A = B by A1,ORDINAL1:11;
now
per cases;
suppose
A4: C = 1;
then exp(C,A) = 1 by ORDINAL2:46;
hence thesis by A4,ORDINAL2:46;
end;
suppose
C <> 1;
then 1 c< C by A2;
then 1 in C by ORDINAL1:11;
then exp(C,A) in exp(C,B) or exp(C,A) = exp(C,B) by A3,Th24;
hence thesis by ORDINAL1:def 2;
end;
end;
hence thesis;
end;
theorem
A c= B implies exp(A,C) c= exp(B,C)
proof
defpred P[Ordinal] means exp(A,$1) c= exp(B,$1);
assume
A1: A c= B;
A2: for C st P[C] holds P[succ C]
proof
let C;
A3: exp(B,succ C) = B*^exp(B,C) by ORDINAL2:44;
exp(A,succ C) = A*^exp(A,C) by ORDINAL2:44;
hence thesis by A1,A3,ORDINAL3:20;
end;
A4: for C st C <> 0 & C is limit_ordinal & for D st D in C holds P[D] holds
P[C]
proof
deffunc F(Ordinal) = exp(A,$1);
let C;
assume that
A5: C <> 0 and
A6: C is limit_ordinal and
A7: for D st D in C holds exp(A,D) c= exp(B,D);
consider f1 such that
A8: dom f1 = C & for D st D in C holds f1.D = F(D) from ORDINAL2:sch
3;
deffunc F(Ordinal) = exp(B,$1);
consider f2 such that
A9: dom f2 = C & for D st D in C holds f2.D = F(D) from ORDINAL2:sch
3;
A10: now
let D;
assume
A11: D in dom f1;
then
A12: f1.D = exp(A,D) by A8;
f2.D = exp(B,D) by A8,A9,A11;
hence f1.D c= f2.D by A7,A8,A11,A12;
end;
A13: exp(A,C) is_limes_of f1 by A5,A6,A8,Th21;
exp(B,C) is_limes_of f2 by A5,A6,A9,Th21;
hence thesis by A8,A9,A13,A10,Th6;
end;
exp(A,{}) = 1 by ORDINAL2:43;
then
A14: P[0] by ORDINAL2:43;
for C holds P[C] from ORDINAL2:sch 1(A14,A2,A4);
hence thesis;
end;
theorem
1 in C & A <> {} implies 1 in exp(C,A)
proof
assume that
A1: 1 in C and
A2: A <> {};
exp(C,{}) = 1 by ORDINAL2:43;
hence thesis by A1,A2,Th24,ORDINAL3:8;
end;
theorem Th30:
exp(C,A+^B) = exp(C,B)*^exp(C,A)
proof
defpred P[Ordinal] means exp(C,A+^$1) = exp(C,$1)*^exp(C,A);
A1: 1 = exp(C,{}) by ORDINAL2:43;
A2: for B st P[B] holds P[succ B]
proof
let B such that
A3: exp(C,A+^B) = exp(C,B)*^exp(C,A);
thus exp(C,A+^succ B) = exp(C,succ(A+^B)) by ORDINAL2:28
.= C*^exp(C,A+^B) by ORDINAL2:44
.= C*^exp(C,B)*^exp(C,A) by A3,ORDINAL3:50
.= exp(C,succ B)*^exp(C,A) by ORDINAL2:44;
end;
A4: for B st B <> 0 & B is limit_ordinal & for D st D in B holds P[D] holds
P[B]
proof
deffunc F(Ordinal) = exp(C,$1);
let B such that
A5: B <> 0 and
A6: B is limit_ordinal and
A7: for D st D in B holds exp(C,A+^D) = exp(C,D)*^exp(C,A);
consider fi such that
A8: dom fi = B & for D st D in B holds fi.D = F(D) from ORDINAL2:sch
3;
consider psi such that
A9: dom psi = A+^B & for D st D in A+^B holds psi.D = F(D) from
ORDINAL2:sch 3;
deffunc F(Ordinal) = exp(C,$1);
consider f1 such that
A10: dom f1 = A & for D st D in A holds f1.D = F(D) from ORDINAL2:sch
3;
A11: now
let D;
assume D in dom(fi*^exp(C,A));
then
A12: D in dom fi by ORDINAL3:def 4;
hence psi.((dom f1)+^D) = exp(C,A+^D) by A8,A9,A10,ORDINAL2:32
.= (exp(C,D))*^exp(C,A) by A7,A8,A12
.= (fi.D)*^exp(C,A) by A8,A12
.= (fi*^exp(C,A)).D by A12,ORDINAL3:def 4;
end;
A13: now
let D such that
A14: D in dom f1;
A c= A+^B by ORDINAL3:24;
hence psi.D = exp(C,D) by A9,A10,A14
.= f1.D by A10,A14;
end;
dom psi = (dom f1)+^(dom(fi*^exp(C,A))) by A8,A9,A10,ORDINAL3:def 4;
then
A15: psi = f1^(fi*^exp(C,A)) by A13,A11,Def1;
exp(C,B)*^exp(C,A) is_limes_of fi*^exp(C,A) by A5,A6,A8,Th5,Th21;
then
A16: exp(C,B)*^exp(C,A) is_limes_of psi by A15,Th3;
A17: A+^B <> {} by A5,ORDINAL3:26;
A+^B is limit_ordinal by A5,A6,ORDINAL3:29;
then lim psi = exp(C,A+^B) by A9,A17,ORDINAL2:45;
hence thesis by A16,ORDINAL2:def 10;
end;
exp(C,A) = 1*^exp(C,A) by ORDINAL2:39;
then
A18: P[0] by A1,ORDINAL2:27;
for B holds P[B] from ORDINAL2:sch 1(A18,A2,A4);
hence thesis;
end;
theorem
exp(exp(C,A),B) = exp(C,B*^A)
proof
defpred P[Ordinal] means exp(exp(C,A),$1) = exp(C,$1*^A);
A1: exp(C,{}) = 1 by ORDINAL2:43;
A2: for B st P[B] holds P[succ B]
proof
let B;
assume exp(exp(C,A),B) = exp(C,B*^A);
hence exp(exp(C,A),succ B) = exp(C,A)*^exp(C,B*^A) by ORDINAL2:44
.= exp(C,B*^A+^A) by Th30
.= exp(C,(succ B)*^A) by ORDINAL2:36;
end;
A3: for B st B <> 0 & B is limit_ordinal & for D st D in B holds P[D] holds
P[B]
proof
deffunc F(Ordinal) = exp(exp(C,A),$1);
let B;
assume that
A4: B <> 0 and
A5: B is limit_ordinal and
A6: for D st D in B holds exp(exp(C,A),D) = exp(C,D*^A);
consider fi such that
A7: dom fi = B & for D st D in B holds fi.D = F(D) from ORDINAL2:sch
3;
deffunc F(Ordinal) = $1*^A;
consider f1 such that
A8: dom f1 = B & for D st D in B holds f1.D = F(D) from ORDINAL2:sch
3;
deffunc F(Ordinal) = exp(C,$1);
consider f2 such that
A9: dom f2 = B*^A & for D st D in B*^A holds f2.D = F(D) from
ORDINAL2:sch 3;
A10: now
assume
A11: A <> {};
then B*^A <> {} by A4,ORDINAL3:31;
then
A12: exp(C,B*^A) is_limes_of f2 by A5,A9,Th21,ORDINAL3:40;
A13: rng f1 c= dom f2
proof
let x be object;
assume x in rng f1;
then consider y being object such that
A14: y in dom f1 and
A15: x = f1.y by FUNCT_1:def 3;
reconsider y as Ordinal by A14;
x = y*^A by A8,A14,A15;
hence thesis by A8,A9,A11,A14,ORDINAL2:40;
end;
A16: sup rng f1 = dom f2
proof
sup rng f1 c= sup dom f2 by A13,ORDINAL2:22;
hence sup rng f1 c= dom f2 by ORDINAL2:18;
let x be object;
assume
A17: x in dom f2;
then reconsider D = x as Ordinal;
consider A1 such that
A18: A1 in B and
A19: D in A1*^A by A5,A9,A17,ORDINAL3:41;
f1.A1 = A1*^A by A8,A18;
then A1*^A in rng f1 by A8,A18,FUNCT_1:def 3;
then A1*^A in sup rng f1 by ORDINAL2:19;
hence thesis by A19,ORDINAL1:10;
end;
A20: dom(f2*f1) = B
proof
thus dom(f2*f1) c= B by A8,RELAT_1:25;
let x be object;
assume
A21: x in B;
then reconsider E = x as Ordinal;
A22: f1.E = E*^A by A8,A21;
E*^A in B*^A by A11,A21,ORDINAL2:40;
hence thesis by A8,A9,A21,A22,FUNCT_1:11;
end;
now
let x be object;
assume
A23: x in B;
then reconsider D = x as Ordinal;
A24: f1.D = D*^A by A8,A23;
thus fi.x = exp(exp(C,A),D) by A7,A23
.= exp(C,D*^A) by A6,A23
.= f2.(f1.D) by A9,A11,A23,A24,ORDINAL2:40
.= (f2*f1).x by A8,A23,FUNCT_1:13;
end;
then fi = f2*f1 by A7,A20,FUNCT_1:2;
then exp(C,B*^A) is_limes_of fi by A8,A11,A12,A16,Th14,Th19;
then exp(C,B*^A) = lim fi by ORDINAL2:def 10;
hence thesis by A4,A5,A7,ORDINAL2:45;
end;
A25: B*^{} = {} by ORDINAL2:38;
exp(C,{}) = 1 by ORDINAL2:43;
hence thesis by A25,A10,ORDINAL2:46;
end;
exp(exp(C,A),{}) = 1 by ORDINAL2:43;
then
A26: P[0] by A1,ORDINAL2:35;
for B holds P[B] from ORDINAL2:sch 1(A26,A2,A3);
hence thesis;
end;
theorem
1 in C implies A c= exp(C,A)
proof
defpred P[Ordinal] means $1 c= exp(C,$1);
assume
A1: 1 in C;
A2: P[B] implies P[succ B]
proof
assume
A3: B c= exp(C,B);
A4: exp(C,B) = 1*^exp(C,B) by ORDINAL2:39;
exp(C,succ B) = C*^exp(C,B) by ORDINAL2:44;
then exp(C,B) in exp(C,succ B) by A1,A4,Th22,ORDINAL2:40;
then B in exp(C,succ B) by A3,ORDINAL1:12;
hence thesis by ORDINAL1:21;
end;
A5: 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(C,$1);
let A such that
A6: A <> 0 and
A7: A is limit_ordinal and
A8: for B st B in A holds B c= exp(C,B);
consider fi such that
A9: dom fi = A & for B st B in A holds fi.B = F(B) from ORDINAL2:sch
3;
let x be object;
assume
A10: x in A;
then reconsider B = x as Ordinal;
fi.B = exp(C,B) by A9,A10;
then exp(C,B) in rng fi by A9,A10,FUNCT_1:def 3;
then
A11: exp(C,B) in sup fi by ORDINAL2:19;
fi is increasing by A1,A9,Th25;
then
A12: sup fi = lim fi by A6,A7,A9,Th8
.= exp(C,A) by A6,A7,A9,ORDINAL2:45;
B c= exp(C,B) by A8,A10;
hence thesis by A12,A11,ORDINAL1:12;
end;
A13: P[0] by XBOOLE_1:2;
P[B] from ORDINAL2:sch 1(A13,A2,A5);
hence thesis;
end;
::$N Fixed-point lemma for normal functions
scheme
CriticalNumber { phi(Ordinal) -> Ordinal } : ex A st phi(A) = A
provided
A1: for A,B st A in B holds phi(A) in phi(B) and
A2: for A st A <> {} & A is limit_ordinal for phi st dom phi = A & for B
st B in A holds phi.B = phi(B) holds phi(A) is_limes_of phi
proof
A3: now
defpred P[Ordinal] means not $1 c= phi($1);
assume
A4: ex A st P[A];
consider A such that
A5: P[A] and
A6: for B st P[B] holds A c= B from ORDINAL1:sch 1(A4);
phi(phi(A)) in phi(A) by A1,A5,ORDINAL1:16;
then not phi(A) c= phi(phi(A)) by ORDINAL1:5;
hence contradiction by A5,A6;
end;
deffunc G(Ordinal,Sequence) = {};
deffunc F(Ordinal,Ordinal) = phi($2);
consider phi such that
A7: dom phi = omega and
A8: 0 in omega implies phi.0 = phi(0) and
A9: for A st succ A in omega holds phi.(succ A) = F(A,phi.A) and
for A st A in omega & A <> 0 & A is limit_ordinal holds phi.A = G(A,phi
|A) from ORDINAL2:sch 11;
assume
A10: not thesis;
A11: now
let A;
A12: A <> phi(A) by A10;
A c= phi(A) by A3;
then A c< phi(A) by A12;
hence A in phi(A) by ORDINAL1:11;
end;
A13: phi is increasing
proof
let A,B;
assume that
A14: A in B and
A15: B in dom phi;
defpred R[Ordinal] means A+^$1 in omega & $1 <> {} implies phi.A in phi.(A
+^$1);
A16: for B st B <> 0 & B is limit_ordinal & for C st C in B holds R[C]
holds R[B]
proof
let B such that
A17: B <> 0 and
A18: B is limit_ordinal and
for C st C in B holds A+^C in omega & C <> {} implies phi.A in phi.(
A+^C) and
A19: A+^B in omega and
A20: B <> {};
A+^B <> {} by A20,ORDINAL3:26;
then
A21: {} in A+^B by ORDINAL3:8;
A+^B is limit_ordinal by A17,A18,ORDINAL3:29;
then omega c= A+^B by A21,ORDINAL1:def 11;
hence thesis by A19,ORDINAL1:5;
end;
A22: for C st R[C] holds R[succ C]
proof
let C such that
A23: A+^C in omega & C <> {} implies phi.A in phi.(A+^C) and
A24: A+^succ C in omega and
succ C <> {};
reconsider D = phi.(A+^C) as Ordinal;
A25: A+^C in succ(A+^C) by ORDINAL1:6;
A26: D in phi(D) by A11;
A27: A+^succ C = succ(A+^C) by ORDINAL2:28;
then phi.(A+^succ C) = phi(D) by A9,A24;
hence thesis by A23,A24,A25,A27,A26,ORDINAL1:10,ORDINAL2:27;
end;
A28: R[0];
A29: for C holds R[C] from ORDINAL2:sch 1(A28,A22,A16);
ex C st B = A+^C & C <> {} by A14,ORDINAL3:28;
hence thesis by A7,A15,A29;
end;
deffunc phi(Ordinal) = phi ($1);
consider fi such that
A30: dom fi = sup phi & for A st A in sup phi holds fi.A = phi(A) from
ORDINAL2:sch 3;
phi({}) in rng phi by A7,A8,Lm1,FUNCT_1:def 3;
then
A31: sup phi <> {} by ORDINAL2:19;
then
A32: phi(sup phi) is_limes_of fi by A2,A7,A13,A30,Lm2,Th16;
A33: sup fi c= sup phi
proof
let x be object;
assume
A34: x in sup fi;
then reconsider A = x as Ordinal;
consider B such that
A35: B in rng fi and
A36: A c= B by A34,ORDINAL2:21;
consider y being object such that
A37: y in dom fi and
A38: B = fi.y by A35,FUNCT_1:def 3;
reconsider y as Ordinal by A37;
consider C such that
A39: C in rng phi and
A40: y c= C by A30,A37,ORDINAL2:21;
y c< C iff y <> C & y c= C;
then
A41: phi(y) in phi(C) or y = C by A1,A40,ORDINAL1:11;
B = phi(y) by A30,A37,A38;
then
A42: B c= phi(C) by A41,ORDINAL1:def 2;
consider z being object such that
A43: z in dom phi and
A44: C = phi.z by A39,FUNCT_1:def 3;
reconsider z as Ordinal by A43;
A45: succ z in omega by A7,A43,Lm2,ORDINAL1:28;
then
A46: phi.succ z in rng phi by A7,FUNCT_1:def 3;
phi.succ z = phi(C) by A9,A44,A45;
then phi(C) in sup phi by A46,ORDINAL2:19;
then B in sup phi by A42,ORDINAL1:12;
hence thesis by A36,ORDINAL1:12;
end;
A47: fi is increasing
proof
let A,B;
assume that
A48: A in B and
A49: B in dom fi;
A50: fi.B = phi(B) by A30,A49;
fi.A = phi(A) by A30,A48,A49,ORDINAL1:10;
hence thesis by A1,A48,A50;
end;
sup phi is limit_ordinal by A7,A13,Lm2,Th16;
then sup fi = lim fi by A30,A31,A47,Th8
.= phi(sup phi) by A32,ORDINAL2:def 10;
hence contradiction by A11,A33,ORDINAL1:5;
end;
reserve W for Universe;
registration
let W;
cluster ordinal for Element of W;
existence
proof
A1: On W c= W by ORDINAL2:7;
{} in On W by CLASSES2:51,ORDINAL3:8;
hence thesis by A1;
end;
end;
definition
let W;
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;
cluster non empty for Ordinal of W;
existence
proof
A1: On W c= W by ORDINAL2:7;
{} in On W by CLASSES2:51,ORDINAL3:8;
then 1 in W by A1,Lm3,CLASSES2:5;
hence thesis by Lm9;
end;
end;
registration
let W;
cluster On W -> non empty;
coherence by CLASSES2:51;
end;
registration
let W;
cluster -> Sequence-like Ordinal-yielding for Ordinal-Sequence of W;
coherence
proof
let s be Ordinal-Sequence of W;
thus dom s is epsilon-transitive epsilon-connected by FUNCT_2:def 1;
take On W;
thus rng s c= On W by RELAT_1:def 19;
end;
end;
reserve A1,B1 for Ordinal of W,
phi for Ordinal-Sequence of W;
scheme
UOSLambda { W() -> Universe, F(set) -> Ordinal of W() } : ex phi being
Ordinal-Sequence of W() st for a being Ordinal of W() holds phi.a = F(a) proof
consider psi such that
A1: dom psi = On W() & for A st A in On W() holds psi.A = F(A) from
ORDINAL2:sch 3;
rng psi c= On W()
proof
let x be object;
assume x in rng psi;
then consider y being object such that
A2: y in dom psi and
A3: x = psi.y by FUNCT_1:def 3;
reconsider y as Ordinal by A2;
x = F(y) by A1,A2,A3;
hence thesis by ORDINAL1:def 9;
end;
then reconsider psi as Ordinal-Sequence of W()
by A1,FUNCT_2:def 1,RELSET_1:4;
take psi;
let a be Ordinal of W();
a in On W() by ORDINAL1:def 9;
hence thesis by A1;
end;
definition
let W;
func 0-element_of W -> Ordinal of W equals
{};
correctness
proof
A1: On W c= W by ORDINAL2:7;
{} in On W by ORDINAL3:8;
then reconsider A = {} as Ordinal of W by A1;
A = {};
hence thesis;
end;
func 1-element_of W -> non empty Ordinal of W equals
1;
correctness
proof
A2: On W c= W by ORDINAL2:7;
{} in On W by ORDINAL3:8;
then reconsider A = 1 as Ordinal of W by A2,Lm3,CLASSES2:5;
A = 1;
hence thesis by Lm9;
end;
let phi,A1;
redefine func phi.A1 -> Ordinal of W; :: redefines . (FUNCT_1, definition)
coherence
proof
reconsider B = phi.A1 as Ordinal;
A3: dom phi = On W by FUNCT_2:def 1;
A4: rng phi c= On W by RELAT_1:def 19;
A1 in On W by ORDINAL1:def 9;
then B in rng phi by A3,FUNCT_1:def 3;
then
A5: B in On W by A4;
On W c= W by ORDINAL2:7;
hence thesis by A5;
end;
end;
definition
let W;
let p2,p1 be Ordinal-Sequence of W;
redefine func p1*p2 -> Ordinal-Sequence of W; :: redefines * (FUNCT_1, synonym) → * (RELAT_1, synonym) → (#) (RELAT_1, definition)
coherence
proof
A1: rng p2 c= On W by RELAT_1:def 19;
A2: dom p2 = On W by FUNCT_2:def 1;
dom p1 = On W by FUNCT_2:def 1;
then
A3: dom(p1*p2) = On W by A2,A1,RELAT_1:27;
then reconsider f = p1*p2 as Sequence by ORDINAL1:def 7;
A4: rng p1 c= On W by RELAT_1:def 19;
rng(p1*p2) c= rng p1 by RELAT_1:26;
then rng f c= On W by A4;
hence thesis by A3,FUNCT_2:def 1,RELSET_1:4;
end;
end;
theorem
0-element_of W = {} & 1-element_of W = 1;
definition
let W,A1;
redefine func succ A1 -> non empty Ordinal of W; :: redefines succ (ORDINAL1, definition)
coherence by CLASSES2:5;
let B1;
redefine func A1 +^ B1 -> Ordinal of W; :: redefines +^ (ORDINAL2, definition)
coherence
proof
defpred P[Ordinal] means $1 in W implies A1+^$1 in W;
A1: for B st for C st C in B holds P[C] holds P[B]
proof
let B such that
A2: for C st C in B holds C in W implies A1+^C in W and
A3: B in W;
[:B,{1-element_of W}:] in W by A3,CLASSES2:61;
then [:A1,{0-element_of W}:] \/ [:B,{1-element_of W}:] in W
by CLASSES2:60;
then
A4: card([:A1,{0-element_of W}:] \/ [:B,{1-element_of W}:]) in card W
by CLASSES2:1;
A5: A1+^B c= W
proof
let x be object;
assume
A6: x in A1+^B;
then reconsider A = x as Ordinal;
A7: now
A8: B c= W by A3,ORDINAL1:def 2;
assume A1 c= A;
then consider C such that
A9: A = A1+^C by ORDINAL3:27;
C in B by A6,A9,ORDINAL3:22;
hence thesis by A2,A9,A8;
end;
A10: A in A1 or A1 c= A by ORDINAL1:16;
A1 c= W by ORDINAL1:def 2;
hence thesis by A10,A7;
end;
card(A1+^B) = card([:A1,{0-element_of W}:] \/ [:B,{ 1-element_of W}
:] ) by CARD_2:9;
hence thesis by A4,A5,CLASSES1:1;
end;
for B holds P[B] from ORDINAL1:sch 2(A1);
hence thesis;
end;
end;
definition
let W,A1,B1;
redefine func A1 *^ B1 -> Ordinal of W; :: redefines *^ (ORDINAL2, definition)
coherence
proof
defpred P[Ordinal] means $1 in W implies $1*^B1 in W;
A1: for A st for C st C in A holds P[C] holds P[A]
proof
let A such that
A2: for C st C in A holds C in W implies C*^B1 in W and
A3: A in W;
[:A,B1:] in W by A3,CLASSES2:61;
then
A4: card [:A,B1:] in card W by CLASSES2:1;
A5: A*^B1 c= W
proof
let x be object;
A6: B1 c= W by ORDINAL1:def 2;
assume
A7: x in A*^B1;
then reconsider B = x as Ordinal;
B1 <> {} by A7,ORDINAL2:38;
then consider C,D such that
A8: B = C*^B1+^D and
A9: D in B1 by ORDINAL3:47;
C*^B1 c= B by A8,ORDINAL3:24;
then C*^B1 in A*^B1 by A7,ORDINAL1:12;
then
A10: C in A by ORDINAL3:34;
A c= W by A3,ORDINAL1:def 2;
then reconsider CB = C*^B1, D as Ordinal of W by A2,A9,A6,A10;
x = CB+^D by A8;
hence thesis;
end;
card(A*^B1) = card [:A,B1:] by CARD_2:11;
hence thesis by A4,A5,CLASSES1:1;
end;
for A holds P[A] from ORDINAL1:sch 2(A1);
hence thesis;
end;
end;
theorem Th34:
A1 in dom phi
proof
dom phi = On W by FUNCT_2:def 1;
hence thesis by ORDINAL1:def 9;
end;
theorem Th35:
dom fi in W & rng fi c= W implies sup fi in W
proof
assume that
A1: dom fi in W and
A2: rng fi c= W;
ex A st rng fi c= A by ORDINAL2:def 4;
then for x st x in rng fi holds x is Ordinal;
then reconsider B = union rng fi as epsilon-transitive epsilon-connected set
by ORDINAL1:23;
A3: rng fi = fi.:(dom fi) by RELAT_1:113;
A4: sup fi c= succ B
proof
let x be object;
assume
A5: x in sup fi;
then reconsider A = x as Ordinal;
consider C such that
A6: C in rng fi and
A7: A c= C by A5,ORDINAL2:21;
C c= union rng fi by A6,ZFMISC_1:74;
then A c= B by A7;
hence thesis by ORDINAL1:22;
end;
card dom fi in card W by A1,CLASSES2:1;
then card rng fi in card W by A3,CARD_1:67,ORDINAL1:12;
then rng fi in W by A2,CLASSES1:1;
then union rng fi in W by CLASSES2:59;
then succ B in W by CLASSES2:5;
hence thesis by A4,CLASSES1:def 1;
end;
reserve L for Sequence;
theorem
phi is increasing & phi is continuous & omega in W implies ex A st A
in dom phi & phi.A = A
proof
deffunc D(set,set) = {};
assume that
A1: phi is increasing and
A2: phi is continuous and
A3: omega in W;
deffunc C(set,set) = phi.$2;
reconsider N = phi.(0-element_of W) as Ordinal;
consider L such that
A4: dom L = omega and
A5: 0 in omega implies L.0 = N and
A6: for A st succ A in omega holds L.(succ A) = C(A,L.A) and
for A st A in omega & A <> 0 & A is limit_ordinal holds L.A = D(A,L|A)
from ORDINAL2:sch 5;
defpred P[Ordinal] means $1 in dom L implies L.$1 is Ordinal of W;
A7: for A st P[A] holds P[succ A]
proof
let A such that
A8: A in dom L implies L.A is Ordinal of W and
A9: succ A in dom L;
A in succ A by ORDINAL1:6;
then reconsider x = L.A as Ordinal of W by A8,A9,ORDINAL1:10;
L.succ A = phi.x by A4,A6,A9;
hence thesis;
end;
A10: for A st A <> 0 & A is limit_ordinal & for B st B in A holds P[B]
holds P[A]
proof
let A such that
A11: A <> 0 and
A12: A is limit_ordinal and
for B st B in A holds B in dom L implies L.B is Ordinal of W and
A13: A in dom L;
{} in A by A11,ORDINAL3:8;
then omega c= A by A12,ORDINAL1:def 11;
hence thesis by A4,A13,ORDINAL1:5;
end;
A14: P[0] by A4,A5;
A15: for A holds P[A] from ORDINAL2:sch 1(A14,A7,A10);
rng L c= sup rng L
proof
let x be object;
assume
A16: x in rng L;
then consider y being object such that
A17: y in dom L and
A18: x = L.y by FUNCT_1:def 3;
reconsider y as Ordinal by A17;
reconsider A = L.y as Ordinal of W by A15,A17;
A in sup rng L by A16,A18,ORDINAL2:19;
hence thesis by A18;
end;
then reconsider L as Ordinal-Sequence by ORDINAL2:def 4;
A19: dom phi = On W by FUNCT_2:def 1;
assume
A20: not thesis;
A21: now
let A1;
A1 in dom phi by Th34;
then
A22: A1 c= phi.A1 by A1,Th10;
A1 <> phi.A1 by A20,Th34;
then A1 c< phi.A1 by A22;
hence A1 in phi.A1 by ORDINAL1:11;
end;
L is increasing
proof
let A,B;
assume that
A23: A in B and
A24: B in dom L;
defpred P[Ordinal] means A+^$1 in omega & $1 <> {} implies L.A in L.(A+^$1
);
A25: for B st B <> 0 & B is limit_ordinal & for C st C in B holds P[C]
holds P[B]
proof
let B such that
A26: B <> 0 and
A27: B is limit_ordinal and
for C st C in B holds A+^C in omega & C <> {} implies L.A in L.(A+^C
) and
A28: A+^B in omega and
A29: B <> {};
A+^B <> {} by A29,ORDINAL3:26;
then
A30: {} in A+^B by ORDINAL3:8;
A+^B is limit_ordinal by A26,A27,ORDINAL3:29;
then omega c= A+^B by A30,ORDINAL1:def 11;
hence thesis by A28,ORDINAL1:5;
end;
A31: for C st P[C] holds P[succ C]
proof
let C such that
A32: A+^C in omega & C <> {} implies L.A in L.(A+^C) and
A33: A+^succ C in omega and
succ C <> {};
A34: A+^succ C = succ(A+^C) by ORDINAL2:28;
A35: A+^C in succ(A+^C) by ORDINAL1:6;
then reconsider D = L.(A+^C) as Ordinal of W by A4,A15,A33,A34,
ORDINAL1:10;
A36: D in phi.D by A21;
L.(A+^succ C) = phi.D by A6,A33,A34;
hence thesis by A32,A33,A35,A34,A36,ORDINAL1:10,ORDINAL2:27;
end;
A37: P[0];
A38: for C holds P[C] from ORDINAL2:sch 1(A37,A31,A25);
ex C st B = A+^C & C <> {} by A23,ORDINAL3:28;
hence thesis by A4,A24,A38;
end;
then
A39: sup L is limit_ordinal by A4,Lm2,Th16;
A40: rng L c= W
proof
let x be object;
assume x in rng L;
then consider y being object such that
A41: y in dom L and
A42: x = L.y by FUNCT_1:def 3;
reconsider y as Ordinal by A41;
L.y is Ordinal of W by A15,A41;
hence thesis by A42;
end;
then reconsider S = sup L as Ordinal of W by A3,A4,Th35;
set fi = phi|sup L;
N in rng L by A4,A5,Lm1,FUNCT_1:def 3;
then
A43: sup L <> {} by ORDINAL2:19;
A44: S in On W by ORDINAL1:def 9;
then
A45: phi.S is_limes_of fi by A2,A43,A39,A19;
S c= dom phi by A44,A19,ORDINAL1:def 2;
then
A46: dom fi = S by RELAT_1:62;
A47: sup fi c= sup L
proof
let x be object;
assume
A48: x in sup fi;
then reconsider A = x as Ordinal;
consider B such that
A49: B in rng fi and
A50: A c= B by A48,ORDINAL2:21;
consider y being object such that
A51: y in dom fi and
A52: B = fi.y by A49,FUNCT_1:def 3;
reconsider y as Ordinal by A51;
consider C such that
A53: C in rng L and
A54: y c= C by A46,A51,ORDINAL2:21;
reconsider C1 = C as Ordinal of W by A40,A53;
y c< C1 iff y c= C1 & y <> C1;
then y in C1 & C1 in dom phi or y = C by A19,A54,ORDINAL1:11,def 9;
then
A55: phi.y in phi.C1 or y = C1 by A1;
B = phi.y by A51,A52,FUNCT_1:47;
then
A56: B c= phi.C1 by A55,ORDINAL1:def 2;
consider z being object such that
A57: z in dom L and
A58: C = L.z by A53,FUNCT_1:def 3;
reconsider z as Ordinal by A57;
A59: succ z in omega by A4,A57,Lm2,ORDINAL1:28;
then
A60: L.succ z in rng L by A4,FUNCT_1:def 3;
L.succ z = phi.C by A6,A58,A59;
then phi.C1 in sup L by A60,ORDINAL2:19;
then B in sup L by A56,ORDINAL1:12;
hence thesis by A50,ORDINAL1:12;
end;
fi is increasing
proof
A61: dom fi c= dom phi by RELAT_1:60;
let A,B;
assume that
A62: A in B and
A63: B in dom fi;
A64: fi.B = phi.B by A63,FUNCT_1:47;
fi.A = phi.A by A62,A63,FUNCT_1:47,ORDINAL1:10;
hence thesis by A1,A62,A63,A61,A64;
end;
then sup fi = lim fi by A43,A39,A46,Th8
.= phi.(sup L) by A45,ORDINAL2:def 10;
then not S in phi.S by A47,ORDINAL1:5;
hence contradiction by A21;
end;
begin :: Addenda
:: from ZFREFLE1, 2007.03.14, A.T.
reserve e,u for set;
theorem
A is_cofinal_with B & B is_cofinal_with C implies A is_cofinal_with C
proof
given xi1 being Ordinal-Sequence such that
A1: dom xi1 = B and
A2: rng xi1 c= A and
A3: xi1 is increasing and
A4: A = sup xi1;
given xi2 being Ordinal-Sequence such that
A5: dom xi2 = C and
A6: rng xi2 c= B and
A7: xi2 is increasing and
A8: B = sup xi2;
consider xi being Ordinal-Sequence such that
A9: xi = xi1*xi2 and
A10: xi is increasing by A3,A7,Th13;
take xi;
thus
A11: dom xi = C by A1,A5,A6,A9,RELAT_1:27;
rng xi c= rng xi1 by A9,RELAT_1:26;
hence
A12: rng xi c= A & xi is increasing by A2,A10;
thus A c= sup xi
proof
let a be object;
assume
A13: a in A;
then reconsider a as Ordinal;
consider b being Ordinal such that
A14: b in rng xi1 and
A15: a c= b by A4,A13,ORDINAL2:21;
consider e being object such that
A16: e in B and
A17: b = xi1.e by A1,A14,FUNCT_1:def 3;
reconsider e as Ordinal by A16;
consider c being Ordinal such that
A18: c in rng xi2 and
A19: e c= c by A8,A16,ORDINAL2:21;
consider u being object such that
A20: u in C and
A21: c = xi2.u by A5,A18,FUNCT_1:def 3;
reconsider u as Ordinal by A20;
A22: xi1.c = xi.u by A9,A11,A20,A21,FUNCT_1:12;
xi.u in rng xi by A11,A20,FUNCT_1:def 3;
then
A23: xi.u in sup xi by ORDINAL2:19;
xi1.e c= xi1.c by A1,A3,A6,A18,A19,Th9;
hence thesis by A15,A17,A22,A23,ORDINAL1:12,XBOOLE_1:1;
end;
sup rng xi c= sup A by A12,ORDINAL2:22;
hence thesis by ORDINAL2:18;
end;
theorem
A is_cofinal_with B implies (A is limit_ordinal iff B is limit_ordinal )
proof
given psi such that
A1: dom psi = B and
A2: rng psi c= A and
A3: psi is increasing and
A4: A = sup psi;
thus A is limit_ordinal implies B is limit_ordinal
proof
assume
A5: A is limit_ordinal;
now
let C;
reconsider c = psi.C as Ordinal;
assume
A6: C in B;
then psi.C in rng psi by A1,FUNCT_1:def 3;
then succ c in A by A2,A5,ORDINAL1:28;
then consider b being Ordinal such that
A7: b in rng psi and
A8: succ c c= b by A4,ORDINAL2:21;
consider e being object such that
A9: e in B and
A10: b = psi.e by A1,A7,FUNCT_1:def 3;
reconsider e as Ordinal by A9;
c in succ c by ORDINAL1:6;
then not e c= C by A1,A3,A6,A8,A10,Th9,ORDINAL1:5;
then C in e by ORDINAL1:16;
then succ C c= e by ORDINAL1:21;
hence succ C in B by A9,ORDINAL1:12;
end;
hence thesis by ORDINAL1:28;
end;
thus thesis by A1,A3,A4,Th16;
end;
:: from 2009.09.28, A.T.
registration let D;
let f,g be Sequence of D;
cluster f^g -> D-valued;
coherence
proof
rng f c= D & rng g c= D by RELAT_1:def 19;
then
A1: rng f \/ rng g c= D by XBOOLE_1:8;
rng(f^g) c= rng f \/ rng g by Th2;
hence rng(f^g) c= D by A1;
end;
end;
theorem
for A, B being Sequence holds rng A c= rng(A^B) by Th7A;
theorem
for A, B being Sequence holds rng B c= rng(A^B) by Th8A;