:: On Powers of Cardinals
:: by Grzegorz Bancerek
::
:: Received August 24, 1992
:: Copyright (c) 1992-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 NUMBERS, SUBSET_1, ORDINAL1, CARD_1, FUNCT_1, ORDINAL2, TARSKI,
CARD_3, RELAT_1, FINSET_1, XBOOLE_0, ARYTM_3, WELLORD1, WELLORD2,
ORDINAL4, CARD_2, ORDINAL3, ZFMISC_1, FUNCT_2, FUNCOP_1, MCART_1, CARD_5,
MEMBERED, NAT_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, CARD_1, ORDINAL1, NUMBERS,
XCMPLX_0, NAT_1, MEMBERED, RELAT_1, FUNCT_1, FINSET_1, FUNCT_2, WELLORD1,
WELLORD2, XTUPLE_0, MCART_1, FUNCOP_1, ORDINAL2, ORDINAL3, CARD_2,
CARD_3, ORDINAL4;
constructors WELLORD1, WELLORD2, FUNCOP_1, ORDINAL3, XXREAL_0, NAT_1,
FINSEQ_1, CARD_2, CARD_3, ORDINAL4, RELSET_1, MEMBERED, ORDERS_1,
XREAL_0, XTUPLE_0, NUMBERS;
registrations XBOOLE_0, FUNCT_1, ORDINAL1, FUNCOP_1, ORDINAL2, ORDINAL3,
NAT_1, CARD_1, CARD_3, ORDINAL4, MEMBERED, FINSET_1, CARD_2, XTUPLE_0;
requirements NUMERALS, BOOLE, SUBSET;
definitions TARSKI, FUNCT_1, ORDINAL2, CARD_1, CARD_3, XBOOLE_0, ORDINAL1;
equalities ORDINAL2, CARD_3, ORDINAL1;
expansions TARSKI, FUNCT_1, ORDINAL2, CARD_1, XBOOLE_0;
theorems TARSKI, FUNCT_1, FUNCT_2, FUNCOP_1, NAT_1, FINSET_1, ORDINAL1,
ORDINAL2, ORDINAL3, ORDINAL4, WELLORD1, WELLORD2, CARD_1, CARD_2, CARD_3,
CARD_4, ZFMISC_1, FUNCT_4, FUNCT_5, RELAT_1, XBOOLE_0, XBOOLE_1,
XTUPLE_0;
schemes FUNCT_1, ORDINAL1, PARTFUN1, CARD_1, CARD_3, ORDINAL2, CLASSES1,
XBOOLE_0, CARD_2, XFAMILY;
begin :: Results of [(30),AXIOMS].
reserve k,n,m for Nat,
A,B,C for Ordinal,
X for set,
x,y,z for object;
Lm1: 1 = card 1;
Lm2: 2 = card 2;
begin :: Infinity, alephs and cofinality
reserve f,g,h,fx for Function,
K,M,N for Cardinal,
phi,psi for
Ordinal-Sequence;
theorem Th1:
nextcard card X = nextcard X
proof
card card X in nextcard X & for M st card card X in M holds nextcard X
c= M by CARD_1:def 3;
hence thesis by CARD_1:def 3;
end;
theorem Th2:
y in Union f iff ex x st x in dom f & y in f.x
proof
thus y in Union f implies ex x st x in dom f & y in f.x
proof
assume y in Union f;
then consider X such that
A1: y in X and
A2: X in rng f by TARSKI:def 4;
consider x being object such that
A3: x in dom f & X = f.x by A2,FUNCT_1:def 3;
take x;
thus thesis by A1,A3;
end;
given x such that
A4: x in dom f and
A5: y in f.x;
f.x in rng f by A4,FUNCT_1:def 3;
hence thesis by A5,TARSKI:def 4;
end;
theorem Th3:
aleph A is infinite
proof
{} c= A;
then omega c= aleph A by CARD_1:23,46;
hence thesis;
end;
theorem
M is infinite implies ex A st M = aleph A
proof
defpred P[set] means $1 is infinite implies ex A st $1 = aleph A;
A1: P[K] implies P[nextcard K]
proof
assume that
A2: P[K] and
A3: not nextcard K is finite;
now
assume K is finite;
then reconsider K9 = K as finite set;
nextcard Segm card K9 = card Segm(card K9 + 1) by NAT_1:42;
hence contradiction by A3;
end;
then consider A such that
A4: K = aleph A by A2;
take succ A;
thus thesis by A4,CARD_1:19;
end;
A5: K <> {} & K is limit_cardinal & (for N st N in K holds P[N]) implies P[
K]
proof
deffunc a(Ordinal) = aleph $1;
defpred R[object,object] means ex A st $1 = aleph A & $2 = A;
assume that
K <> {} and
A6: K is limit_cardinal and
A7: for N st N in K holds P[N] and
A8: not K is finite;
defpred P[object] means ex N st N = $1 & not N is finite;
consider X such that
A9: for x being object holds x in X iff x in K & P[x] from XBOOLE_0:sch 1;
A10: for x being object st x in X ex y being object st R[x,y]
proof
let x be object;
assume
A11: x in X;
then consider N such that
A12: N = x and
A13: not N is finite by A9;
N in K by A9,A11,A12;
then ex A st x = aleph A by A7,A12,A13;
hence thesis;
end;
consider f such that
A14: dom f = X &
for x being object st x in X holds R[x,f.x] from CLASSES1:sch 1(
A10);
now
let x be set;
assume x in rng f;
then consider y being object such that
A15: y in X and
A16: x = f.y by A14,FUNCT_1:def 3;
consider A such that
A17: y = aleph A and
A18: x = A by A14,A15,A16;
thus x is Ordinal by A18;
thus x c= rng f
proof
let z be object;
assume
A19: z in x;
then reconsider z9 = z as Ordinal by A18;
A20: aleph z9 in aleph A by A18,A19,CARD_1:21;
aleph A in K by A9,A15,A17;
then
A21: aleph z9 in K by A20,ORDINAL1:10;
not aleph z9 is finite by Th3;
then
A22: aleph z9 in X by A9,A21;
then ex A st aleph z9 = aleph A & f.(aleph z9) = A by A14;
then z9 = f.(aleph z9) by CARD_1:22;
hence thesis by A14,A22,FUNCT_1:def 3;
end;
end;
then reconsider A = rng f as epsilon-transitive epsilon-connected set
by ORDINAL1:19;
consider L being Sequence such that
A23: dom L = A & for B st B in A holds L.B = a(B) from ORDINAL2:sch 2;
now
let B;
assume B in A;
then consider x being object such that
A24: x in X and
A25: B = f.x by A14,FUNCT_1:def 3;
consider C such that
A26: x = aleph C and
A27: B = C by A14,A24,A25;
A28: aleph succ C = nextcard aleph C by CARD_1:19;
aleph C in K by A9,A24,A26;
then
A29: aleph succ C c= K by A28,CARD_3:90;
aleph succ C <> K by A6,A28;
then
A30: aleph succ C in K by A29,CARD_1:3;
not aleph succ C is finite by Th3;
then
A31: aleph succ C in X by A9,A30;
then consider D being Ordinal such that
A32: aleph succ C = aleph D and
A33: f.(aleph succ C) = D by A14;
succ C = D by A32,CARD_1:22;
hence succ B in A by A14,A27,A31,A33,FUNCT_1:def 3;
end;
then A is limit_ordinal by ORDINAL1:28;
then
A34: A = {} or aleph A = card sup L by A23,CARD_1:20;
take A;
sup L c= K
proof
let x be Ordinal;
assume
A35: x in sup L;
reconsider x9 = x as Ordinal;
consider C such that
A36: C in rng L and
A37: x9 c= C by A35,ORDINAL2:21;
consider y being object such that
A38: y in dom L and
A39: C = L.y by A36,FUNCT_1:def 3;
reconsider y as Ordinal by A38;
A40: C = aleph y by A23,A38,A39;
consider z being object such that
A41: z in dom f and
A42: y = f.z by A23,A38,FUNCT_1:def 3;
ex D being Ordinal st z = aleph D & y = D by A14,A41,A42;
then C in K by A9,A14,A40,A41;
hence thesis by A37,ORDINAL1:12;
end;
then card sup L c= card K by CARD_1:11;
then
A43: card sup L c= K;
now
per cases;
case
A = {};
then not omega in X by A14,RELAT_1:42;
then not omega in K by A9;
then
A44: K c= omega by CARD_1:4;
omega c= K by A8,CARD_3:85;
hence K = omega by A44;
end;
case
A45: A <> {};
assume K <> aleph A;
then
A46: card sup L in K by A34,A43,A45,CARD_1:3;
not aleph A is finite by Th3;
then
A47: card sup L in X by A9,A34,A45,A46;
then consider B such that
A48: card sup L = aleph B and
A49: f.(card sup L) = B by A14;
A = B by A34,A45,A48,CARD_1:22;
then A in A by A14,A47,A49,FUNCT_1:def 3;
hence contradiction;
end;
end;
hence thesis by CARD_1:46;
end;
A50: P[{}];
for M holds P[M] from CARD_1:sch 1(A50,A1,A5);
hence thesis;
end;
registration
let phi;
cluster Union phi -> ordinal;
coherence
proof
ex A st rng phi c= A by ORDINAL2:def 4;
then On rng phi = rng phi by ORDINAL3:6;
hence thesis by ORDINAL3:5;
end;
end;
theorem Th5:
X c= A implies ex phi st phi = canonical_isomorphism_of(RelIncl
order_type_of RelIncl X, RelIncl X) & phi is increasing & dom phi =
order_type_of RelIncl X & rng phi = X
proof
set R = RelIncl X;
set B = order_type_of R;
set phi = canonical_isomorphism_of (RelIncl B,R);
assume
A1: X c= A;
then R is well-ordering by WELLORD2:8;
then R, RelIncl B are_isomorphic by WELLORD2:def 2;
then RelIncl B is well-ordering & RelIncl B, R are_isomorphic by WELLORD1:40
,WELLORD2:8;
then
A2: phi is_isomorphism_of RelIncl B,R by WELLORD1:def 9;
then
A3: phi is one-to-one by WELLORD1:def 7;
A4: field RelIncl B = B by WELLORD2:def 1;
then
A5: dom phi = B by A2,WELLORD1:def 7;
A6: field R = X by WELLORD2:def 1;
then
A7: rng phi = X by A2,WELLORD1:def 7;
reconsider phi as Sequence by A5,ORDINAL1:def 7;
reconsider phi as Ordinal-Sequence by A1,A7,ORDINAL2:def 4;
take phi;
thus phi = canonical_isomorphism_of (RelIncl order_type_of RelIncl X,
RelIncl X);
thus phi is increasing
proof
let a,b be Ordinal;
assume that
A8: a in b and
A9: b in dom phi;
A10: a in dom phi by A8,A9,ORDINAL1:10;
reconsider a9 = phi.a, b9 = phi.b as Ordinal;
A11: b9 in X by A7,A9,FUNCT_1:def 3;
a c= b by A8,ORDINAL1:def 2;
then [a,b] in RelIncl B by A5,A9,A10,WELLORD2:def 1;
then
A12: [a9,b9] in R by A2,WELLORD1:def 7;
a9 in X by A7,A10,FUNCT_1:def 3;
then
A13: a9 c= b9 by A12,A11,WELLORD2:def 1;
a <> b by A8;
then a9 <> b9 by A3,A9,A10;
then a9 c< b9 by A13;
hence thesis by ORDINAL1:11;
end;
thus thesis by A2,A4,A6,WELLORD1:def 7;
end;
theorem Th6:
X c= A implies sup X is_cofinal_with order_type_of RelIncl X
proof
assume
A1: X c= A;
then consider phi such that
phi = canonical_isomorphism_of (RelIncl order_type_of RelIncl X, RelIncl
X) and
A2: phi is increasing & dom phi = order_type_of RelIncl X & rng phi = X
by Th5;
take phi;
On X = X by A1,ORDINAL3:6;
hence thesis by A2,ORDINAL2:def 3;
end;
theorem Th7:
X c= A implies card X = card order_type_of RelIncl X
proof
set R = RelIncl X;
set B = order_type_of R;
set phi = canonical_isomorphism_of (RelIncl B,R);
assume X c= A;
then R is well-ordering by WELLORD2:8;
then R, RelIncl B are_isomorphic by WELLORD2:def 2;
then RelIncl B is well-ordering & RelIncl B, R are_isomorphic by WELLORD1:40
,WELLORD2:8;
then
A1: phi is_isomorphism_of RelIncl B,R by WELLORD1:def 9;
field R = X by WELLORD2:def 1;
then
A2: rng phi = X by A1,WELLORD1:def 7;
field RelIncl B = B by WELLORD2:def 1;
then
A3: dom phi = B by A1,WELLORD1:def 7;
phi is one-to-one by A1,WELLORD1:def 7;
then B,X are_equipotent by A3,A2,WELLORD2:def 4;
hence thesis by CARD_1:5;
end;
theorem Th8:
ex B st B c= card A & A is_cofinal_with B
proof
set M = card A;
M,A are_equipotent by CARD_1:def 2;
then consider f such that
A1: f is one-to-one and
A2: dom f = M and
A3: rng f = A by WELLORD2:def 4;
defpred P[set] means not f.$1 in Union (f|$1);
reconsider f as Sequence by A2,ORDINAL1:def 7;
reconsider f as Ordinal-Sequence by A3,ORDINAL2:def 4;
consider X such that
A4: for x being set holds x in X iff x in M & P[x] from XFAMILY:sch 1;
set R = RelIncl X;
set B = order_type_of R;
take B;
A5: X c= M
by A4;
hence B c= card A by WELLORD2:14;
set phi = canonical_isomorphism_of (RelIncl B,R);
R is well-ordering by A5,WELLORD2:8;
then R, RelIncl B are_isomorphic by WELLORD2:def 2;
then RelIncl B is well-ordering & RelIncl B, R are_isomorphic by WELLORD1:40
,WELLORD2:8;
then
A6: phi is_isomorphism_of RelIncl B,R by WELLORD1:def 9;
then
A7: phi is one-to-one by WELLORD1:def 7;
field RelIncl B = B by WELLORD2:def 1;
then
A8: dom phi = B by A6,WELLORD1:def 7;
field R = X by WELLORD2:def 1;
then
A9: rng phi = X by A6,WELLORD1:def 7;
reconsider phi as Sequence by A8,ORDINAL1:def 7;
reconsider phi as Ordinal-Sequence by A5,A9,ORDINAL2:def 4;
A10: dom (f*phi) = B by A2,A5,A8,A9,RELAT_1:27;
then reconsider xi = f*phi as Sequence by ORDINAL1:def 7;
rng (f*phi) c= A by A3,RELAT_1:26;
then reconsider xi as Ordinal-Sequence by ORDINAL2:def 4;
take xi;
thus dom xi = B & rng xi c= A by A2,A3,A5,A8,A9,RELAT_1:26,27;
thus xi is increasing
proof
let a,b be Ordinal;
assume that
A11: a in b and
A12: b in dom xi;
A13: a in dom xi by A11,A12,ORDINAL1:10;
then
A14: phi.a in X by A8,A9,A10,FUNCT_1:def 3;
a <> b by A11;
then
A15: phi.a <> phi.b by A8,A7,A10,A12,A13;
reconsider a9 = phi.a, b9 = phi.b as Ordinal;
reconsider a99 = f.a9, b99 = f.b9 as Ordinal;
A16: phi.b in X by A8,A9,A10,A12,FUNCT_1:def 3;
then not b99 in Union (f|b9) by A4;
then
A17: Union (f|b9) c= b99 by ORDINAL1:16;
a c= b by A11,ORDINAL1:def 2;
then [a,b] in RelIncl B by A10,A12,A13,WELLORD2:def 1;
then [phi.a,phi.b] in R by A6,WELLORD1:def 7;
then a9 c= b9 by A14,A16,WELLORD2:def 1;
then a9 c< b9 by A15;
then a9 in b9 by ORDINAL1:11;
then a99 c= Union (f|b9) by A2,A5,A14,FUNCT_1:50,ZFMISC_1:74;
then
A18: a99 c= b99 by A17;
a99 <> b99 by A1,A2,A5,A15,A14,A16;
then
A19: a99 c< b99 by A18;
a99 = xi.a & b99 = xi.b by A11,A12,FUNCT_1:12,ORDINAL1:10;
hence thesis by A19,ORDINAL1:11;
end;
thus A c= sup xi
proof
let x be Ordinal;
assume x in A;
then consider y being object such that
A20: y in dom f and
A21: x = f.y by A3,FUNCT_1:def 3;
reconsider x9 = x, y as Ordinal by A20;
now
per cases;
suppose
not f.y in Union (f|y);
then y in X by A2,A4,A20;
then consider z being object such that
A22: z in B & y = phi.z by A8,A9,FUNCT_1:def 3;
x9 = xi.z & xi.z in rng xi by A10,A21,A22,FUNCT_1:12,def 3;
hence thesis by ORDINAL2:19;
end;
suppose
A23: f.y in Union (f|y);
defpred P[Ordinal] means $1 in y & f.y in f.$1;
consider z such that
A24: z in dom (f|y) and
A25: f.y in (f|y).z by A23,Th2;
reconsider z as Ordinal by A24;
A26: (f|y).z = f.z by A24,FUNCT_1:47;
dom (f|y) = dom f /\ y by RELAT_1:61;
then z in y by A24,XBOOLE_0:def 4;
then
A27: ex C st P[C] by A25,A26;
consider C such that
A28: P[C] & for B st P[B] holds C c= B from ORDINAL1:sch 1(A27);
now
thus C in M by A2,A20,A28,ORDINAL1:10;
assume f.C in Union (f|C);
then consider a be object such that
A29: a in dom (f|C) and
A30: f.C in (f|C).a by Th2;
reconsider a as Ordinal by A29;
reconsider fa = (f|C).a, fy = f.y as Ordinal;
f.a = fa by A29,FUNCT_1:47;
then
A31: fy in f.a by A28,A30,ORDINAL1:10;
dom (f|C) = dom f /\ C by RELAT_1:61;
then
A32: a in C by A29,XBOOLE_0:def 4;
then a in y by A28,ORDINAL1:10;
hence contradiction by A28,A32,A31,ORDINAL1:5;
end;
then C in X by A4;
then consider z being object such that
A33: z in B and
A34: C = phi.z by A8,A9,FUNCT_1:def 3;
reconsider z as Ordinal by A33;
reconsider xz = xi.z as Ordinal;
xz in rng xi by A10,A33,FUNCT_1:def 3;
then
A35: xz in sup xi by ORDINAL2:19;
x9 in xz by A10,A21,A28,A33,A34,FUNCT_1:12;
hence thesis by A35,ORDINAL1:10;
end;
end;
hence thesis;
end;
sup A = A by ORDINAL2:18;
hence thesis by A3,ORDINAL2:22,RELAT_1:26;
end;
theorem Th9:
ex M st M c= card A & A is_cofinal_with M & for B st A
is_cofinal_with B holds M c= B
proof
defpred P[Ordinal] means $1 c= card A & A is_cofinal_with $1;
A1: ex B st P[B] by Th8;
consider C such that
A2: P[C] and
A3: for B st P[B] holds C c= B from ORDINAL1:sch 1(A1);
take M = card C;
consider B such that
A4: B c= M and
A5: C is_cofinal_with B by Th8;
A6: M c= C by CARD_1:8;
then
A7: B c= C by A4;
then B c= card A by A2,XBOOLE_1:1;
then C c= B by A2,A3,A5,ORDINAL4:37;
then
A8: C = B by A7;
hence M c= card A & A is_cofinal_with M by A2,A4,A6,XBOOLE_0:def 10;
let B;
assume that
A9: A is_cofinal_with B and
A10: not M c= B;
A11: C = M by A4,A6,A8;
then not B c= card A by A3,A9,A10;
hence contradiction by A2,A11,A10,XBOOLE_1:1;
end;
Lm3: rng phi = rng psi & phi is increasing & psi is increasing implies for A
st A in dom phi holds A in dom psi & phi.A = psi.A
proof
assume that
A1: rng phi = rng psi and
A2: phi is increasing;
defpred P[Ordinal] means $1 in dom phi implies $1 in dom psi & phi.$1 = psi.
$1;
assume
A3: for A,B st A in B & B in dom psi holds psi.A in psi.B;
A4: for A st for B st B in A holds P[B] holds P[A]
proof
let A;
assume that
A5: for B st B in A & B in dom phi holds B in dom psi & phi.B = psi.B and
A6: A in dom phi;
phi.A in rng phi by A6,FUNCT_1:def 3;
then consider x being object such that
A7: x in dom psi and
A8: phi.A = psi.x by A1,FUNCT_1:def 3;
reconsider x as Ordinal by A7;
A9: now
assume
A10: A in x;
then
A11: A in dom psi by A7,ORDINAL1:10;
then psi.A in rng psi by FUNCT_1:def 3;
then consider y being object such that
A12: y in dom phi and
A13: psi.A = phi.y by A1,FUNCT_1:def 3;
reconsider y as Ordinal by A12;
psi.A in psi.x by A3,A7,A10;
then not A c= y by A2,A8,A12,A13,ORDINAL1:5,ORDINAL4:9;
then
A14: y in A by ORDINAL1:16;
then
A15: psi.y = phi.y by A5,A12;
psi.y in psi.A by A3,A11,A14;
hence contradiction by A13,A15;
end;
now
assume
A16: x in A;
then phi.x in phi.A & x in dom phi by A2,A6,ORDINAL1:10;
then phi.A in phi.A by A5,A8,A16;
hence contradiction;
end;
hence thesis by A7,A8,A9,ORDINAL1:14;
end;
thus P[A] from ORDINAL1:sch 2(A4);
end;
theorem
rng phi = rng psi & phi is increasing & psi is increasing implies phi
= psi
proof
assume
A1: rng phi = rng psi & phi is increasing & psi is increasing;
A2: dom phi = dom psi
proof
thus dom phi c= dom psi
by A1,Lm3;
let x be Ordinal;
assume x in dom psi;
hence thesis by A1,Lm3;
end;
for x being object st x in dom phi holds phi.x = psi.x by A1,Lm3;
hence thesis by A2;
end;
theorem Th11:
phi is increasing implies phi is one-to-one
proof
assume
A1: for A,B st A in B & B in dom phi holds phi.A in phi.B;
let x,y be object;
assume that
A2: x in dom phi & y in dom phi and
A3: phi.x = phi.y;
reconsider A = x, B = y as Ordinal by A2;
A4: A in B or A = B or B in A by ORDINAL1:14;
not phi.A in phi.B by A3;
hence thesis by A1,A2,A3,A4;
end;
theorem Th12:
(phi^psi)|(dom phi) = phi
proof
dom (phi^psi) = (dom phi)+^(dom psi) by ORDINAL4:def 1;
then dom phi c= dom (phi^psi) by ORDINAL3:24;
then
A1: dom phi = (dom (phi^psi))/\(dom phi) by XBOOLE_1:28;
for x being object st x in dom phi holds phi.x = (phi^psi).x
by ORDINAL4:def 1;
hence thesis by A1,FUNCT_1:46;
end;
theorem
X <> {} implies card { Y where Y is Subset of X: card Y in M } c= M*`
exp(card X,M)
proof
set Z = { Y where Y is Subset of X: card Y in M };
X,card X are_equipotent by CARD_1:def 2;
then consider f such that
A1: f is one-to-one and
A2: dom f = X and
A3: rng f = card X by WELLORD2:def 4;
defpred P[object,object] means
ex X be set, A be Ordinal, phi be Ordinal-Sequence st
X = $1 & $2 = [A,phi] &
dom phi = M & phi|A is increasing & rng (phi|A) = f.:X &
for B st A c= B & B in M holds phi.B = {};
A4: for x being object st x in Z ex y being object st P[x,y]
proof
deffunc f(set) = {};
let x be object;
reconsider xx = x as set by TARSKI:1;
set A = order_type_of RelIncl (f.:xx);
consider xi2 being Ordinal-Sequence such that
A5: dom xi2 = M -^ A & for B st B in M -^ A holds xi2.B = f(B) from
ORDINAL2:sch 3;
assume x in Z;
then
A6: ex Y being Subset of X st x = Y & card Y in M;
consider xi1 being Ordinal-Sequence such that
xi1 = canonical_isomorphism_of (RelIncl A, RelIncl (f.:xx)) and
A7: xi1 is increasing and
A8: dom xi1 = A and
A9: rng xi1 = f.:xx by A3,Th5,RELAT_1:111;
set phi = xi1^xi2;
take y = [A,phi];
take xx, A, phi;
thus xx = x;
card (f.:xx) = card A by A3,Th7,RELAT_1:111;
then card A in M by A6,CARD_1:67,ORDINAL1:12;
then A in M by CARD_3:44;
then A c= M by ORDINAL1:def 2;
then A+^( M -^ A) = M by ORDINAL3:def 5;
hence y = [A,phi] & dom phi = M & phi|A is increasing &
rng (phi|A) = f.:xx
by A7,A8,A9,A5,Th12,ORDINAL4:def 1;
let B;
assume that
A10: A c= B and
A11: B in M;
A12: B-^A in M-^A by A10,A11,ORDINAL3:53;
B = A+^(B-^A) by A10,ORDINAL3:def 5;
then phi.B = xi2.(B-^A) by A8,A5,A12,ORDINAL4:def 1;
hence thesis by A5,A12;
end;
consider g such that
A13: dom g = Z &
for x being object st x in Z holds P[x,g.x] from CLASSES1:sch 1(A4);
assume
A14: X <> {};
rng g c= [:M,Funcs(M,card X):]
proof
let x be object;
assume x in rng g;
then consider y being object such that
A15: y in dom g and
A16: x = g.y by FUNCT_1:def 3;
consider yy being set, A being Ordinal, phi being Ordinal-Sequence
such that
A17: yy = y and
A18: x = [A,phi] and
A19: dom phi = M and
A20: phi|A is increasing and
A21: rng (phi|A) = f.:yy and
A22: for B st A c= B & B in M holds phi.B = {} by A13,A15,A16;
A23: ex Y being Subset of X st y = Y & card Y in M by A13,A15;
rng phi c= card X
proof
let x be object;
assume x in rng phi;
then consider z being object such that
A24: z in dom phi and
A25: x = phi.z by FUNCT_1:def 3;
reconsider z as Ordinal by A24;
z in A or A c= z by ORDINAL1:16;
then x in f.:yy & f.:yy c= card X or x = {} by A3,A19,A21,A22,A24,A25,
FUNCT_1:50,RELAT_1:111;
hence thesis by A14,ORDINAL3:8;
end;
then
A26: phi in Funcs(M,card X) by A19,FUNCT_2:def 2;
A27: A c= M or M c= A;
phi|A is one-to-one by A20,Th11;
then dom (phi|A),f.:yy are_equipotent by A21,WELLORD2:def 4;
then card dom (phi|A) = card (f.:yy) by CARD_1:5;
then card dom (phi|A) in M by A23,CARD_1:67,ORDINAL1:12,A17;
then
A28: dom (phi|A) in M by CARD_3:44;
then dom (phi|A) <> M;
then A in M by A19,A28,A27,RELAT_1:62,68;
hence thesis by A18,A26,ZFMISC_1:87;
end;
then
A29: card rng g c= card [:M,Funcs(M,card X):] by CARD_1:11;
g is one-to-one
proof
let x,y be object;
assume that
A30: x in dom g and
A31: y in dom g and
A32: g.x = g.y;
consider yy being set, A2 be Ordinal, phi2 be Ordinal-Sequence such that
A33: yy = y and
A34: g.y = [A2,phi2] and
dom phi2 = M and
phi2|A2 is increasing and
A35: rng (phi2|A2) = f.:yy and
for B st A2 c= B & B in M holds phi2.B = {} by A13,A31;
consider xx being set, A1 be Ordinal, phi1 be Ordinal-Sequence such that
A36: xx = x and
A37: g.x = [A1,phi1] and
dom phi1 = M and
phi1|A1 is increasing and
A38: rng (phi1|A1) = f.:xx and
for B st A1 c= B & B in M holds phi1.B = {} by A13,A30;
A39: A1 = A2 & phi1 = phi2 by A32,A37,A34,XTUPLE_0:1;
A40: ex Y being Subset of X st x = Y & card Y in M by A13,A30;
xx = yy
proof
thus xx c= yy
proof
let z be object;
assume
A41: z in xx;
then f.z in f.:xx by A2,A40,FUNCT_1:def 6,A36;
then ex x1 being object st x1 in dom f & x1 in yy & f.z = f.x1
by A38,A35,A39
,FUNCT_1:def 6;
hence thesis by A1,A2,A40,A41,A36;
end;
let z be object;
A42: ex Y being Subset of X st y = Y & card Y in M by A13,A31;
assume
A43: z in yy;
then f.z in f.:yy by A2,A42,FUNCT_1:def 6,A33;
then
ex x1 being object st x1 in dom f & x1 in xx & f.z = f.x1 by A38,A35,A39,
FUNCT_1:def 6;
hence thesis by A1,A2,A42,A43,A33;
end;
hence thesis by A33,A36;
end;
then
A44: Z,rng g are_equipotent by A13,WELLORD2:def 4;
card [:M,Funcs(M,card X):] = card [:M,card Funcs(M,card X):] by CARD_2:7
.= M*`card Funcs(M,card X) by CARD_2:def 2
.= M*`exp(card X,M) by CARD_2:def 3;
hence thesis by A44,A29,CARD_1:5;
end;
theorem Th14:
M in exp(2,M)
proof
card bool M = exp(2,card M) & card M = M by CARD_2:31;
hence thesis by CARD_1:14;
end;
registration
cluster infinite for Cardinal;
existence
proof
take omega;
thus thesis;
end;
end;
registration
cluster infinite -> non empty for set;
coherence;
end;
definition
mode Aleph is infinite Cardinal;
let M;
func cf M -> Cardinal means
:Def1:
M is_cofinal_with it & for N st M
is_cofinal_with N holds it c= N;
existence
proof
defpred P[Ordinal] means M is_cofinal_with $1 & $1 is Cardinal;
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);
reconsider K = A as Cardinal by A2;
take K;
thus M is_cofinal_with K by A2;
let N;
assume M is_cofinal_with N;
hence thesis by A2;
end;
uniqueness;
let N;
func N-powerfunc_of M -> Cardinal-Function means
: Def2:
(for x holds x in
dom it iff x in M & x is Cardinal) & for K st K in M holds it.K = exp(K,N);
existence
proof
deffunc f(set) = exp(card $1,N);
defpred P[object] means $1 is Cardinal;
consider X such that
A3: for x being object holds x in X iff x in M & P[x] from XBOOLE_0:sch 1;
consider f being Cardinal-Function such that
A4: dom f = X & for x being set st x in X holds f.x = f(x) from CARD_3:sch 1;
take f;
thus x in dom f iff x in M & x is Cardinal by A3,A4;
let K;
assume K in M;
then K = card K & K in X by A3;
hence thesis by A4;
end;
uniqueness
proof
defpred P[object] means $1 in M & $1 is Cardinal;
let f1,f2 be Cardinal-Function;
assume that
A5: for x holds x in dom f1 iff P[x] and
A6: for K st K in M holds f1.K = exp(K,N) and
A7: for x holds x in dom f2 iff P[x] and
A8: for K st K in M holds f2.K = exp(K,N);
A9: now
let x be object;
assume
A10: x in dom f1;
then reconsider K = x as Cardinal by A5;
A11: K in M by A5,A10;
hence f1.x = exp(K,N) by A6
.= f2.x by A8,A11;
end;
dom f1 = dom f2 from XBOOLE_0:sch 2(A5,A7);
hence thesis by A9;
end;
end;
registration
let A;
cluster aleph A -> infinite;
coherence by Th3;
end;
begin :: Arithmetics of alephs
reserve a,b for Aleph;
::$CT
theorem Th15:
a <> 0 & a <> 1 & a <> 2 & a <> card n & card n in a & omega c= a
proof
omega c= a & card n in omega by CARD_3:85;
hence thesis;
end;
theorem Th16:
a c= M or a in M implies M is Aleph
proof
assume a c= M or a in M;
then
A1: a c= M by ORDINAL1:16;
omega c= a by Th15;
then omega c= M by A1;
hence thesis;
end;
theorem Th17:
a c= M or a in M implies a +` M = M & M +` a = M & a *` M = M &
M *` a = M
proof
card 0 in a by Th15;
then
A1: 0 in a;
assume
A2: a c= M or a in M;
then
A3: M is infinite by Th16;
A4: a c= M by A2,ORDINAL1:16;
thus a +` M = M by CARD_2:76,A3,A4;
thus M +` a = M by CARD_2:76,A3,A4;
thus a *` M = M by A1,CARD_4:16,A3,A4;
thus M *` a = M by A1,CARD_4:16,A3,A4;
end;
theorem
a +` a = a & a *` a = a by CARD_2:75,CARD_4:15;
theorem Th19:
M c= exp(M,a)
proof
1 in a by Lm1,Th15;
then M = 0 & {} c= exp(M,a) or exp(M,1) c= exp(M,a) & exp(M,1) = M by
CARD_2:27,93;
hence thesis;
end;
theorem
union a = a by ORDINAL1:def 6;
registration
let a,M;
cluster a +` M -> infinite;
coherence
proof
a c= M or M c= a;
then a +` M = M & M is Aleph or a +` M = a by Th17,CARD_2:76;
hence thesis;
end;
end;
registration
let M,a;
cluster M +` a -> infinite;
coherence;
end;
registration
let a,b;
cluster a *` b -> infinite;
coherence
proof
a c= b or b c= a;
hence thesis by Th17;
end;
cluster exp(a,b) -> infinite;
coherence
proof
1 in b by Lm1,Th15;
then
A1: exp(a,1) c= exp(a,b) by CARD_2:92;
exp(a,1) = a & omega c= a by Th15,CARD_2:27;
then omega c= exp(a,b) by A1;
hence thesis;
end;
end;
begin :: Regular alephs
definition
let IT be Aleph;
attr IT is regular means
cf IT = IT;
end;
notation
let IT be Aleph;
antonym IT is irregular for IT is regular;
end;
registration
let a;
cluster nextcard a -> infinite;
coherence
proof
A1: omega c= a by Th15;
a in nextcard a by CARD_1:18;
then a c= nextcard a by ORDINAL1:16;
then omega c= nextcard a by A1;
hence thesis;
end;
end;
theorem Th21:
cf omega = omega
proof
defpred P[set,set] means $2 c= $1;
assume
A1: cf omega <> omega;
cf omega c= omega by Def1;
then cf omega in omega by A1,CARD_1:3;
then reconsider B = cf omega as finite set;
set n = card B;
A2: for x,y being set st P[x,y] & P[y,x] holds x = y;
A3: for x,y,z being set st P[x,y] & P[y,z] holds P[x,z] by XBOOLE_1:1;
omega is_cofinal_with n by Def1;
then consider xi being Ordinal-Sequence such that
A4: dom xi = n and
A5: rng xi c= omega and
xi is increasing and
A6: omega = sup xi;
reconsider rxi = rng xi as finite set by A4,FINSET_1:8;
A7: rxi <> {} by A6,ORDINAL2:18;
consider x being set such that
A8: x in rxi & for y being set st y in rxi & y <> x holds not P[y,x]
from CARD_2:sch 3(A7,A2,A3);
reconsider x as Ordinal by A5,A8;
now
let A;
assume A in rng xi;
then A c= x or not x c= A by A8;
hence A in succ x by ORDINAL1:22;
end;
then
A9: omega c= succ x by A6,ORDINAL2:20;
succ x in omega by A5,A8,ORDINAL1:28;
hence contradiction by A9;
end;
theorem Th22:
cf nextcard a = nextcard a
proof
nextcard a is_cofinal_with cf nextcard a by Def1;
then consider xi being Ordinal-Sequence such that
A1: dom xi = cf nextcard a and
A2: rng xi c= nextcard a and
xi is increasing and
A3: nextcard a = sup xi;
A4: card Union xi c= Sum Card xi & Sum (cf nextcard a --> a) = (cf nextcard
a)*` a by CARD_2:65,CARD_3:39;
A5: card nextcard a = nextcard a & succ Union xi = (Union xi) +^ 1 by
ORDINAL2:31;
A6: now
let x be object;
assume
A7: x in cf nextcard a;
xi.x in rng xi by A1,A7,FUNCT_1:def 3;
then
A8: card (xi.x) in nextcard a by A2,CARD_1:8,ORDINAL1:12;
(Card xi).x = card (xi.x) & (cf nextcard a --> a).x = a by A1,A7,
CARD_3:def 2,FUNCOP_1:7;
hence (Card xi).x c= (cf nextcard a --> a).x by A8,CARD_3:91;
end;
dom Card xi = dom xi & dom (cf nextcard a --> a) = cf nextcard a by
CARD_3:def 2;
then Sum Card xi c= Sum (cf nextcard a --> a) by A1,A6,CARD_3:30;
then card Union xi c= (cf nextcard a)*`a by A4;
then
A9: (card Union xi) +` 1 c= (cf nextcard a)*`a +` 1 by CARD_2:84;
A10: card ((Union xi) +^ 1) = (card Union xi) +` card 1 by CARD_2:13;
ex A st rng xi c= A by ORDINAL2:def 4;
then On rng xi = rng xi by ORDINAL3:6;
then
A11: card nextcard a c= card succ Union xi by A3,CARD_1:11,ORDINAL3:72;
A12: cf nextcard a c= nextcard a by Def1;
now
per cases;
suppose
cf nextcard a = 0;
then
A13: (cf nextcard a)*`a = 0 by CARD_2:20;
thus thesis by A11,A5,A9,A10,A13;
end;
suppose
A14: cf nextcard a <> 0;
0 c= cf nextcard a;
then
A15: 0 in cf nextcard a by A14,CARD_1:3;
A16: cf nextcard a c= a or a c= cf nextcard a;
1 in a by Lm1,Th15;
then
A17: (cf nextcard a)*`a = a & a+`1 = a & a in nextcard a or (cf nextcard
a)*`a = cf nextcard a & cf nextcard a is Aleph by A15,A16,Th17,CARD_1:18
,CARD_2:76,CARD_4:16;
then
nextcard a c= (cf nextcard a) +` 1 & 1 in cf nextcard a by A11,A5,A9,A10
,Th15,CARD_1:4;
then nextcard a c= cf nextcard a by A11,A5,A9,A10,A17,CARD_1:4
,CARD_2:76;
hence thesis by A12;
end;
end;
hence thesis;
end;
theorem Th23:
omega c= cf a
proof
A1: a is_cofinal_with cf a by Def1;
then cf a <> {} by ORDINAL2:50;
then
A2: {} in cf a by ORDINAL3:8;
cf a is limit_ordinal by A1,ORDINAL4:38;
hence thesis by A2,ORDINAL1:def 11;
end;
theorem
cf 0 = 0 & cf card (n+1) = 1
proof
A1: succ n is_cofinal_with 1 by ORDINAL3:73;
card (n+1) = n+1 & Segm(n+1) = succ Segm n by NAT_1:38;
then cf card (n+1) c= 1 by A1,Def1;
then
A2: cf card (n+1) = 1 or cf card (n+1) = 0 & {} c= n & n in succ n by
ORDINAL1:6,ORDINAL3:16;
cf 0 c= 0 & 0 c= cf 0 by Def1;
hence cf 0 = 0;
card (n+1) is_cofinal_with cf card (n+1) by Def1;
hence thesis by A2,ORDINAL2:50;
end;
theorem Th25:
X c= M & card X in cf M implies sup X in M & union X in M
proof
assume that
A1: X c= M and
A2: card X in cf M;
set A = order_type_of (RelIncl X);
A3: card A = card X by A1,Th7;
consider N such that
A4: N c= card A and
A5: A is_cofinal_with N and
for C st A is_cofinal_with C holds N c= C by Th9;
sup X is_cofinal_with A by A1,Th6;
then
A6: sup X is_cofinal_with N by A5,ORDINAL4:37;
A7: now
assume sup X = M;
then cf M c= N by A6,Def1;
hence contradiction by A2,A3,A4,CARD_1:4;
end;
for x st x in X holds x is Ordinal by A1;
then reconsider A = union X as epsilon-transitive epsilon-connected set
by ORDINAL1:23;
A8: sup M = M by ORDINAL2:18;
sup X c= sup M by A1,ORDINAL2:22;
then
A9: sup X c< M by A8,A7;
hence sup X in M by ORDINAL1:11;
A c= sup X
proof
let x be Ordinal;
assume x in A;
then consider Y being set such that
A10: x in Y and
A11: Y in X by TARSKI:def 4;
reconsider Y as Ordinal by A1,A11;
Y in sup X by A11,ORDINAL2:19;
then Y c= sup X by ORDINAL1:def 2;
hence thesis by A10;
end;
hence thesis by A9,ORDINAL1:11,12;
end;
theorem Th26:
dom phi = M & rng phi c= N & M in cf N implies sup phi in N &
Union phi in N
proof
assume that
A1: dom phi = M and
A2: rng phi c= N and
A3: M in cf N;
card rng phi c= card M by A1,CARD_1:12;
then card rng phi in cf N by A3,ORDINAL1:12;
hence thesis by A2,Th25;
end;
registration
let a;
cluster cf a -> infinite;
coherence by Th16,Th23;
end;
theorem Th27:
cf a in a implies a is limit_cardinal
proof
assume
A1: cf a in a;
given M such that
A2: a = nextcard M;
cf a c= M by A1,A2,CARD_3:91;
then reconsider M as Aleph;
nextcard M in nextcard M by A1,A2,Th22;
hence contradiction;
end;
theorem Th28:
cf a in a implies ex xi being Ordinal-Sequence st dom xi = cf a
& rng xi c= a & xi is increasing & a = sup xi & xi is Cardinal-Function & not 0
in rng xi
proof
a is_cofinal_with cf a by Def1;
then consider xi being Ordinal-Sequence such that
A1: dom xi = cf a and
A2: rng xi c= a and
xi is increasing and
A3: a = sup xi;
deffunc f(Sequence) = (nextcard (xi.dom $1)) \/ nextcard sup $1;
consider phi being Sequence such that
A4: dom phi = cf a & for A for psi being Sequence st A in cf a & psi =
phi|A holds phi.A = f(psi) from ORDINAL1:sch 4;
phi is Ordinal-yielding
proof
take sup rng phi;
let x be object;
assume
A5: x in rng phi;
then consider y being object such that
A6: y in dom phi and
A7: x = phi.y by FUNCT_1:def 3;
reconsider y as Ordinal by A6;
y c= dom phi by A6,ORDINAL1:def 2;
then dom (phi|y) = y by RELAT_1:62;
then x = ( nextcard (xi.y)) \/ nextcard sup (phi|y) by A4,A6,A7;
hence thesis by A5,ORDINAL2:19;
end;
then reconsider phi as Ordinal-Sequence;
defpred P[Ordinal] means $1 in cf a implies phi.$1 in a;
assume cf a in a;
then
A8: a is limit_cardinal by Th27;
A9: now
let A such that
A10: for B st B in A holds P[B];
thus P[A]
proof
assume
A11: A in cf a;
then
A12: card A in cf a by CARD_1:9;
A c= dom phi by A4,A11,ORDINAL1:def 2;
then
A13: dom (phi|A) = A by RELAT_1:62;
then phi.A = (nextcard (xi.A)) \/ nextcard sup (phi|A) by A4,A11;
then
A14: phi.A = nextcard (xi.A) or phi.A = nextcard sup (phi|A) by ORDINAL3:12;
A15: rng (phi|A) c= a
proof
let x be object;
assume x in rng (phi|A);
then consider y being object such that
A16: y in dom (phi|A) and
A17: x = (phi|A).y by FUNCT_1:def 3;
reconsider y as Ordinal by A16;
x = phi.y & y in cf a by A11,A13,A16,A17,FUNCT_1:47,ORDINAL1:10;
hence thesis by A10,A13,A16;
end;
(phi|A).:A = rng (phi|A) by A13,RELAT_1:113;
then card rng (phi|A) in cf a by A12,CARD_1:67,ORDINAL1:12;
then sup rng (phi|A) in a by A15,Th25;
then card sup (phi|A) in a by CARD_1:9;
then
A18: nextcard card sup (phi|A) c= a by CARD_3:90;
xi.A in rng xi by A1,A11,FUNCT_1:def 3;
then card (xi.A) in a by A2,CARD_1:9;
then
A19: nextcard card (xi.A) c= a by CARD_3:90;
A20: nextcard card sup (phi|A) <> a & nextcard card sup (phi|A) =
nextcard sup ( phi|A) by A8,Th1;
a <> nextcard card (xi.A) & nextcard card (xi.A) = nextcard (xi.A)
by A8,Th1;
hence thesis by A19,A18,A20,A14,CARD_1:3;
end;
end;
A21: for A holds P[A] from ORDINAL1:sch 2(A9);
A22: rng phi c= a
proof
let x be object;
assume x in rng phi;
then ex y being object st y in dom phi & x = phi.y by FUNCT_1:def 3;
hence thesis by A4,A21;
end;
take phi;
thus dom phi = cf a by A4;
thus rng phi c= a
proof
let x be object;
assume x in rng phi;
then ex y being object st y in dom phi & x = phi.y by FUNCT_1:def 3;
hence thesis by A4,A21;
end;
thus phi is increasing
proof
let A,B;
assume that
A23: A in B and
A24: B in dom phi;
reconsider C = phi.A as Ordinal;
A in dom phi by A23,A24,ORDINAL1:10;
then C in rng (phi|B) by A23,FUNCT_1:50;
then
A25: C in sup (phi|B) by ORDINAL2:19;
sup (phi|B) in nextcard sup (phi|B) by CARD_1:18;
then
A26: C in nextcard sup (phi|B) by A25,ORDINAL1:10;
phi.B = ( nextcard (xi.dom (phi|B))) \/ nextcard sup (phi|B) by A4,A24;
hence thesis by A26,XBOOLE_0:def 3;
end;
thus a c= sup phi
proof
let x be Ordinal;
assume x in a;
then reconsider x as Element of a;
consider A such that
A27: A in rng xi and
A28: x c= A by A3,ORDINAL2:21;
consider y being object such that
A29: y in dom xi and
A30: A = xi.y by A27,FUNCT_1:def 3;
reconsider y as Ordinal by A29;
y c= cf a by A1,A29,ORDINAL1:def 2;
then dom (phi|y) = y by A4,RELAT_1:62;
then
A in nextcard A & phi.y = ( nextcard A) \/ nextcard sup (phi|y) by A1,A4
,A29,A30,CARD_1:18;
then A in phi.y by XBOOLE_0:def 3;
then
A31: A c= phi.y by ORDINAL1:def 2;
phi.y in rng phi by A1,A4,A29,FUNCT_1:def 3;
then phi.y in sup phi by ORDINAL2:19;
hence thesis by A28,A31,ORDINAL1:12,XBOOLE_1:1;
end;
sup a = a by ORDINAL2:18;
hence sup phi c= a by A22,ORDINAL2:22;
phi is Cardinal-yielding
proof
let y be object;
assume
A32: y in dom phi;
then reconsider y as Ordinal;
y c= dom phi by A32,ORDINAL1:def 2;
then dom (phi|y) = y by RELAT_1:62;
then phi.y = ( nextcard (xi.y)) \/ nextcard sup (phi|y) by A4,A32;
hence thesis by ORDINAL3:12;
end;
hence phi is Cardinal-Function;
assume 0 in rng phi;
then consider x being object such that
A33: x in dom phi and
A34: 0 = phi.x by FUNCT_1:def 3;
reconsider x as Ordinal by A33;
x c= dom phi by A33,ORDINAL1:def 2;
then dom (phi|x) = x by RELAT_1:62;
then 0 = ( nextcard (xi.x)) \/ nextcard sup (phi|x) by A4,A33,A34;
then 0 = nextcard (xi.x) or 0 = nextcard sup (phi|x);
hence contradiction by CARD_1:15;
end;
theorem
omega is regular & nextcard a is regular
by Th21,Th22;
begin :: Infinite powers
reserve a,b for Aleph;
theorem Th30:
a c= b implies exp(a,b) = exp(2,b)
proof
A1: card bool a = exp(2,card a) by CARD_2:31;
card a = a & card a in card bool a by CARD_1:14;
then
A2: exp(a,b) c= exp(exp(2,a),b) by A1,CARD_2:92;
assume a c= b;
then
A3: exp(exp(2,a),b) = exp(2,a*`b) & a*`b = b by Th17,CARD_2:30;
2 in a by Lm2,Th15;
then exp(2,b) c= exp(a,b) by CARD_2:92;
hence thesis by A2,A3;
end;
theorem
exp(nextcard a,b) = exp(a,b) *` nextcard a
proof
now
per cases by CARD_1:4;
suppose
A1: a in b;
then a c= b by CARD_1:3;
then
A2: exp(a,b) = exp(2,b) by Th30;
nextcard a c= b by A1,CARD_3:90;
then exp(nextcard a,b) = exp(2,b) & nextcard a in exp(2,b) by Th14,Th30,
ORDINAL1:12;
hence thesis by A2,Th17;
end;
suppose
A3: b c= a;
deffunc f(Ordinal) = Funcs(b,$1);
consider phi being Sequence such that
A4: dom phi = nextcard a & for A st A in nextcard a holds phi.A = f
(A) from ORDINAL2:sch 2;
A5: cf nextcard a = nextcard a by Th22;
A6: b in nextcard a by A3,CARD_3:91;
Funcs(b,nextcard a) c= Union phi
proof
let x be object;
assume x in Funcs(b,nextcard a);
then consider f be Function such that
A7: x = f and
A8: dom f = b and
A9: rng f c= nextcard a by FUNCT_2:def 2;
reconsider f as Sequence by A8,ORDINAL1:def 7;
reconsider f as Ordinal-Sequence by A9,ORDINAL2:def 4;
sup f in nextcard a by A6,A5,A8,A9,Th26;
then
A10: phi.sup f in rng phi by A4,FUNCT_1:def 3;
rng f c= sup f by ORDINAL2:49;
then
A11: f in Funcs(b,sup f) by A8,FUNCT_2:def 2;
phi.sup f = Funcs(b,sup f) by A6,A5,A4,A8,A9,Th26;
hence thesis by A7,A11,A10,TARSKI:def 4;
end;
then
A12: card Funcs(b,nextcard a) c= card Union phi by CARD_1:11;
card Funcs(b,nextcard a) = exp(nextcard a,b) & card Union phi c=
Sum Card phi by CARD_2:def 3,CARD_3:39;
then
A13: exp(nextcard a,b) c= Sum Card phi by A12;
a in nextcard a by CARD_1:18;
then
A14: exp(nextcard a,b) *` exp(nextcard a,b) = exp(nextcard a,b) & exp(a,
b) c= exp (nextcard a,b) by CARD_2:92,CARD_4:15;
exp(nextcard a,1) = nextcard a & 1 in b by Lm1,Th15,CARD_2:27;
then nextcard a c= exp(nextcard a,b) by CARD_2:92;
then
A15: exp(a,b)*`nextcard a c= exp(nextcard a,b) by A14,CARD_2:90;
A16: now
let x be object;
reconsider xx=x as set by TARSKI:1;
A17: card card xx = card xx & card b = card b;
assume
A18: x in nextcard a;
then reconsider x9 = x as Ordinal;
A19: phi.x9 = Funcs(b,x9) by A4,A18;
card xx in nextcard a by A18,CARD_1:8,ORDINAL1:12;
then card xx c= a by CARD_3:91;
then Funcs(b,card xx) c= Funcs(b,a) by FUNCT_5:56;
then
A20: card Funcs(b,card xx) c= card Funcs(b,a) by CARD_1:11;
A21: card Funcs(b,a) = exp(a,b) by CARD_2:def 3;
(nextcard a --> exp(a,b)).x = exp(a,b) & Card phi.x = card (phi.x
) by A4,A18,CARD_3:def 2,FUNCOP_1:7;
hence Card phi.x c= (nextcard a --> exp(a,b)).x by A19,A17,A20,A21,
FUNCT_5:61;
end;
dom Card phi = dom phi & dom (nextcard a --> exp(a,b)) = nextcard a
by CARD_3:def 2;
then
A22: Sum Card phi c= Sum (nextcard a --> exp(a,b)) by A4,A16,CARD_3:30;
Sum (nextcard a --> exp(a,b)) = (nextcard a)*`exp(a,b) by CARD_2:65;
then exp(nextcard a,b) c= exp(a,b)*`nextcard a by A13,A22;
hence thesis by A15;
end;
end;
hence thesis;
end;
theorem Th32:
Sum (b-powerfunc_of a) c= exp(a,b)
proof
set X = { c where c is Element of a: c is Cardinal};
set f = X --> exp(a,b);
X c= a
proof
let x be object;
assume x in X;
then ex c being Element of a st x = c & c is Cardinal;
hence thesis;
end;
then
A1: f c= a --> exp(a,b) by FUNCT_4:4;
Sum (a --> exp(a,b)) = a*`exp( a,b) by CARD_2:65;
then
A2: Sum f c= a*`exp(a,b) by A1,CARD_3:33;
A3: dom f = X & dom (b-powerfunc_of a) = X
proof
thus dom f = X;
thus dom (b-powerfunc_of a) c= X
proof
let x be object;
assume x in dom (b-powerfunc_of a);
then x in a & x is Cardinal by Def2;
hence thesis;
end;
let x be object;
assume x in X;
then ex c being Element of a st x = c & c is Cardinal;
hence thesis by Def2;
end;
1 in b & exp(a,1) = a by Lm1,Th15,CARD_2:27;
then a c= exp(a,b) by CARD_2:93;
then
A4: a*`exp(a,b) = exp(a,b) by Th17;
now
let x be object;
assume
A5: x in X;
then consider c being Element of a such that
A6: x = c and
A7: c is Cardinal;
reconsider c as Cardinal by A7;
A8: f.x = exp(a,b) by A5,FUNCOP_1:7;
(b-powerfunc_of a).x = exp(c,b) by A6,Def2;
hence (b-powerfunc_of a).x c= f.x by A8,CARD_2:93;
end;
then Sum (b-powerfunc_of a) c= Sum f by A3,CARD_3:30;
hence thesis by A2,A4;
end;
theorem
a is limit_cardinal & b in cf a implies exp(a,b) = Sum (b-powerfunc_of
a)
proof
assume that
A1: a is limit_cardinal and
A2: b in cf a;
deffunc f(Ordinal) = Funcs(b,$1);
consider L being Sequence such that
A3: dom L = a & for A st A in a holds L.A = f(A) from ORDINAL2:sch 2;
A4: now
let x be object;
A5: card Union (b-powerfunc_of a) c= Sum (b-powerfunc_of a) by CARD_3:40;
assume
A6: x in a;
then reconsider x9 = x as Ordinal;
set m = card x9;
A7: m in a by A6,CARD_1:8,ORDINAL1:12;
then m in dom (b-powerfunc_of a) by Def2;
then
A8: (b-powerfunc_of a).(card x9) in rng (b-powerfunc_of a) by FUNCT_1:def 3;
x9,m are_equipotent by CARD_1:def 2;
then
A9: card Funcs(b,x9) = card Funcs(b,card x9) by FUNCT_5:60;
L.x = Funcs(b,x9) & (Card L).x = card (L.x) by A3,A6,CARD_3:def 2;
then
A10: (Card L).x = exp(m,b) by A9,CARD_2:def 3;
(b-powerfunc_of a).(card x9) = exp(card x9,b) by A7,Def2;
then card exp(card x9,b) c= card Union (b-powerfunc_of a) by A8,CARD_1:11
,ZFMISC_1:74;
then
A11: card exp(card x9,b) c= Sum (b-powerfunc_of a) by A5;
thus (Card L).x c= (a --> Sum (b-powerfunc_of a)).x by A6,A10,A11,
FUNCOP_1:7;
end;
dom (a --> Sum (b-powerfunc_of a)) = a & dom Card L = dom L by CARD_3:def 2
;
then
A12: Sum Card L c= Sum (a --> Sum (b-powerfunc_of a)) by A3,A4,CARD_3:30;
a c= Sum (b-powerfunc_of a)
proof
let x be Ordinal;
reconsider xx=x as set;
assume
A13: x in a;
reconsider x9 = x as Ordinal;
set m = card x9;
m in a by A13,CARD_1:8,ORDINAL1:12;
then
A14: nextcard m c= a by CARD_3:90;
nextcard m <> a by A1;
then
A15: nextcard m in a by A14,CARD_1:3;
then nextcard m in dom (b-powerfunc_of a) by Def2;
then
A16: (b-powerfunc_of a).(nextcard m) in rng (b-powerfunc_of a) by FUNCT_1:def 3
;
(b-powerfunc_of a).(nextcard m) = exp(nextcard m,b) by A15,Def2;
then
A17: card exp(nextcard m,b) c= card Union (b-powerfunc_of a) by A16,CARD_1:11
,ZFMISC_1:74;
A18: nextcard m c= exp(nextcard m,b) by Th19;
card xx = card card xx;
then
A19: x9 in nextcard x9 & nextcard card xx = nextcard xx by CARD_1:18,CARD_3:88;
card exp(nextcard m,b) = exp(nextcard m,b) & card Union (b
-powerfunc_of a) c= Sum (b-powerfunc_of a) by CARD_3:40;
then exp(nextcard m,b) c= Sum (b-powerfunc_of a) by A17;
then nextcard card xx c= Sum (b-powerfunc_of a) by A18;
hence thesis by A19;
end;
then
A20: a*`Sum (b-powerfunc_of a) = Sum (b-powerfunc_of a) by Th17;
Funcs(b,a) c= Union L
proof
let x be object;
assume x in Funcs(b,a);
then consider f such that
A21: x = f and
A22: dom f = b and
A23: rng f c= a by FUNCT_2:def 2;
reconsider f as Sequence by A22,ORDINAL1:def 7;
reconsider f as Ordinal-Sequence by A23,ORDINAL2:def 4;
rng f c= sup f by ORDINAL2:49;
then
A24: x in Funcs(b,sup f) by A21,A22,FUNCT_2:def 2;
sup f in a by A2,A22,A23,Th26;
then
A25: L.sup f in rng L by A3,FUNCT_1:def 3;
L.sup f = Funcs(b,sup f) by A2,A3,A22,A23,Th26;
hence thesis by A24,A25,TARSKI:def 4;
end;
then
A26: card Funcs(b,a) c= card Union L by CARD_1:11;
card Union L c= Sum Card L by CARD_3:39;
then card Funcs(b,a) c= Sum Card L by A26;
then
A27: exp(a,b) c= Sum Card L by CARD_2:def 3;
A28: Sum (b-powerfunc_of a) c= exp(a,b) by Th32;
Sum (a --> Sum (b-powerfunc_of a)) = a*`Sum (b-powerfunc_of a) by CARD_2:65;
then exp(a,b) c= a*`Sum (b-powerfunc_of a) by A27,A12;
hence thesis by A28,A20;
end;
theorem
cf a c= b & b in a implies exp(a,b) = exp(Sum (b-powerfunc_of a), cf a)
proof
assume that
A1: cf a c= b and
A2: b in a;
consider phi such that
A3: dom phi = cf a and
A4: rng phi c= a and
phi is increasing and
A5: a = sup phi and
A6: phi is Cardinal-Function and
A7: not 0 in rng phi by A1,A2,Th28,ORDINAL1:12;
defpred R[object,object] means
ex g,h st g = $1 & h = $2 & dom g = b & rng g c= a
& dom h = cf a & for y st y in cf a ex fx st h.y = [fx,phi.y] & dom fx = b &
for z st z in b holds (g.z in phi.y implies fx.z = g.z) & (not g.z in phi.y
implies fx.z = 0);
A8: for x being object st x in Funcs(b,a) ex x1 being object st R[x,x1]
proof
let x be object;
assume x in Funcs(b,a);
then consider g such that
A9: x = g & dom g = b & rng g c= a by FUNCT_2:def 2;
defpred P[object,object]
means ex fx st $2 = [fx,phi.$1] & dom fx = b & for z st
z in b holds (g.z in phi.$1 implies fx.z = g.z) & (not g.z in phi.$1 implies fx
.z = 0);
A10: for y being object st y in cf a ex x2 being object st P[y,x2]
proof
deffunc g(object) = 0;
deffunc f(object) = g.$1;
let y be object such that
y in cf a;
defpred C[object] means g.$1 in phi.y;
consider fx such that
A11: dom fx = b &
for z being object st z in b holds (C[z] implies fx.z = f(z)) &
(not C[z] implies fx.z = g(z)) from PARTFUN1:sch 1;
take [fx,phi.y], fx;
thus thesis by A11;
end;
consider h such that
A12: dom h = cf a &
for y being object st y in cf a holds P[y,h.y] from CLASSES1:
sch 1 ( A10);
take h, g, h;
thus thesis by A9,A12;
end;
consider f such that
A13: dom f = Funcs(b,a) &
for x being object st x in Funcs(b,a) holds R[x,f.x] from
CLASSES1:sch 1(A8);
deffunc f(set) = Funcs(b,$1);
consider F being Function such that
A14: dom F = dom (b-powerfunc_of a) &
for x being set st x in dom (b-powerfunc_of a)
holds F.x = f(x) from FUNCT_1:sch 5;
A15: rng f c= Funcs(cf a, Union disjoin F)
proof
let y be object;
assume y in rng f;
then consider x being object such that
A16: x in dom f and
A17: y = f.x by FUNCT_1:def 3;
consider g,h such that
g = x and
A18: h = f.x and
dom g = b and
rng g c= a and
A19: dom h = cf a and
A20: for y st y in cf a ex fx st h.y = [fx,phi.y] & dom fx = b & for z
st z in b holds (g.z in phi.y implies fx.z = g.z) & (not g.z in phi.y implies
fx.z = 0) by A13,A16;
rng h c= Union disjoin F
proof
let x1 be object;
assume x1 in rng h;
then consider x2 being object such that
A21: x2 in dom h and
A22: x1 = h.x2 by FUNCT_1:def 3;
consider fx such that
A23: x1 = [fx,phi.x2] and
A24: dom fx = b and
A25: for z st z in b holds (g.z in phi.x2 implies fx.z = g.z) & (not
g.z in phi.x2 implies fx.z = 0) by A19,A20,A21,A22;
rng fx c= phi.x2
proof
reconsider x2 as Ordinal by A19,A21;
let z be object;
reconsider A = phi.x2 as Ordinal;
assume z in rng fx;
then consider z9 being object such that
A26: z9 in dom fx & z = fx.z9 by FUNCT_1:def 3;
A27: z = g.z9 & g.z9 in phi.x2 or z = 0 by A24,A25,A26;
A <> 0 by A3,A7,A19,A21,FUNCT_1:def 3;
hence thesis by A27,ORDINAL3:8;
end;
then
A28: fx in Funcs(b,phi.x2) by A24,FUNCT_2:def 2;
A29: [fx,phi.x2]`1 = fx & [fx,phi.x2]`2 = phi.x2;
phi.x2 in rng phi & phi.x2 is Cardinal by A3,A6,A19,A21,CARD_3:def 1
,FUNCT_1:def 3;
then
A30: phi.x2 in dom (b-powerfunc_of a) by A4,Def2;
then F.(phi.x2) = Funcs(b,phi.x2) by A14;
hence thesis by A14,A23,A28,A30,A29,CARD_3:22;
end;
hence thesis by A17,A18,A19,FUNCT_2:def 2;
end;
card card Union disjoin F = card Union disjoin F & card cf a = cf a;
then
A31: card Funcs(cf a, Union disjoin F) = card Funcs(cf a, card Union
disjoin F) by FUNCT_5:61
.= exp(card Union disjoin F, cf a) by CARD_2:def 3;
A32: dom Card F = dom F by CARD_3:def 2;
A33: f is one-to-one
proof
let x,y be object;
assume that
A34: x in dom f and
A35: y in dom f and
A36: f.x = f.y;
consider g1, h1 being Function such that
A37: g1 = x and
A38: h1 = f.x and
A39: dom g1 = b and
A40: rng g1 c= a and
dom h1 = cf a and
A41: for x1 being object st x1 in cf a ex fx st h1.x1 = [fx,phi.x1] & dom
fx = b &
for z being object st z in b holds (g1.z in phi.x1 implies fx.z = g1.z) &
(not g1.z
in phi.x1 implies fx.z = 0) by A13,A34;
consider g2, h2 being Function such that
A42: g2 = y and
A43: h2 = f.y and
A44: dom g2 = b and
A45: rng g2 c= a and
dom h2 = cf a and
A46: for x2 being object st x2 in cf a ex fx st h2.x2 = [fx,phi.x2] & dom
fx = b &
for z being object st z in b holds (g2.z in phi.x2 implies fx.z = g2.z) &
(not g2.z in phi.x2 implies fx.z = 0) by A13,A35;
now
let x1 be object;
assume x1 in b;
then reconsider X = x1 as Element of b;
g1.X in rng g1 & g2.X in rng g2 by A39,A44,FUNCT_1:def 3;
then reconsider A1 = g1.x1, A2 = g2.x1 as Element of a by A40,A45;
set A = A1 \/ A2;
A = A1 or A = A2 by ORDINAL3:12;
then succ A in a by ORDINAL1:28;
then consider B such that
A47: B in rng phi and
A48: succ A c= B by A5,ORDINAL2:21;
consider x2 being object such that
A49: x2 in dom phi and
A50: B = phi.x2 by A47,FUNCT_1:def 3;
A51: A in succ A by ORDINAL1:6;
then
A52: A2 in B by A48,ORDINAL1:12,XBOOLE_1:7;
consider f1 being Function such that
A53: h1.x2 = [f1,phi.x2] and
dom f1 = b and
A54: for z st z in b holds (g1.z in phi.x2 implies f1.z = g1.z) & (
not g1.z in phi.x2 implies f1.z = 0) by A3,A41,A49;
A1 in B by A48,A51,ORDINAL1:12,XBOOLE_1:7;
then
A55: f1.X = g1.x1 by A50,A54;
consider f2 being Function such that
A56: h2.x2 = [f2,phi.x2] and
dom f2 = b and
A57: for z st z in b holds (g2.z in phi.x2 implies f2.z = g2.z) & (
not g2.z in phi.x2 implies f2.z = 0) by A3,A46,A49;
f1 = f2 by A36,A38,A43,A53,A56,XTUPLE_0:1;
hence g1.x1 = g2.x1 by A50,A57,A52,A55;
end;
hence thesis by A37,A39,A42,A44,FUNCT_1:2;
end;
A58: dom disjoin F = dom F by CARD_3:def 3;
A59: now
let x be object;
assume
A60: x in dom F;
then
A61: (disjoin F).x = [:F.x,{x}:] by CARD_3:def 3;
(Card F).x = card (F.x) & (Card disjoin F).x = card ((disjoin F).x)
by A58,A60,CARD_3:def 2;
hence (Card disjoin F).x = (Card F).x by A61,CARD_1:69;
end;
now
let x be object;
assume
A62: x in dom F;
then reconsider M = x as Cardinal by A14,Def2;
M in a by A14,A62,Def2;
then
A63: (b-powerfunc_of a).M = exp(M,b) by Def2;
reconsider xx=x as set by TARSKI:1;
(Card F).x = card (F.x) & F.x = Funcs(b,xx) by A14,A62,CARD_3:def 2;
hence (Card F).x = (b-powerfunc_of a).x by A63,CARD_2:def 3;
end;
then
A64: Card F = b-powerfunc_of a by A14,A32;
dom Card disjoin F = dom disjoin F by CARD_3:def 2;
then Card F = Card disjoin F by A58,A32,A59;
then card Union disjoin F c= Sum (b-powerfunc_of a) by A64,CARD_3:39;
then
A65: exp(card Union disjoin F, cf a) c= exp(Sum (b-powerfunc_of a), cf a)
by CARD_2:93;
exp(a,b) = card Funcs(b,a) by CARD_2:def 3;
then exp(a,b) c= card Funcs(cf a, Union disjoin F) by A13,A33,A15,CARD_1:10;
then
A66: exp(exp(a,b), cf a) = exp(a,b*`cf a) & exp(a,b) c= exp(Sum (b
-powerfunc_of a ), cf a) by A31,A65,CARD_2:30;
Sum (b-powerfunc_of a) c= exp(a,b) by Th32;
then
A67: exp(Sum (b-powerfunc_of a), cf a) c= exp(exp(a,b), cf a) by CARD_2:93;
b*`cf a = b by A1,Th17;
hence thesis by A67,A66;
end;
reserve O for Ordinal,
F for Subset of omega;
:: from AMISTD_3, 2010.10.01, A.T.
Lm4: for X being finite set st X c= O holds order_type_of RelIncl X is finite
proof
let X be finite set;
assume X c= O;
then RelIncl X is well-ordering by WELLORD2:8;
then RelIncl X,RelIncl order_type_of RelIncl X are_isomorphic by
WELLORD2:def 2;
hence thesis by CARD_3:105;
end;
theorem Th35:
for X being finite set st X c= O holds order_type_of RelIncl X =
card X
proof
let X be finite set;
assume
A1: X c= O;
then order_type_of RelIncl X is finite by Lm4;
then reconsider o = order_type_of RelIncl X as Nat;
card X = card order_type_of RelIncl X by A1,Th7;
then o = card X;
hence thesis;
end;
theorem Th36:
{x} c= O implies order_type_of RelIncl {x} = 1
proof
card {x} = 1 by CARD_2:42;
hence thesis by Th35;
end;
theorem
{x} c= O implies canonical_isomorphism_of (RelIncl order_type_of
RelIncl {x}, RelIncl {x}) = 0 .--> x
proof
set X = {x};
set R = RelIncl X;
set C = canonical_isomorphism_of (RelIncl order_type_of R,R);
A1: RelIncl {0} = {[0,0]} by WELLORD2:22;
assume
A2: X c= O;
then
A3: order_type_of R = {0} by Th36,CARD_1:49;
R is well-ordering by A2,WELLORD2:8;
then R, RelIncl order_type_of R are_isomorphic by WELLORD2:def 2;
then
A4: RelIncl order_type_of R, R are_isomorphic by WELLORD1:40;
RelIncl order_type_of R is well-ordering by WELLORD2:8;
then
A5: C is_isomorphism_of RelIncl order_type_of R, R by A4,WELLORD1:def 9;
then
A6: rng canonical_isomorphism_of(RelIncl {0}, R) = field R by A3,WELLORD1:def 7
.= X by WELLORD2:def 1;
dom canonical_isomorphism_of(RelIncl {0}, R) = field RelIncl {0} by A5,A3,
WELLORD1:def 7
.= {0} by A1,RELAT_1:173;
hence thesis by A3,A6,FUNCT_4:112;
end;
registration
let O be Ordinal, X be Subset of O, n be set;
cluster canonical_isomorphism_of (RelIncl order_type_of RelIncl X,RelIncl X)
.n -> ordinal;
coherence
proof
consider phi being Ordinal-Sequence such that
A1: phi = canonical_isomorphism_of(RelIncl order_type_of RelIncl X,
RelIncl X) and
phi is increasing and
dom phi = order_type_of RelIncl X and
rng phi = X by Th5;
per cases;
suppose
n in dom phi;
thus thesis by A1;
end;
suppose
not n in dom phi;
thus thesis by A1;
end;
end;
end;
registration
let X be natural-membered set, n be set;
cluster canonical_isomorphism_of
(RelIncl order_type_of RelIncl X,RelIncl X).n -> natural;
coherence
proof
X c= NAT
by ORDINAL1:def 12;
then reconsider X as Subset of NAT;
consider phi being Ordinal-Sequence such that
A1: phi = canonical_isomorphism_of(RelIncl order_type_of RelIncl X,
RelIncl X) and
phi is increasing and
dom phi = order_type_of RelIncl X and
A2: rng phi = X by Th5;
per cases;
suppose
A3: n in dom phi;
phi.n in rng phi by A3,FUNCT_1:def 3;
hence thesis by A1,A2;
end;
suppose
not n in dom phi;
hence thesis by A1,FUNCT_1:def 2;
end;
end;
end;
theorem
card F c= order_type_of RelIncl F
proof
card F = card order_type_of RelIncl F by Th7;
hence thesis by CARD_1:8;
end;