:: Cardinal Numbers
:: by Grzegorz Bancerek
::
:: Received September 19, 1989
:: Copyright (c) 1990-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies ORDINAL1, RELAT_1, FUNCT_1, XBOOLE_0, TARSKI, WELLORD1, WELLORD2,
ZFMISC_1, ORDINAL2, FUNCOP_1, FINSET_1, SUBSET_1, MCART_1, CARD_1,
BSPACE, NAT_1, XCMPLX_0, FUNCT_4, QUANTAL1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, ENUMSET1, XTUPLE_0,
MCART_1, FUNCT_1, FUNCOP_1, WELLORD1, ORDINAL1, ORDINAL2, WELLORD2,
FINSET_1, FUNCT_4;
constructors ENUMSET1, WELLORD1, WELLORD2, FUNCOP_1, ORDINAL2, FINSET_1,
XTUPLE_0, FUNCT_4;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, ORDINAL1, FUNCOP_1, FINSET_1,
ZFMISC_1, XTUPLE_0, FUNCT_4;
requirements NUMERALS, SUBSET, BOOLE;
definitions TARSKI, FUNCT_1, FINSET_1, WELLORD2, XBOOLE_0, RELAT_1;
equalities ORDINAL1, RELAT_1;
expansions ORDINAL1, TARSKI, FUNCT_1, FINSET_1, WELLORD2, XBOOLE_0;
theorems TARSKI, FUNCT_1, ZFMISC_1, ORDINAL1, ORDINAL2, WELLORD1, WELLORD2,
RELAT_1, FINSET_1, XBOOLE_0, XBOOLE_1, FUNCOP_1, ENUMSET1, ORDINAL3,
MCART_1, XTUPLE_0, FUNCT_4;
schemes ORDINAL1, ORDINAL2, FUNCT_1, FINSET_1, XBOOLE_0, PARTFUN1;
begin
reserve A,B,C for Ordinal,
X,X1,Y,Y1,Z for set,a,b,b1,b2,x,y,z for object,
R for Relation,
f,g,h for Function,
k,m,n for Nat;
definition
let IT be object;
attr IT is cardinal means
:Def1:
ex B st IT = B & for A st A,B are_equipotent holds B c= A;
end;
registration
cluster cardinal for set;
existence
proof
set A = the Ordinal;
defpred P[Ordinal] means $1,A are_equipotent;
A1: ex A st P[A];
consider B such that
A2: P[B] & for C st P[C] holds B c= C from ORDINAL1:sch 1(A1);
reconsider IT = B as set;
take IT,B;
thus thesis by A2,WELLORD2:15;
end;
end;
definition
mode Cardinal is cardinal set;
end;
registration
cluster cardinal -> ordinal for set;
coherence;
end;
reserve M,N for Cardinal;
::$CT
theorem Th1:
M,N are_equipotent implies M = N
proof
A1: ex A st M = A & for C st C,A are_equipotent holds A c= C by Def1;
ex B st N = B & for C st C,B are_equipotent holds B c= C by Def1;
hence thesis by A1;
end;
theorem
M in N iff M c= N & M <> N by ORDINAL1:11,XBOOLE_0:def 8;
theorem
M in N iff not N c= M by ORDINAL1:5,16;
definition
let X;
func card X -> Cardinal means
:Def2:
X, it are_equipotent;
existence
proof
defpred P[Ordinal] means X,$1 are_equipotent;
consider R such that
A1: R well_orders X by WELLORD2:17;
set Q = R|_2 X, A = order_type_of Q;
Q is well-ordering by A1,WELLORD2:16;
then Q,RelIncl A are_isomorphic by WELLORD2:def 2;
then consider f such that
A2: f is_isomorphism_of Q,RelIncl A by WELLORD1:def 8;
X,A are_equipotent
proof
take f;
dom f = field Q & rng f = field RelIncl A by A2,WELLORD1:def 7;
hence thesis by A1,A2,WELLORD1:def 7,WELLORD2:16,def 1;
end;
then
A3: ex A st P[A];
consider A such that
A4: P[A] & for B st P[B] holds A c= B from ORDINAL1:sch 1(A3);
A is cardinal
proof
take A;
thus A = A;
let B;
assume B,A are_equipotent;
hence thesis by A4,WELLORD2:15;
end;
then reconsider M = A as Cardinal;
take M;
thus thesis by A4;
end;
uniqueness by Th1,WELLORD2:15;
projectivity;
end;
registration let C be Cardinal;
reduce card C to C;
reducibility by Def2;
end;
registration
cluster empty -> cardinal for set;
coherence
proof
let S be set;
assume
A1: S is empty;
take {};
thus S = {} by A1;
let A such that
A,{} are_equipotent;
thus thesis;
end;
end;
registration
let X be empty set;
cluster card X -> empty;
coherence;
end;
registration
let X be empty set;
cluster card X -> zero;
coherence;
end;
registration
let X be non empty set;
cluster card X -> non empty;
coherence
proof
assume card X is empty;
then ex f st f is one-to-one & dom f = X & rng f = {}
by Def2,WELLORD2:def 4;
hence contradiction by RELAT_1:42;
end;
end;
registration
let X be non empty set;
cluster card X -> non zero;
coherence;
end;
theorem Th4:
X,Y are_equipotent iff card X = card Y
proof
A1: Y,card Y are_equipotent by Def2;
A2: X,card X are_equipotent by Def2;
hence X,Y are_equipotent implies card X = card Y by Def2,WELLORD2:15;
assume card X = card Y;
hence thesis by A2,A1,WELLORD2:15;
end;
theorem Th5:
R is well-ordering implies field R,order_type_of R are_equipotent
proof
assume R is well-ordering;
then R,RelIncl order_type_of R are_isomorphic by WELLORD2:def 2;
then consider f such that
A1: f is_isomorphism_of R,RelIncl order_type_of R by WELLORD1:def 8;
take f;
field RelIncl order_type_of R = order_type_of R by WELLORD2:def 1;
hence thesis by A1,WELLORD1:def 7;
end;
theorem Th6:
X c= M implies card X c= M
proof
defpred P[Ordinal] means $1 c= M & X,$1 are_equipotent;
reconsider m = M as Ordinal;
assume X c= M;
then
A1: order_type_of RelIncl X c= m & RelIncl X is well-ordering by WELLORD2:8,14;
field RelIncl X = X by WELLORD2:def 1;
then
A2: ex A st P[A] by A1,Th5;
consider A such that
A3: P[A] & for B st P[B] holds A c= B from ORDINAL1:sch 1(A2);
A is cardinal
proof
take A;
thus A = A;
let B;
assume
A4: B,A are_equipotent;
assume
A5: not A c= B;
then m c= B by A3,A4,WELLORD2:15;
hence contradiction by A3,A5;
end;
then reconsider A as Cardinal;
card X = A by A3,Def2;
hence thesis by A3;
end;
theorem Th7:
card A c= A
proof
( ex B st card A = B & for C st C,B are_equipotent holds B c= C)& A,card
A are_equipotent by Def1,Def2;
hence thesis;
end;
theorem
X in M implies card X in M by Th7,ORDINAL1:12;
::$N Cantor-Bernstein Theorem
theorem Th9:
card X c= card Y iff ex f st f is one-to-one & dom f = X & rng f c= Y
proof
thus card X c= card Y implies ex f st f is one-to-one & dom f = X & rng f c=
Y
proof
consider f such that
A1: f is one-to-one and
A2: dom f = X & rng f = card X by Def2,WELLORD2:def 4;
assume
A3: card X c= card Y;
consider g such that
A4: g is one-to-one and
A5: dom g = Y & rng g = card Y by Def2,WELLORD2:def 4;
take h = g"*f;
thus h is one-to-one by A1,A4;
rng g = dom(g") & dom g = rng(g") by A4,FUNCT_1:33;
hence thesis by A3,A2,A5,RELAT_1:26,27;
end;
given f such that
A6: f is one-to-one and
A7: dom f = X & rng f c= Y;
consider g such that
A8: g is one-to-one and
A9: dom g = Y and
A10: rng g = card Y by Def2,WELLORD2:def 4;
A11: X,rng(g*f) are_equipotent
proof
take g*f;
thus g*f is one-to-one by A6,A8;
thus dom(g*f) = X by A7,A9,RELAT_1:27;
thus thesis;
end;
A12: rng(g*f),card rng(g*f) are_equipotent by Def2;
card rng(g*f) c= card Y by A10,Th6,RELAT_1:26;
hence thesis by A12,Def2,A11,WELLORD2:15;
end;
theorem Th10:
X c= Y implies card X c= card Y
proof
assume
A1: X c= Y;
ex f st f is one-to-one & dom f = X & rng f c= Y
proof
take id X;
thus thesis by A1,RELAT_1:45;
end;
hence thesis by Th9;
end;
theorem Th11:
card X c= card Y iff ex f st dom f = Y & X c= rng f
proof
thus card X c= card Y implies ex f st dom f = Y & X c= rng f
proof
assume card X c= card Y;
then consider f such that
A1: f is one-to-one and
A2: dom f = X and
A3: rng f c= Y by Th9;
defpred P[object,object] means
$1 in rng f & $2 = f".$1 or not $1 in rng f & $2
= 0;
A4: for x being object st x in Y ex y being object st P[x,y]
proof
let x being object such that
x in Y;
not x in rng f implies thesis;
hence thesis;
end;
A5: for x,y,z being object st x in Y & P[x,y] & P[x,z] holds y = z;
consider g such that
A6: dom g = Y & for y being object st y in Y holds P[y,g.y]
from FUNCT_1:sch 2(A5,
A4);
take g;
thus dom g = Y by A6;
let x be object;
assume
A7: x in X;
then
A8: f.x in rng f by A2,FUNCT_1:def 3;
f".(f.x) = x by A1,A2,A7,FUNCT_1:34;
then x = g.(f.x) by A3,A6,A8;
hence thesis by A3,A6,A8,FUNCT_1:def 3;
end;
given f such that
A9: dom f = Y and
A10: X c= rng f;
deffunc f(object) = f"{$1};
consider g such that
A11: dom g = X &
for x being object st x in X holds g.x = f(x) from FUNCT_1:sch 3;
per cases;
suppose X <> {};
then reconsider M = rng g as non empty set by A11,RELAT_1:42;
for Z st Z in M holds Z <> {}
proof
let Z;
assume Z in M;
then consider x being object such that
A12: x in dom g & Z = g.x by FUNCT_1:def 3;
A13: x in {x} by TARSKI:def 1;
Z = f"{x} & ex y being object st y in dom f & x = f.y
by A10,A11,A12,FUNCT_1:def 3;
hence thesis by A13,FUNCT_1:def 7;
end;
then consider F being Function such that
A14: dom F = M and
A15: for Z st Z in M holds F.Z in Z by FUNCT_1:111;
A16: dom(F*g) = X by A11,A14,RELAT_1:27;
A17: F*g is one-to-one
proof
let x,y be object;
assume that
A18: x in dom(F*g) and
A19: y in dom(F*g) and
A20: (F*g).x = (F*g).y;
A21: g.y = f"{y} by A11,A16,A19;
then f"{y} in M by A11,A16,A19,FUNCT_1:def 3;
then F.(f"{y}) in f"{y} by A15;
then
A22: f.(F.(f"{y})) in {y} by FUNCT_1:def 7;
A23: g.x = f"{x} by A11,A16,A18;
then f"{x} in M by A11,A16,A18,FUNCT_1:def 3;
then F.(f"{x}) in f"{x} by A15;
then f.(F.(f"{x})) in {x} by FUNCT_1:def 7;
then
A24: f.(F.(f"{x})) = x by TARSKI:def 1;
(F*g).x = F.(g.x) & (F*g).y = F. ( g.y) by A11,A16,A18,A19,FUNCT_1:13;
hence thesis by A20,A23,A21,A22,A24,TARSKI:def 1;
end;
rng(F*g) c= Y
proof
let x be object;
assume x in rng(F*g);
then consider y being object such that
A25: y in dom(F*g) and
A26: x = (F*g).y by FUNCT_1:def 3;
A27: x = F.(g.y) by A11,A16,A25,A26,FUNCT_1:13;
A28: g.y = f"{y} by A11,A16,A25;
then f"{y} in M by A11,A16,A25,FUNCT_1:def 3;
then x in f"{y} by A15,A28,A27;
hence thesis by A9,FUNCT_1:def 7;
end;
hence thesis by A16,A17,Th9;
end;
suppose X = {};
hence thesis;
end;
end;
theorem Th12:
not X,bool X are_equipotent
proof
given f such that
f is one-to-one and
A1: dom f = X & rng f = bool X;
defpred P[object] means for Y st Y = f.$1 holds not $1 in Y;
consider Z such that
A2: for a being object holds a in Z iff a in X & P[a] from XBOOLE_0:sch 1;
Z c= X
by A2;
then consider a being object such that
A3: a in X and
A4: Z = f.a by A1,FUNCT_1:def 3;
ex Y st Y = f.a & a in Y by A2,A3,A4;
hence contradiction by A2,A4;
end;
::$N Cantor Theorem
::$L https://en.wikipedia.org/wiki/Cantor's_theorem Cantor Theorem
theorem Th13:
card X in card bool X
proof
deffunc f(object) = {$1};
consider f such that
A1: dom f = X &
for x being object st x in X holds f.x = f(x) from FUNCT_1:sch 3;
A2: rng f c= bool X
proof
let x be object;
assume x in rng f;
then consider y being object such that
A3: y in dom f and
A4: x = f.y by FUNCT_1:def 3;
A5: { y } c= X
by A1,A3,TARSKI:def 1;
f.y = { y } by A1,A3;
hence thesis by A4,A5;
end;
A6: card X <> card bool X by Th4,Th12;
f is one-to-one
proof
let x,y be object;
assume that
A7: x in dom f & y in dom f and
A8: f.x = f.y;
f.x = { x } & f.y = { y } by A1,A7;
hence thesis by A8,ZFMISC_1:3;
end;
then card X c= card bool X by A1,A2,Th9;
hence thesis by A6,ORDINAL1:11,XBOOLE_0:def 8;
end;
definition
let X;
func nextcard X -> Cardinal means
:Def3:
card X in it & for M st card X in M holds it c= M;
existence
proof
defpred P[Ordinal] means ex M st $1 = M & card X in M;
card X in card bool X by Th13;
then
A1: ex A st P[A];
consider A such that
A2: P[A] and
A3: for B st P[B] holds A c= B from ORDINAL1:sch 1(A1);
consider M such that
A4: A = M and
A5: card X in M by A2;
take M;
thus card X in M by A5;
let N;
assume card X in N;
hence thesis by A3,A4;
end;
uniqueness;
end;
theorem
{} in nextcard X
proof
card {} c= card X & card X in nextcard X by Def3;
hence thesis by ORDINAL1:12;
end;
theorem Th15:
card X = card Y implies nextcard X = nextcard Y
proof
assume
A1: card X = card Y;
card X in nextcard X & for N st card X in N holds nextcard X c= N by Def3;
hence thesis by A1,Def3;
end;
theorem Th16:
X,Y are_equipotent implies nextcard X = nextcard Y
proof
assume X,Y are_equipotent;
then card X = card Y by Th4;
hence thesis by Th15;
end;
theorem Th17:
A in nextcard A
proof
assume not A in nextcard A;
then
A1: card nextcard A c= card A by Th10,ORDINAL1:16;
A2: nextcard card A = nextcard A by Def2,Th16;
A3: card card A in nextcard card A by Def3;
thus contradiction by A1,A2,A3,ORDINAL1:5;
end;
reserve S for Sequence;
definition
let M;
attr M is limit_cardinal means
not ex N st M = nextcard N;
end;
definition
let A;
func aleph A -> set means
:Def5:
ex S st it = last S & dom S = succ A & S.0 = card omega &
(for B st succ B in succ A holds S.succ B = nextcard(S.B)) &
for B st B in succ A & B <> 0 & B is limit_ordinal holds S.B = card sup(S|B);
correctness
proof
set B = card omega;
deffunc D(Ordinal,Sequence) = card sup $2;
deffunc C(Ordinal,set) = nextcard $2;
(ex x,S st x = last S & dom S = succ A & S.0 = B &
(for C st succ C
in succ A holds S.succ C = C(C,S.C)) & for C st C in succ A & C <> 0 & C is
limit_ordinal holds S.C = D(C,S|C) ) &
for x1,x2 being set st (ex S st x1 =
last S & dom S = succ A & S.0 = B & (for C st succ C in succ A holds S.succ C
= C(C,S.C)) & for C st C in succ A & C <> 0 & C is limit_ordinal holds S.C = D
(C,S|C) ) & (ex S st x2 = last S & dom S = succ A & S.0 = B & (for C st succ C
in succ A holds S.succ C = C(C,S.C)) & for C st C in succ A & C <> 0 & C is
limit_ordinal holds S.C = D(C,S|C) ) holds x1 = x2 from ORDINAL2:sch 7;
hence thesis;
end;
end;
Lm1: now
deffunc D(Ordinal,Sequence) = card sup $2;
deffunc C(Ordinal,set) = nextcard $2;
deffunc F(Ordinal) = aleph $1;
A1: for A,x holds x = F(A) iff ex S st x = last S & dom S = succ A & S.0 =
card omega & (for C st succ C in succ A holds S.succ C = C(C,S.C)) & for C st C
in succ A & C <> 0 & C is limit_ordinal holds S.C = D(C,S|C) by Def5;
F(0) = card omega from ORDINAL2:sch 8(A1);
hence aleph 0 = card omega;
thus for A holds F(succ A) = C(A,F(A)) from ORDINAL2:sch 9(A1);
thus A <> 0 & A is limit_ordinal implies for S st dom S = A & for B st B in
A holds S.B = aleph B holds aleph A = card sup S
proof
assume
A2: A <> 0 & A is limit_ordinal;
let S such that
A3: dom S = A and
A4: for B st B in A holds S.B = F(B);
thus F(A) = D(A,S) from ORDINAL2:sch 10(A1,A2,A3,A4);
end;
end;
deffunc f(Ordinal) = aleph $1;
registration
let A;
cluster aleph A -> cardinal;
coherence
proof
A1: now
consider S such that
A2: dom S = A & for B st B in A holds S.B = f(B) from ORDINAL2:sch 2;
assume that
A3: A <> {} and
A4: for B holds A <> succ B;
aleph A = card sup S by A3,A2,Lm1,A4,ORDINAL1:29;
hence aleph A is Cardinal;
end;
now
given B such that
A5: A = succ B;
aleph A = nextcard aleph B by A5,Lm1;
hence thesis;
end;
hence thesis by A1,Lm1;
end;
end;
theorem
aleph succ A = nextcard aleph A by Lm1;
theorem
A <> {} & A is limit_ordinal implies for S st dom S = A & for B st B
in A holds S.B = aleph B holds aleph A = card sup S by Lm1;
theorem Th20:
A in B iff aleph A in aleph B
proof
defpred P[Ordinal] means for A st A in $1 holds aleph A in aleph $1;
A1: for B st P[B] holds P[succ B]
proof
let B such that
A2: P[B];
let A;
A3: aleph succ B = nextcard aleph B by Lm1;
A4: now
assume A in B;
then
A5: aleph A in aleph B by A2;
aleph B in nextcard aleph B by Th17;
hence thesis by A3,A5,ORDINAL1:10;
end;
A6: A c< B iff A c= B & A <> B;
assume A in succ B;
hence thesis by A3,A6,A4,Th17,ORDINAL1:11,22;
end;
A7: 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
A8: B <> 0 and
A9: B is limit_ordinal and
for C st C in B for A st A in C holds aleph A in aleph C;
let A;
consider S such that
A10: dom S = B & for C st C in B holds S.C = f(C) from ORDINAL2:sch 2;
assume A in B;
then succ A in B by A9,ORDINAL1:28;
then
A11: S.succ A in rng S & S.succ A = aleph succ A by A10,FUNCT_1:def 3;
sup rng S = sup S by ORDINAL2:26;
then
A12: aleph succ A c= sup S by A11,ORDINAL1:def 2,ORDINAL2:19;
A13: card aleph succ A = aleph succ A;
A14: aleph succ A = nextcard aleph A & aleph A in nextcard aleph A
by Th17,Lm1;
aleph B = card sup S by A8,A9,A10,Lm1;
then aleph succ A c= aleph B by A12,A13,Th10;
hence thesis by A14;
end;
A15: P[0];
A16: for B holds P[B] from ORDINAL2:sch 1(A15,A1,A7);
hence A in B implies aleph A in aleph B;
assume
A17: aleph A in aleph B;
then
A18: aleph A <> aleph B;
not B in A by A16,A17;
hence thesis by A18,ORDINAL1:14;
end;
theorem Th21:
aleph A = aleph B implies A = B
proof
assume
A1: aleph A = aleph B;
A2: now
assume B in A;
then aleph B in aleph A by Th20;
hence contradiction by A1;
end;
now
assume A in B;
then aleph A in aleph B by Th20;
hence contradiction by A1;
end;
hence thesis by A2,ORDINAL1:14;
end;
theorem
A c= B iff aleph A c= aleph B
proof
A1: aleph A c< aleph B iff aleph A <> aleph B & aleph A c= aleph B;
A in B iff aleph A in aleph B by Th20;
hence thesis by A1,Th21,ORDINAL1:11,XBOOLE_0:def 8;
end;
theorem
X c= Y & Y c= Z & X,Z are_equipotent implies X,Y are_equipotent & Y,Z
are_equipotent
proof
assume that
A1: X c= Y & Y c= Z and
A2: X,Z are_equipotent;
A3: card X = card Z by A2,Th4;
card X c= card Y & card Y c= card Z by A1,Th10;
hence thesis by A3,Th4,XBOOLE_0:def 10;
end;
theorem
bool Y c= X implies card Y in card X & not Y,X are_equipotent
proof
assume bool Y c= X;
then card bool Y c= card X by Th10;
hence card Y in card X by Th13;
then card Y <> card X;
hence thesis by Th4;
end;
theorem Th25:
X,{} are_equipotent implies X = {} by RELAT_1:42;
theorem
card {} = 0;
theorem Th27:
for x being object holds
X,{x} are_equipotent iff ex x being object st X = { x }
proof let x be object;
thus X,{x} are_equipotent implies ex x being object st X = { x }
proof
assume X,{x} are_equipotent;
then consider f such that
f is one-to-one and
A1: dom f = { x } and
A2: rng f = X by WELLORD2:def 4;
rng f = { f.x } by A1,FUNCT_1:4;
hence thesis by A2;
end;
given y being object such that
A3: X = { y };
take f = X --> x;
A4: dom f = X;
thus f is one-to-one
proof
let a,b be object;
assume that
A5: a in dom f and
A6: b in dom f and
f.a = f.b;
a = y by A3,A5,TARSKI:def 1;
hence thesis by A3,A6,TARSKI:def 1;
end;
thus dom f = X;
thus rng f c= { x } by FUNCOP_1:13;
let a be object;
assume a in { x };
then
A7: a = x by TARSKI:def 1;
A8: y in { y } by TARSKI:def 1;
then f.y = x by A3,FUNCOP_1:7;
hence thesis by A3,A4,A7,A8,FUNCT_1:def 3;
end;
theorem
for x being object holds
card X = card { x } iff ex x being object st X = { x } by Th4,Th27;
theorem Th29:
for x being object holds card { x } = 1
proof let x be object;
A1: 1 = succ 0;
1 is cardinal
proof
take IT = 1;
thus 1 = IT;
let A;
assume A,IT are_equipotent;
then ex y being object st A = { y } by A1,Th27;
hence thesis by A1,ZFMISC_1:33;
end;
then reconsider M = 1 as Cardinal;
{ x },M are_equipotent by A1,Th27;
hence thesis by Def2;
end;
theorem Th30:
X misses X1 & Y misses Y1 & X,Y are_equipotent & X1,Y1
are_equipotent implies X \/ X1,Y \/ Y1 are_equipotent
proof
assume that
A1: X /\ X1 = {} and
A2: Y /\ Y1 = {};
given f such that
A3: f is one-to-one and
A4: dom f = X and
A5: rng f = Y;
given g such that
A6: g is one-to-one and
A7: dom g = X1 and
A8: rng g = Y1;
defpred P[object,object] means $1 in X & $2 = f.$1 or $1 in X1 & $2 = g.$1;
A9: for x being object st x in X \/ X1 ex y being object st P[x,y]
proof
let x be object;
assume x in X \/ X1;
then x in X or x in X1 by XBOOLE_0:def 3;
hence thesis;
end;
A10: for x,y,z being object st x in X \/ X1 & P[x,y] & P[x,z] holds y = z
by A1,XBOOLE_0:def 4;
consider h such that
A11: dom h = X \/ X1 and
A12: for x being object st x in X \/ X1 holds P[x,h.x]
from FUNCT_1:sch 2(A10,A9);
take h;
thus h is one-to-one
proof
let x,y be object;
assume that
A13: x in dom h and
A14: y in dom h and
A15: h.x = h.y;
A16: y in X & h.y = f.y or y in X1 & h.y = g.y by A11,A12,A14;
A17: x in X & h.x = f.x or x in X1 & h.x = g.x by A11,A12,A13;
A18: now
assume
A19: y in X & x in X1;
then f.y in Y & g.x in Y1 by A4,A5,A7,A8,FUNCT_1:def 3;
hence contradiction by A1,A2,A15,A17,A16,A19,XBOOLE_0:def 4;
end;
now
assume
A20: x in X & y in X1;
then f.x in Y & g.y in Y1 by A4,A5,A7,A8,FUNCT_1:def 3;
hence contradiction by A1,A2,A15,A17,A16,A20,XBOOLE_0:def 4;
end;
hence thesis by A3,A4,A6,A7,A15,A17,A16,A18;
end;
thus dom h = X \/ X1 by A11;
thus rng h c= Y \/ Y1
proof
let x be object;
assume x in rng h;
then consider y being object such that
A21: y in dom h and
A22: x = h.y by FUNCT_1:def 3;
A23: y in X & x = f.y or y in X1 & x = g.y by A11,A12,A21,A22;
A24: now
assume y in X1;
then x in Y1 by A1,A7,A8,A23,FUNCT_1:def 3,XBOOLE_0:def 4;
hence thesis by XBOOLE_0:def 3;
end;
now
assume y in X;
then x in Y by A1,A4,A5,A23,FUNCT_1:def 3,XBOOLE_0:def 4;
hence thesis by XBOOLE_0:def 3;
end;
hence thesis by A11,A21,A24,XBOOLE_0:def 3;
end;
let x be object such that
A25: x in Y \/ Y1;
A26: now
assume x in Y1;
then consider y being object such that
A27: y in dom g and
A28: x = g.y by A8,FUNCT_1:def 3;
A29: y in X \/ X1 by A7,A27,XBOOLE_0:def 3;
then P[y,h.y] by A12;
hence thesis by A1,A7,A11,A27,A28,A29,FUNCT_1:def 3,XBOOLE_0:def 4;
end;
now
assume x in Y;
then consider y being object such that
A30: y in dom f and
A31: x = f.y by A5,FUNCT_1:def 3;
A32: y in X \/ X1 by A4,A30,XBOOLE_0:def 3;
then P[y,h.y] by A12;
hence thesis by A1,A4,A11,A30,A31,A32,FUNCT_1:def 3,XBOOLE_0:def 4;
end;
hence thesis by A25,A26,XBOOLE_0:def 3;
end;
theorem Th31:
x in X & y in X implies X \ { x },X \ { y } are_equipotent
proof
assume that
A1: x in X and
A2: y in X;
defpred P[object,object] means $1 = y & $2 = x or $1 <> y & $1 = $2;
A3: for a being object st a in X \ { x } ex b being object st P[a,b]
proof
let a be object such that
a in X \ { x };
a = y implies thesis;
hence thesis;
end;
A4: for a,b1,b2 being object st a in X \ { x } & P[a,b1] & P[a,b2]
holds b1 = b2;
consider f such that
A5: dom f = X \ { x } &
for a being object st a in X \ { x } holds P[a,f.a] from
FUNCT_1:sch 2(A4, A3);
take f;
thus f is one-to-one
proof
let b1,b2 be object;
assume that
A6: b1 in dom f & b2 in dom f and
A7: f.b1 = f.b2 & b1 <> b2;
A8: ( not b1 in { x })& not b2 in { x } by A5,A6,XBOOLE_0:def 5;
( P[b1,f.b1])& P[b2,f.b2] by A5,A6;
hence thesis by A7,A8,TARSKI:def 1;
end;
thus dom f = X \ { x } by A5;
thus rng f c= X \ { y }
proof
let z be object;
assume z in rng f;
then consider a being object such that
A9: a in dom f and
A10: z = f.a by FUNCT_1:def 3;
A11: now
assume
A12: a = y;
then ( not y in { x })& z = x by A5,A9,A10,XBOOLE_0:def 5;
then y <> z by TARSKI:def 1;
then
A13: not z in { y } by TARSKI:def 1;
z in X by A1,A5,A9,A10,A12;
hence thesis by A13,XBOOLE_0:def 5;
end;
now
assume a <> y;
then ( not a in { y })& a = z by A5,A9,A10,TARSKI:def 1;
hence thesis by A5,A9,XBOOLE_0:def 5;
end;
hence thesis by A11;
end;
let z be object;
assume
A14: z in X \ { y };
then not z in { y } by XBOOLE_0:def 5;
then
A15: z <> y by TARSKI:def 1;
A16: now
assume z <> x;
then not z in { x } by TARSKI:def 1;
then
A17: z in X \ { x } by A14,XBOOLE_0:def 5;
then z = f.z by A5,A15;
hence thesis by A5,A17,FUNCT_1:def 3;
end;
now
assume
A18: z = x;
then not y in { x } by A15,TARSKI:def 1;
then
A19: y in dom f by A2,A5,XBOOLE_0:def 5;
then z = f.y by A5,A18;
hence thesis by A19,FUNCT_1:def 3;
end;
hence thesis by A16;
end;
theorem Th32:
X c= dom f & f is one-to-one implies X,f.:X are_equipotent
proof
assume that
A1: X c= dom f and
A2: f is one-to-one;
take g = f|X;
thus g is one-to-one by A2,FUNCT_1:52;
thus dom g = X by A1,RELAT_1:62;
thus thesis by RELAT_1:115;
end;
theorem Th33:
X,Y are_equipotent & x in X & y in Y implies X \ { x },Y \ { y }
are_equipotent
proof
given f such that
A1: f is one-to-one and
A2: dom f = X and
A3: rng f = Y;
A4: X \ { x },f.:(X \ { x }) are_equipotent by A1,A2,Th32;
assume that
A5: x in X and
A6: y in Y;
f.x in Y by A2,A3,A5,FUNCT_1:def 3;
then
A7: Y \ { f.x },Y \ { y } are_equipotent by A6,Th31;
f.:(X \ { x }) = f.:X \ Im(f,x) by A1,FUNCT_1:64
.= Y \ Im(f,x) by A2,A3,RELAT_1:113
.= Y \ { f.x } by A2,A5,FUNCT_1:59;
hence thesis by A4,A7,WELLORD2:15;
end;
theorem Th34:
succ X, succ Y are_equipotent implies X, Y are_equipotent
proof
A1: X in succ X & Y in succ Y by ORDINAL1:6;
X = succ X \ {X} & Y = succ Y \ {Y} by ORDINAL1:37;
hence thesis by A1,Th33;
end;
theorem Th35:
n = {} or ex m st n = succ m
proof
defpred P[Nat] means $1 = {} or ex m st $1 = succ m;
A1: for a being Nat st P[a] holds P[succ a];
A2: P[0];
thus P[n] from ORDINAL2:sch 17(A2,A1);
end;
Lm2: n,m are_equipotent implies n = m
proof
defpred P[Nat] means for n st n,$1 are_equipotent holds n = $1;
A1: for a being Nat st P[a] holds P[succ a]
proof
let a be Nat such that
A2: P[a];
let n;
assume
A3: n,succ a are_equipotent;
per cases;
suppose
n = {};
hence thesis by A3,RELAT_1:42;
end;
suppose
n <> {};
then ex m st n = succ m by Th35;
hence thesis by A2,A3,Th34;
end;
end;
A4: P[0] by Th25;
P[m] from ORDINAL2:sch 17(A4,A1);
hence thesis;
end;
theorem Th36:
x in omega implies x is cardinal
proof
assume that
A1: x in omega and
A2: for B st x = B ex C st C,B are_equipotent & not B c= C;
reconsider A = x as Ordinal by A1;
consider B such that
A3: B,A are_equipotent and
A4: not A c= B by A2;
B in A by A4,ORDINAL1:16;
then B in omega by A1,ORDINAL1:10;
then reconsider n = A, m = B as Nat by A1;
n,m are_equipotent by A3;
hence contradiction by A4,Lm2;
end;
registration
cluster natural -> cardinal for number;
correctness by Th36;
end;
theorem Th37:
X,Y are_equipotent & X is finite implies Y is finite
proof
assume X,Y are_equipotent;
then consider f such that
f is one-to-one and
A1: dom f = X and
A2: rng f = Y;
given p being Function such that
A3: rng p = X and
A4: dom p in omega;
take f*p;
thus rng(f*p) = Y by A1,A2,A3,RELAT_1:28;
thus thesis by A1,A3,A4,RELAT_1:27;
end;
theorem Th38:
n is finite & card n is finite
proof
reconsider n as Element of omega by ORDINAL1:def 12;
rng id n = n & dom id n = n by RELAT_1:45;
hence thesis;
end;
theorem
card n = card m implies n = m;
theorem
card n c= card m iff n c= m;
theorem
card n in card m iff n in m;
Lm3:
X is finite implies ex n st X,n are_equipotent
proof
defpred P[set] means ex n st $1,n are_equipotent;
A1: P[{}];
A2: for Z,Y st Z in X & Y c= X & P[Y] holds P[Y \/ {Z}]
proof
let Z,Y such that
Z in X and
Y c= X;
given n such that
A3: Y,n are_equipotent;
A4: not Z in Y implies thesis
proof
assume
A5: not Z in Y;
now
set x = the Element of Y /\ { Z };
assume Y /\ { Z } <> {};
then x in Y & x in { Z } by XBOOLE_0:def 4;
hence contradiction by A5,TARSKI:def 1;
end;
then
A6: Y misses { Z };
A7: now
assume n meets { n };
then consider x being object such that
A8: x in n and
A9: x in { n } by XBOOLE_0:3;
A: x = n by A9,TARSKI:def 1;
reconsider xx = x as set by TARSKI:1;
not xx in xx;
hence contradiction by A8,A;
end;
take succ n;
{ Z },{ n } are_equipotent by Th27;
hence thesis by A3,A7,A6,Th30;
end;
Z in Y implies thesis
proof
assume
A10: Z in Y;
take n;
thus thesis by A3,A10,XBOOLE_1:12,ZFMISC_1:31;
end;
hence thesis by A4;
end;
assume
A11: X is finite;
thus P[X] from FINSET_1:sch 2(A11,A1,A2);
end;
::$CT
theorem Th42:
nextcard card n = card succ n
proof
reconsider sn = succ n as Nat;
for M st card card n in M holds card succ n c= M by ORDINAL1:21;
hence thesis by Def3,ORDINAL1:6;
end;
:: definition
:: let n be Nat;
:: redefine func succ n -> Element of omega;
:: coherence by ORDINAL1:def 12;
:: end;
definition
let X be finite set;
redefine func card X -> Element of omega; :: redefines card (CARD_1, definition)
coherence
proof
consider n such that
A1: X,n are_equipotent by Lm3;
reconsider n as Element of omega by ORDINAL1:def 12;
X,n are_equipotent by A1;
hence thesis by Def2;
end;
end;
theorem
X is finite implies nextcard X is finite
proof
assume X is finite;
then reconsider X as finite set;
card X = card card X;
then
A1: card(succ card X) = nextcard card X by Th42;
nextcard card X = nextcard X by Def2,Th16;
hence thesis by A1,Th38;
end;
scheme
CardinalInd { Sigma[set] }: for M holds Sigma[M]
provided
A1: Sigma[{}] and
A2: for M st Sigma[M] holds Sigma[nextcard M] and
A3: for M st M <> {} & M is limit_cardinal & for N st N in M holds Sigma
[N] holds Sigma[M]
proof
let M;
defpred P[Ordinal] means $1 is Cardinal implies Sigma[$1];
A4: for A st for B st B in A holds P[B] holds P[A]
proof
let A such that
A5: for B st B in A holds P[B] and
A6: A is Cardinal;
reconsider M = A as Cardinal by A6;
A7: now
assume not M is limit_cardinal;
then consider N such that
A8: M = nextcard N;
N in M by A8,Th17;
hence Sigma[M] by A2,A5,A8;
end;
now
assume
A9: M <> {} & M is limit_cardinal;
for N st N in M holds Sigma[N] by A5;
hence Sigma[M] by A3,A9;
end;
hence thesis by A1,A7;
end;
for A holds P[A] from ORDINAL1:sch 2(A4);
hence thesis;
end;
scheme
CardinalCompInd { Sigma[set] }: for M holds Sigma[M]
provided
A1: for M st for N st N in M holds Sigma[N] holds Sigma[M]
proof
let M;
defpred P[Ordinal] means $1 is Cardinal implies Sigma[$1];
A2: for A st for B st B in A holds P[B] holds P[A]
proof
let A such that
A3: for B st B in A holds B is Cardinal implies Sigma[B];
assume A is Cardinal;
then reconsider M = A as Cardinal;
for N st N in M holds Sigma[N] by A3;
hence thesis by A1;
end;
for A holds P[A] from ORDINAL1:sch 2(A2);
hence thesis;
end;
theorem Th44:
aleph 0 = omega
proof
thus aleph 0 c= omega by Lm1,Th7;
thus omega c= aleph 0
proof
let x be object;
assume
A1: x in omega;
then reconsider A = x as Ordinal;
consider n being Element of omega such that
A2: A = n by A1;
card succ n c= card omega by Th10,ORDINAL1:21;
hence thesis by A2,Lm1,ORDINAL1:6;
end;
end;
registration
cluster omega -> cardinal for number;
coherence by Th44;
end;
theorem
card omega = omega;
registration
cluster omega -> limit_cardinal;
coherence
proof
given N such that
A1: omega = nextcard N;
N in omega by A1,Th17;
then
A2: succ N in omega by ORDINAL1:def 12;
reconsider n=N as Element of omega by A1,Th17;
nextcard card n = card succ n & card n = n by Th42;
hence contradiction by A1,A2;
end;
end;
registration
cluster -> finite for Element of omega;
coherence by Th38;
end;
registration
cluster finite for Cardinal;
existence
proof
set n = the Element of omega;
take n;
thus thesis;
end;
end;
theorem
for M being finite Cardinal ex n st M = card n
proof
let M be finite Cardinal;
card M = M;
hence thesis;
end;
registration
let X be finite set;
cluster card X -> finite;
coherence;
end;
Lm4: A,n are_equipotent implies A = n
proof
defpred P[Nat] means for A st A,$1 are_equipotent holds A = $1;
A1: for n st P[n] holds P[succ n]
proof
let n such that
A2: P[n];
let A;
A3: n in (succ n) & (succ n) \ { n} = n by ORDINAL1:6,37;
assume
A4: A,succ n are_equipotent;
then A <> {} by RELAT_1:42;
then
A5: {} in A by ORDINAL3:8;
now
A6: succ n in omega by ORDINAL1:def 12;
assume A is limit_ordinal;
then
A7: omega c= A by A5,ORDINAL1:def 11;
card A = card (succ n) by A4,Th4;
hence contradiction by A7,Lm1,Th10,ORDINAL1:5,A6;
end;
then consider B such that
A8: A = succ B by ORDINAL1:29;
B in A & A\{B} = B by A8,ORDINAL1:6,37;
hence thesis by A2,A4,A8,A3,Th33;
end;
A9: P[0] by Th25;
P[n] from ORDINAL2:sch 17(A9,A1);
hence thesis;
end;
Lm5: A is finite iff A in omega
proof
thus A is finite implies A in omega
proof
assume A is finite;
then consider n such that
A1: A,n are_equipotent by Lm3;
A = n by A1,Lm4;
hence thesis by ORDINAL1:def 12;
end;
assume A in omega;
hence thesis;
end;
registration
cluster omega -> infinite;
coherence
proof
not omega in omega;
hence thesis by Lm5;
end;
end;
registration
cluster infinite for set;
existence
proof
take omega;
thus thesis;
end;
end;
registration
let X be infinite set;
cluster card X -> infinite;
coherence
proof
X,card X are_equipotent by Def2;
hence thesis by Th37;
end;
end;
begin :: The meaning of numerals, 2006.08.25
theorem Th47:
1 = { 0 }
proof
thus 1 = succ 0
.= { 0 };
end;
theorem Th48:
2 = { 0,1 }
proof
thus 2 = succ 1
.= { 0,1 } by Th47,ENUMSET1:1;
end;
theorem Th49:
3 = { 0,1,2 }
proof
thus 3 = succ 2
.= { 0,1,2 } by Th48,ENUMSET1:3;
end;
theorem Th50:
4 = { 0,1,2,3 }
proof
thus 4 = succ 3
.= { 0,1,2,3 } by Th49,ENUMSET1:6;
end;
theorem Th51:
5 = { 0,1,2,3,4 }
proof
thus 5 = succ 4
.= { 0,1,2,3,4 } by Th50,ENUMSET1:10;
end;
theorem Th52:
6 = { 0,1,2,3,4,5 }
proof
thus 6 = succ 5
.= { 0,1,2,3,4,5 } by Th51,ENUMSET1:15;
end;
theorem Th53:
7 = { 0,1,2,3,4,5,6 }
proof
thus 7 = succ 6
.= { 0,1,2,3,4,5,6 } by Th52,ENUMSET1:21;
end;
theorem Th54:
8 = { 0,1,2,3,4,5,6,7 }
proof
thus 8 = succ 7
.= { 0,1,2,3,4,5,6,7 } by Th53,ENUMSET1:28;
end;
theorem Th55:
9 = { 0,1,2,3,4,5,6,7,8 }
proof
thus 9 = succ 8
.= { 0,1,2,3,4,5,6,7,8 } by Th54,ENUMSET1:84;
end;
theorem
10 = { 0,1,2,3,4,5,6,7,8,9 }
proof
thus 10 = succ 9
.= { 0,1,2,3,4,5,6,7,8,9 } by Th55,ENUMSET1:85;
end;
:: Moved from FRECHET2 by AK on 27.12.2006
theorem
for f being Function
st dom f is infinite & f is one-to-one holds rng f is infinite
proof
let f be Function;
assume
A1: dom f is infinite;
assume f is one-to-one;
then dom f,rng f are_equipotent;
hence thesis by A1,Th37;
end;
:: from ALGSEQ_1, 2007.03.18, A.T.
reserve k,n,m for Nat;
registration
cluster non zero natural for object;
existence
proof
take 1;
thus thesis;
end;
cluster non zero for Nat;
existence
proof
take 1;
thus thesis;
end;
end;
registration let n be non zero natural Number;
cluster Segm n -> non empty;
coherence
proof
n <> 0;
hence thesis;
end;
end;
reserve l for Element of omega;
definition
let n be natural Number;
redefine func Segm n -> Subset of omega; :: redefines Segm (ORDINAL1, definition)
coherence
proof
reconsider n as Nat by TARSKI:1;
n in omega by ORDINAL1:def 12;
hence thesis by ORDINAL1:16;
end;
end;
:: from CARD_4, 2007.08.16, A.T.
theorem
A,n are_equipotent implies A = n by Lm4;
theorem
A is finite iff A in omega by Lm5;
registration
cluster natural -> finite for set;
coherence;
end;
:: from CARD_4, CARD_5 etc. 2008.02.21, A.T.
registration
let A be infinite set;
cluster bool A -> infinite;
coherence
proof
defpred P[object] means ex y being object st $1={y};
consider X being set such that
A1: for x being object holds x in X iff x in bool A & P[x]
from XBOOLE_0:sch 1;
for x being object holds x in union X iff x in A
proof
let x be object;
thus x in union X implies x in A
proof
assume x in union X;
then consider B being set such that
A2: x in B and
A3: B in X by TARSKI:def 4;
B in bool A by A1,A3;
hence thesis by A2;
end;
assume x in A;
then {x} c= A by ZFMISC_1:31;
then
A4: {x} in X by A1;
x in {x} by TARSKI:def 1;
hence thesis by A4,TARSKI:def 4;
end;
then
A5: union X = A by TARSKI:2;
A6: for B being set st B in X holds B is finite
proof
let B be set;
assume B in X;
then ex y being object st B = {y} by A1;
hence thesis;
end;
A7: X c= bool A
by A1;
assume bool A is finite;
hence thesis by A5,A6,A7,FINSET_1:7;
end;
let B be non empty set;
cluster [:A,B:] ->infinite;
coherence
proof
deffunc F(object) = $1`1;
consider f such that
A8: dom f = [:A,B:] and
A9: for x being object st x in [:A,B:] holds f.x = F(x) from FUNCT_1:sch 3;
for x being object holds x in rng f iff x in A
proof let x be object;
thus x in rng f implies x in A
proof
assume x in rng f;
then consider y being object such that
A10: y in dom f and
A11: f.y = x by FUNCT_1:def 3;
x = y`1 by A8,A9,A10,A11;
hence thesis by A8,A10,MCART_1:10;
end;
set y = the Element of B;
assume
A12: x in A;
then
A13: [x,y] in dom f by A8,ZFMISC_1:87;
f.([x,y]) = [x,y]`1 by A9,A12,ZFMISC_1:87
.= x;
hence thesis by A13,FUNCT_1:def 3;
end;
then rng f = A by TARSKI:2;
then
A14: f.:[:A,B:] = A by A8,RELAT_1:113;
assume [:A,B:] is finite;
hence contradiction by A14;
end;
cluster [:B,A:] ->infinite;
coherence
proof
deffunc F(object) = $1`2;
consider f such that
A15: dom f = [:B,A:] and
A16: for x being object st x in [:B,A:] holds f.x = F(x) from FUNCT_1:sch 3;
for y being object holds y in rng f iff y in A
proof let y be object;
thus y in rng f implies y in A
proof
assume y in rng f;
then consider x being object such that
A17: x in dom f and
A18: f.x = y by FUNCT_1:def 3;
y = x`2 by A15,A16,A17,A18;
hence thesis by A15,A17,MCART_1:10;
end;
set x = the Element of B;
assume
A19: y in A;
then
A20: [x,y] in dom f by A15,ZFMISC_1:87;
[x,y]`2 = y;
then f.([x,y]) = y by A16,A19,ZFMISC_1:87;
hence thesis by A20,FUNCT_1:def 3;
end;
then rng f = A by TARSKI:2;
then
A21: f.:[:B,A:] = A by A15,RELAT_1:113;
assume [:B,A:] is finite;
hence contradiction by A21;
end;
end;
registration
let X be infinite set;
cluster infinite for Subset of X;
existence
proof
X c= X;
hence thesis;
end;
end;
:: from NECKLA_2, 2008.06.28, A.T.
registration
cluster finite ordinal -> natural for number;
coherence
by Lm5;
end;
theorem Th60:
for f being Function holds card f = card dom f
proof
let f be Function;
dom f,f are_equipotent
proof
deffunc F(object) = [$1,f.$1];
consider g being Function such that
A1: dom g = dom f and
A2: for x being object st x in dom f holds g.x = F(x) from FUNCT_1:sch 3;
take g;
thus g is one-to-one
proof
let x,y be object;
assume that
A3: x in dom g and
A4: y in dom g;
assume g.x = g.y;
then [x,f.x] = g.y by A1,A2,A3
.= [y,f.y] by A1,A2,A4;
hence thesis by XTUPLE_0:1;
end;
thus dom g = dom f by A1;
thus rng g c= f
proof
let i be object;
assume i in rng g;
then consider x being object such that
A5: x in dom g and
A6: g.x = i by FUNCT_1:def 3;
g.x = [x,f.x] by A1,A2,A5;
hence thesis by A1,A5,A6,FUNCT_1:1;
end;
let x,y be object;
assume
A7: [x,y] in f;
then
A8: x in dom f by FUNCT_1:1;
y = f.x by A7,FUNCT_1:1;
then g.x = [x,y] by A2,A7,FUNCT_1:1;
hence thesis by A1,A8,FUNCT_1:def 3;
end;
hence thesis by Th4;
end;
registration
let X be finite set;
cluster RelIncl X -> finite;
coherence
proof
RelIncl X c= [:X,X:] by WELLORD2:23;
hence thesis;
end;
end;
:: from AMISTD_2, 2010.01.10, A.T
theorem
RelIncl X is finite implies X is finite
proof
set R = RelIncl X;
assume R is finite;
then reconsider A = R as finite Relation;
field A is finite;
hence thesis by WELLORD2:def 1;
end;
theorem
card(k -->x) = k
proof
dom(k -->x) = k;
hence card(k -->x) = card k by Th60
.= k;
end;
begin :: n-element set, 2010.11.17, A.T.
definition
::$CD
let N be object, X be set;
attr X is N-element means
:Def6: card X = N;
end;
registration let N be Cardinal;
cluster N-element for set;
existence
proof
take N;
thus card N = N;
end;
end;
registration
cluster 0-element -> empty for set;
coherence;
cluster empty -> 0-element for set;
coherence;
end;
registration let x be object;
cluster {x} -> 1-element;
coherence
proof
1 = succ 0;
hence card { x } = 1 by Def2,Th27;
end;
end;
registration let N be Cardinal;
cluster N-element for Function;
existence
proof
take f = N --> {{}};
card dom f = N;
hence card f = N by Th60;
end;
end;
registration let N be Cardinal; let f be N-element Function;
cluster dom f -> N-element;
coherence
proof
card f = N by Def6;
hence card dom f = N by Th60;
end;
end;
registration
cluster 1-element -> trivial non empty for set;
coherence
proof let X be set;
assume X is 1-element;
then card X = 1
.= card {0} by Th29;
then ex x being object st X = {x} by Th4,Th27;
hence thesis;
end;
cluster trivial non empty -> 1-element for set;
coherence
proof let X be set;
assume X is trivial non empty;
then ex x being object st X = {x} by ZFMISC_1:131;
hence thesis;
end;
end;
registration let X be non empty set;
cluster 1-element for Subset of X;
existence
proof
take the non empty trivial Subset of X;
thus thesis;
end;
end;
definition let X be non empty set;
mode Singleton of X is 1-element Subset of X;
end;
theorem Th63:
for X being non empty set, A being Singleton of X
ex x being Element of X st A = {x}
proof let X be non empty set, A be Singleton of X;
consider x being object such that
A1: A = {x} by ZFMISC_1:131;
x in A by A1,TARSKI:def 1;
then reconsider x as Element of X;
take x;
thus thesis by A1;
end;
theorem Th64:
card X c= card Y iff ex f st X c= f.:Y
proof
deffunc G(object) = $1;
thus card X c= card Y implies ex f st X c= f.:Y
proof
assume card X c= card Y;
then consider f such that
A1: dom f = Y & X c= rng f by Th11;
take f;
thus thesis by A1,RELAT_1:113;
end;
given f such that
A2: X c= f.:Y;
defpred C[object] means $1 in dom f;
deffunc F(object) = f.$1;
consider g such that
A3: dom g = Y &
for x being object st x in Y holds (C[x] implies g.x = F(x)) & (not C
[x] implies g.x = G(x)) from PARTFUN1:sch 1;
X c= rng g
proof
let x be object;
assume x in X;
then consider y being object such that
A4: y in dom f and
A5: y in Y and
A6: x = f.y by A2,FUNCT_1:def 6;
x = g.y by A3,A4,A5,A6;
hence thesis by A3,A5,FUNCT_1:def 3;
end;
hence thesis by A3,Th11;
end;
theorem
card (f.:X) c= card X by Th64;
theorem
card X in card Y implies Y \ X <> {}
proof
assume that
A1: card X in card Y and
A2: Y \ X = {};
Y c= X by A2,XBOOLE_1:37;
hence contradiction by A1,Th10,ORDINAL1:5;
end;
theorem
for x being object holds
X,[:X,{x}:] are_equipotent & card X = card [:X,{x}:]
proof let x be object;
deffunc f(object) = [$1,x];
consider f such that
A1: dom f = X & for y being object st y in X holds f.y = f(y)
from FUNCT_1:sch 3;
thus X,[:X,{x}:] are_equipotent
proof
take f;
thus f is one-to-one
proof
let y,z be object;
assume that
A2: y in dom f & z in dom f and
A3: f.y = f.z;
A4: [y,x]`1 = y & [z,x]`1 = z;
f.y = [y,x] & f.z = [z,x] by A1,A2;
hence y = z by A3,A4;
end;
thus dom f = X by A1;
thus rng f c= [:X,{x}:]
proof
let y be object;
A5: x in {x} by TARSKI:def 1;
assume y in rng f;
then consider z being object such that
A6: z in dom f and
A7: y = f.z by FUNCT_1:def 3;
y = [z,x] by A1,A6,A7;
hence thesis by A1,A6,A5,ZFMISC_1:87;
end;
let y be object;
assume y in [:X,{x}:];
then consider y1,y2 being object such that
A8: y1 in X and
A9: y2 in {x} and
A10: y = [y1,y2] by ZFMISC_1:84;
y2 = x by A9,TARSKI:def 1;
then y = f.y1 by A1,A8,A10;
hence thesis by A1,A8,FUNCT_1:def 3;
end;
hence thesis by Th4;
end;
:: from POLYFORM, 2011.07.25, A.T.
theorem
for f being Function st f is one-to-one holds card dom f = card rng f
proof
let f be Function;
assume
A1: f is one-to-one;
f .: dom f = rng f by RELAT_1:113;
hence thesis by A1,Th4,Th32;
end;
registration
let F be non trivial set;
let A be Singleton of F;
cluster F\A -> non empty;
coherence
proof
ex x being Element of F st A = {x} by Th63;
hence thesis by ZFMISC_1:139;
end;
end;
registration let k be non empty Cardinal;
cluster k-element -> non empty for set;
coherence;
end;
registration let k be natural Number;
cluster Segm k -> finite;
coherence;
end;
theorem
for f being Function, x,y being object
holds card(f+~(x,y)) = card f
proof let f be Function,x,y be object;
thus card(f+~(x,y)) = card dom(f+~(x,y)) by Th60
.= card dom f by FUNCT_4:99
.= card f by Th60;
end;
registration let n be non zero natural Number;
cluster Segm n -> with_zero;
coherence by ORDINAL3:8;
end;
registration
let c be Cardinal;
cluster cardinal for Subset of c;
existence
proof
take {};
thus thesis by XBOOLE_1:2;
end;
end;