:: Cardinal Arithmetics
:: by Grzegorz Bancerek
::
:: Received March 6, 1990
:: Copyright (c) 1990-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies ORDINAL1, CARD_1, FUNCT_1, TARSKI, RELAT_1, XBOOLE_0, ZFMISC_1,
MCART_1, FUNCT_2, ORDINAL2, ORDINAL3, FUNCOP_1, SUBSET_1, NUMBERS,
ARYTM_3, FINSET_1, XXREAL_0, ARYTM_1, NAT_1, CARD_2, CARD_3, CLASSES1,
FINSUB_1;
notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, XTUPLE_0, RELAT_1, ORDINAL1,
MCART_1, ORDINAL2, ORDINAL3, WELLORD2, CLASSES1, CARD_1, NUMBERS,
FUNCT_1, RELSET_1, FUNCT_2, XCMPLX_0, FINSET_1, FINSUB_1, FUNCOP_1,
SUBSET_1, XXREAL_0, CARD_3;
constructors ENUMSET1, WELLORD2, FUNCOP_1, ORDINAL3, XXREAL_0, XREAL_0, NAT_1,
CARD_1, CARD_3, CLASSES1, SETFAM_1, FINSUB_1, FUNCT_4, RELSET_1,
DOMAIN_1, XTUPLE_0, NUMBERS;
registrations SUBSET_1, ORDINAL1, FINSET_1, XREAL_0, CARD_1, FUNCT_2,
ZFMISC_1, XBOOLE_0, RELAT_1, CARD_3, FUNCT_1, FINSUB_1, RELSET_1,
XTUPLE_0, NAT_1;
requirements NUMERALS, SUBSET, BOOLE, ARITHM, REAL;
definitions TARSKI, FUNCT_1, WELLORD2, XBOOLE_0, CARD_3, ORDINAL1;
equalities TARSKI, XBOOLE_0, CARD_3, ORDINAL1;
expansions TARSKI, FUNCT_1, XBOOLE_0;
theorems TARSKI, ENUMSET1, FUNCT_1, FUNCT_2, MCART_1, ORDINAL1, ORDINAL2,
WELLORD2, ORDINAL3, CARD_1, NAT_1, ZFMISC_1, FUNCT_5, RELAT_1, XBOOLE_0,
XBOOLE_1, XREAL_1, XXREAL_0, CARD_3, CLASSES1, FUNCOP_1, FUNCT_6,
FRAENKEL, FINSET_1, XTUPLE_0;
schemes NAT_1, FUNCT_1, FINSET_1, CLASSES1, ORDINAL2;
begin
reserve A,B for Ordinal,
K,M,N for Cardinal,
x,x1,x2,y,y1,y2,z,u for object,X,Y,Z,X1,X2, Y1,Y2 for set,
f,g for Function;
theorem
x in X & X,Y are_equipotent implies Y <> {} &
ex x st x in Y
proof
assume
A1: x in X;
given f such that
f is one-to-one and
A2: dom f = X & rng f = Y;
f.x in Y by A1,A2,FUNCT_1:def 3;
hence Y <> {};
take f.x;
thus thesis by A1,A2,FUNCT_1:def 3;
end;
theorem
bool X,bool card X are_equipotent & card bool X = card bool card X
proof
consider f such that
A1: f is one-to-one and
A2: dom f = X and
A3: rng f = card X by CARD_1:def 2,WELLORD2:def 4;
deffunc g(set) = f.:$1;
consider g such that
A4: dom g = bool X &
for x being set st x in bool X holds g.x = g(x) from FUNCT_1:sch 5;
thus bool X,bool card X are_equipotent
proof
take g;
thus g is one-to-one
proof
let x,y be object;
assume that
A5: x in dom g and
A6: y in dom g and
A7: g.x = g.y;
reconsider xx=x, yy=y as set by TARSKI:1;
A8: g.x = f.:xx & g.y = f.:yy by A4,A5,A6;
A9: yy c= xx
proof
let z be object;
assume
A10: z in yy;
then f.z in f.:yy by A2,A4,A6,FUNCT_1:def 6;
then ex u being object st u in dom f & u in xx & f.z = f.u
by A7,A8,FUNCT_1:def 6;
hence thesis by A1,A2,A4,A6,A10;
end;
xx c= yy
proof
let z be object;
assume
A11: z in xx;
then f.z in f.:xx by A2,A4,A5,FUNCT_1:def 6;
then ex u being object st u in dom f & u in yy & f.z = f.u
by A7,A8,FUNCT_1:def 6;
hence thesis by A1,A2,A4,A5,A11;
end;
hence thesis by A9,XBOOLE_0:def 10;
end;
thus dom g = bool X by A4;
thus rng g c= bool card X
proof
let x be object;
assume x in rng g;
then consider y being object such that
A12: y in dom g and
A13: x = g.y by FUNCT_1:def 3;
reconsider y as set by TARSKI:1;
A14: f.:y c= rng f by RELAT_1:111;
g.y = f.:y by A4,A12;
hence thesis by A3,A13,A14;
end;
let x be object;
reconsider xx=x as set by TARSKI:1;
A15: f"xx c= dom f by RELAT_1:132;
assume x in bool card X;
then f.:(f"xx) = x by A3,FUNCT_1:77;
then g.(f"xx) = x by A2,A4,A15;
hence thesis by A2,A4,A15,FUNCT_1:def 3;
end;
hence thesis by CARD_1:5;
end;
deffunc g(object) = $1`1;
theorem
Z in Funcs(X,Y) implies Z,X are_equipotent & card Z = card X
proof
assume Z in Funcs(X,Y);
then consider f such that
A1: Z = f and
A2: dom f = X and
rng f c= Y by FUNCT_2:def 2;
thus Z,X are_equipotent
proof
consider g such that
A3: dom g = Z &
for x being object st x in Z holds g.x = g(x) from FUNCT_1:sch 3;
take g;
thus g is one-to-one
proof
let x,y be object;
assume that
A4: x in dom g and
A5: y in dom g;
A6: g.x = x`1 & g.y = y`1 by A3,A4,A5;
ex x1,x2 being object st [x1,x2] = y by A1,A3,A5,RELAT_1:def 1;
then
A7: y = [y`1,y`2];
ex x1,x2 being object st [x1,x2] = x by A1,A3,A4,RELAT_1:def 1;
then
A8: x = [x`1,x`2];
then x`2 = f.(x`1) by A1,A3,A4,FUNCT_1:1;
hence thesis by A1,A3,A5,A8,A7,A6,FUNCT_1:1;
end;
thus dom g = Z by A3;
thus rng g c= X
proof
let x be object;
assume x in rng g;
then consider y being object such that
A9: y in dom g and
A10: x = g.y by FUNCT_1:def 3;
ex x1,x2 being object st [x1,x2] = y by A1,A3,A9,RELAT_1:def 1;
then
A11: y = [y`1,y`2];
x = y`1 by A3,A9,A10;
hence thesis by A1,A2,A3,A9,A11,FUNCT_1:1;
end;
let x be object;
assume x in X;
then
A12: [x,f.x] in Z by A1,A2,FUNCT_1:def 2;
then g.[x,f.x] = [x,f.x]`1 by A3
.= x;
hence thesis by A3,A12,FUNCT_1:def 3;
end;
hence thesis by CARD_1:5;
end;
Lm1: x1 <> x2 implies A+^B,[:A,{x1}:] \/ [:B,{x2}:] are_equipotent & card(A+^B
) = card([:A,{x1}:] \/ [:B,{x2}:])
proof
defpred C[set] means $1 in A;
deffunc F(set) = [$1,x1];
deffunc G(Ordinal) = [$1-^A,x2];
consider f such that
A1: dom f = A+^B and
A2: for x being Ordinal holds x in A+^B implies (C[x] implies f.x = F(x)
) & (not C[x] implies f.x = G(x)) from FINSET_1:sch 1;
assume
A3: x1 <> x2;
thus A+^B,[:A,{x1}:] \/ [:B,{x2}:] are_equipotent
proof
take f;
thus f is one-to-one
proof
let x,y be object;
assume that
A4: x in dom f & y in dom f and
A5: f.x = f.y;
reconsider C1 = x, C2 = y as Ordinal by A1,A4;
per cases;
suppose
A6: x in A & y in A;
A7: [x,x1]`1 = C1 &[y,x1]`1 = C2;
f.C1 = [x,x1] & f.C2 = [y,x1] by A1,A2,A4,A6;
hence thesis by A5,A7;
end;
suppose
A8: not x in A & not y in A;
A9: [C1-^A,x2]`1 = C1-^A & [C2-^A,x2]`1 = C2-^A;
f.x = [C1-^A,x2] & f.y = [C2-^A,x2] by A1,A2,A4,A8;
then
A10: C1-^A = C2-^A by A5,A9;
A c= C1 by A8,ORDINAL1:16;
then
A11: C1 = A+^(C1-^A) by ORDINAL3:def 5;
A c= C2 by A8,ORDINAL1:16;
hence thesis by A10,A11,ORDINAL3:def 5;
end;
suppose
A12: x in A & not y in A;
A13: [x,x1]`2 = x1 & [C2-^A,x2]`2 = x2;
f.x = [x,x1] & f.y = [C2-^A,x2] by A1,A2,A4,A12;
hence thesis by A3,A5,A13;
end;
suppose
A14: not x in A & y in A;
A15: [y,x1]`2 = x1 & [C1-^A,x2]`2 = x2;
f.y = [y,x1] & f.x = [C1-^A,x2] by A1,A2,A4,A14;
hence thesis by A3,A5,A15;
end;
end;
thus dom f = A+^B by A1;
thus rng f c= [:A,{x1}:] \/ [:B,{x2}:]
proof
let x be object;
A16: x1 in {x1} by TARSKI:def 1;
A17: x2 in {x2} by TARSKI:def 1;
assume x in rng f;
then consider y being object such that
A18: y in dom f and
A19: x = f.y by FUNCT_1:def 3;
reconsider C = y as Ordinal by A1,A18;
per cases;
suppose
y in A;
then x = [C,x1] & [C,x1] in [:A,{x1}:] by A1,A2,A18,A19,A16,ZFMISC_1:87
;
hence thesis by XBOOLE_0:def 3;
end;
suppose
A20: not y in A;
then A c= C by ORDINAL1:16;
then A+^(C-^A) = C by ORDINAL3:def 5;
then C-^A in B by A1,A18,ORDINAL3:22;
then
A21: [C-^A,x2] in [:B,{x2}:] by A17,ZFMISC_1:87;
x = [C-^A,x2] by A1,A2,A18,A19,A20;
hence thesis by A21,XBOOLE_0:def 3;
end;
end;
let x be object such that
A22: x in [:A,{x1}:] \/ [:B,{x2}:];
A23: now
assume x in [:B,{x2}:];
then consider y,z being object such that
A24: y in B and
A25: z in {x2} and
A26: x = [y,z] by ZFMISC_1:84;
reconsider y as Ordinal by A24;
A27: A+^y in A+^B by A24,ORDINAL2:32;
A28: not A+^y in A by ORDINAL1:5,ORDINAL3:24;
A+^y-^A = y & z = x2 by A25,ORDINAL3:52,TARSKI:def 1;
then x = f.(A+^y) by A2,A26,A27,A28;
hence thesis by A1,A27,FUNCT_1:def 3;
end;
now
assume x in [:A,{x1}:];
then consider y,z being object such that
A29: y in A and
A30: z in {x1} and
A31: x = [y,z] by ZFMISC_1:84;
A32: A c= A+^B by ORDINAL3:24;
z = x1 by A30,TARSKI:def 1;
then x = f.y by A2,A29,A31,A32;
hence thesis by A1,A29,A32,FUNCT_1:def 3;
end;
hence thesis by A22,A23,XBOOLE_0:def 3;
end;
hence thesis by CARD_1:5;
end;
deffunc plus(set,set) = [:$1,{0}:] \/ [:$2,{1}:];
Lm2: [:X,Y:],[:Y,X:] are_equipotent & card [:X,Y:] = card [:Y,X:]
proof
deffunc f(object) = [$1`2,$1`1];
consider f such that
A1: dom f = [:X,Y:] &
for x being object st x in [:X,Y:] holds f.x = f(x) from
FUNCT_1:sch 3;
thus [:X,Y:],[:Y,X:] are_equipotent
proof
take f;
thus f is one-to-one
proof
let x,y be object;
assume
A2: x in dom f & y in dom f;
then
A3: x = [x`1,x`2] & y = [y`1,y`2] by A1,MCART_1:21;
assume
A4: f.x = f.y;
A5: f.x = [x`2,x`1] & f.y = [y`2,y `1] by A1,A2;
then x`1 = y`1 by A4,XTUPLE_0:1;
hence thesis by A3,A5,A4,XTUPLE_0:1;
end;
thus dom f = [:X,Y:] by A1;
thus rng f c= [:Y,X:]
proof
let x be object;
assume x in rng f;
then consider y being object such that
A6: y in dom f and
A7: x = f.y by FUNCT_1:def 3;
A8: y`2 in Y by A1,A6,MCART_1:10;
x = [y`2,y`1] & y`1 in X by A1,A6,A7,MCART_1:10;
hence thesis by A8,ZFMISC_1:87;
end;
let x be object;
A9: [x`2,x`1]`1 = x`2 & [x`2,x`1]`2 = x`1;
assume
A10: x in [:Y,X:];
then
A11: x = [x`1,x`2] by MCART_1:21;
A12: x`1 in Y & x`2 in X by A10,MCART_1:10;
then
[x`2,x`1] in [:X,Y:] by ZFMISC_1:87;
then f.[x`2,x`1] in rng f by A1,FUNCT_1:def 3;
hence thesis by A1,A11,A12,A9,ZFMISC_1:87;
end;
hence thesis by CARD_1:5;
end;
definition
let M,N;
func M +` N -> Cardinal equals
card( M +^ N);
coherence;
commutativity
proof
let C be Cardinal;
let M,N;
assume C = card( M +^ N);
hence C = card plus( N, M) by Lm1
.= card( N +^ M) by Lm1;
end;
func M *` N -> Cardinal equals
card [:M,N:];
coherence;
commutativity by Lm2;
func exp(M,N) -> Cardinal equals
card Funcs(N,M);
coherence;
end;
theorem Th4:
[:X,Y:],[:Y,X:] are_equipotent & card [:X,Y:] = card [:Y,X:] by Lm2;
theorem Th5:
[:[:X,Y:],Z:],[:X,[:Y,Z:]:] are_equipotent & card [:[:X,Y:],Z:]
= card [:X,[:Y,Z:]:]
proof
deffunc f(object) = [$1`1`1,[$1`1`2,$1`2]];
consider f such that
A1: dom f = [:[:X,Y:],Z:] &
for x being object st x in [:[:X,Y:],Z:] holds f.x = f(x)
from FUNCT_1:sch 3;
thus [:[:X,Y:],Z:],[:X,[:Y,Z:]:] are_equipotent
proof
take f;
thus f is one-to-one
proof
let x,y be object;
assume that
A2: x in dom f and
A3: y in dom f;
assume
A4: f.x = f.y;
A5: x = [x`1,x`2] & y = [y`1,y`2] by A1,A2,A3,MCART_1:21;
x`1 in [:X,Y:] by A1,A2,MCART_1:10;
then
A6: x`1 = [x`1`1,x`1`2 ] by MCART_1:21;
A7: f.x = [x`1`1,[x`1`2,x`2]] & f.y = [y`1`1,[y`1`2,y`2]] by A1,A2,A3;
then
A8: x`1`1 = y`1`1 by A4,XTUPLE_0:1;
y`1 in [:X,Y :] by A1,A3,MCART_1:10;
then
A9: y`1 = [y`1`1,y`1`2] by MCART_1:21;
A10: [x`1`2,x`2] = [y`1`2,y`2] by A7,A4,XTUPLE_0:1;
then x`1`2 = y`1`2 by XTUPLE_0:1;
hence thesis by A5,A8,A10,A6,A9,XTUPLE_0:1;
end;
thus dom f = [:[:X,Y:],Z:] by A1;
thus rng f c= [:X,[:Y,Z:]:]
proof
let x be object;
assume x in rng f;
then consider y being object such that
A11: y in dom f and
A12: x = f.y by FUNCT_1:def 3;
A13: y`1 in [:X,Y:] by A1,A11,MCART_1:10;
then
A14: y`1`2 in Y by MCART_1:10;
y`2 in Z by A1,A11,MCART_1:10;
then
A15: [y`1`2,y`2] in [:Y,Z:] by A14,ZFMISC_1:87;
A16: y`1`1 in X by A13,MCART_1:10;
x = [y`1`1,[y`1`2,y`2]] by A1,A11,A12;
hence thesis by A16,A15,ZFMISC_1:87;
end;
let x be object;
A17: [x`1,x`2`1]`1 = x`1 & [x`1,x`2`1]`2 = x`2 `1;
A18: [[x`1,x`2`1],x`2`2]`1 = [x`1,x`2`1] & [[x`1,x`2`1],x`2`2]`2 = x`2`2;
assume
A19: x in [:X,[:Y,Z:]:];
then
A20: x`2 in [:Y,Z:] by MCART_1:10;
then
A21: x`2`1 in Y by MCART_1:10;
A22: x`2`2 in Z by A20,MCART_1:10;
x`1 in X by A19,MCART_1:10;
then
A23: [x`1,x`2`1] in [:X,Y:] by A21,ZFMISC_1:87;
then
A24: [[x`1,x`2`1],x`2`2] in [:[:X,Y:],Z:] by A22,ZFMISC_1:87;
A25: x`2 = [x`2`1,x`2`2] by A20,MCART_1:21;
x = [x`1,x`2] by A19,MCART_1:21;
then x = f.[[x`1,x`2`1],x`2`2] by A1,A25,A17,A23,A18,A22,ZFMISC_1:87;
hence thesis by A1,A24,FUNCT_1:def 3;
end;
hence thesis by CARD_1:5;
end;
Lm3: [:X,Y:],[:card X,Y:] are_equipotent
proof
consider f such that
A1: f is one-to-one and
A2: dom f = X and
A3: rng f = card X by CARD_1:def 2,WELLORD2:def 4;
deffunc g(object) = [f.$1`1,$1`2];
consider g such that
A4: dom g = [:X,Y:] &
for x being object st x in [:X,Y:] holds g.x = g(x) from
FUNCT_1:sch 3;
take g;
thus g is one-to-one
proof
let x,y be object;
assume
A5: x in dom g & y in dom g;
then
A6: x`1 in X & y`1 in X by A4,MCART_1:10;
assume
A7: g.x = g.y;
g.x = [f.x`1,x`2] & g.y = [f.y`1,y `2] by A4,A5;
then
A8: f.x`1 = f.y`1 & x`2 = y`2 by A7,XTUPLE_0:1;
x = [x`1,x`2] & y = [y`1,y`2] by A4,A5,MCART_1:21;
hence thesis by A1,A2,A6,A8;
end;
thus dom g = [:X,Y:] by A4;
thus rng g c= [:card X,Y:]
proof
let y be object;
assume y in rng g;
then consider x being object such that
A9: x in dom g and
A10: y = g.x by FUNCT_1:def 3;
x`1 in X by A4,A9,MCART_1:10;
then
A11: f.x`1 in card X by A2,A3,FUNCT_1:def 3;
y = [f.x`1,x`2] & x`2 in Y by A4,A9,A10,MCART_1:10;
hence thesis by A11,ZFMISC_1:87;
end;
let y be object;
assume
A12: y in [:card X,Y:];
then y`1 in card X by MCART_1:10;
then consider x being object such that
A13: x in X and
A14: y`1 = f.x by A2,A3,FUNCT_1:def 3;
A15: y = [y`1,y`2] by A12,MCART_1:21;
A16: y`2 in Y by A12,MCART_1:10;
then
A17: [x,y`2] in [:X,Y:] by A13,ZFMISC_1:87;
[x,y`2]`1 = x & [x,y`2]`2 = y`2;
then g.[x,y`2] = y by A4,A15,A14,A16,A13,ZFMISC_1:87;
hence thesis by A4,A17,FUNCT_1:def 3;
end;
::$CT
theorem Th6:
[:X,Y:],[:card X,Y:] are_equipotent & [:X,Y:],[:X,card Y:]
are_equipotent & [:X,Y:],[:card X,card Y:] are_equipotent & card [:X,Y:] = card
[:card X,Y:] & card [:X,Y:] = card [:X,card Y:] & card [:X,Y:] = card [:card X,
card Y:]
proof
[:Y,X:],[:card Y,X:] are_equipotent & [:X,Y:],[:Y,X:] are_equipotent by Lm2
,Lm3;
then
A1: [:X,Y:],[:card Y,X:] are_equipotent by WELLORD2:15;
A2: [:card Y,X:],[:X,card Y:] are_equipotent by Lm2;
hence
A3: [:X,Y:],[:card X,Y:] are_equipotent & [:X,Y:],[:X,card Y:]
are_equipotent by A1,Lm3,WELLORD2:15;
[:X,card Y:],[:card X,card Y:] are_equipotent by Lm3;
hence [:X,Y:],[:card X,card Y:] are_equipotent by A3,WELLORD2:15;
hence thesis by A2,A1,Lm3,CARD_1:5,WELLORD2:15;
end;
theorem Th7:
X1,Y1 are_equipotent & X2,Y2 are_equipotent implies [:X1,X2:],[:
Y1,Y2:] are_equipotent & card [:X1,X2:] = card [:Y1,Y2:]
proof
assume X1,Y1 are_equipotent & X2,Y2 are_equipotent;
then
A1: card X1 = card Y1 & card X2 = card Y2 by CARD_1:5;
[:X1,X2:],[:card X1,card X2:] are_equipotent & [:Y1,Y2:],[:card Y1,card
Y2:] are_equipotent by Th6;
hence [:X1,X2:],[:Y1,Y2:] are_equipotent by A1,WELLORD2:15;
hence thesis by CARD_1:5;
end;
theorem
x1 <> x2 implies A+^B,[:A,{x1}:] \/ [:B,{x2}:] are_equipotent & card(A
+^B) = card([:A,{x1}:] \/ [:B,{x2}:]) by Lm1;
theorem Th9:
x1 <> x2 implies K+`M,[:K,{x1}:] \/ [:M,{x2}:] are_equipotent &
K+`M = card([:K,{x1}:] \/ [:M,{x2}:])
proof
assume x1 <> x2;
then card([:K,{x1}:] \/ [:M,{x2}:]) = K+`M by Lm1;
hence thesis by CARD_1:def 2;
end;
theorem Th10:
A*^B,[:A,B:] are_equipotent & card(A*^B) = card [:A,B:]
proof
defpred P[object,object]
means ex O1, O2 being Ordinal st O1 = $1`1 & O2 = $1`2 &
$2 = O1*^B+^O2;
A1: for x being object st x in [:A,B:] ex y being object st P[x,y]
proof
let x be object;
assume x in [:A,B:];
then x`1 in A & x`2 in B by MCART_1:10;
then reconsider x1 = x`1, x2 = x`2 as Ordinal;
take x1*^B+^x2;
take x1, x2;
thus thesis;
end;
consider f such that
A2: dom f = [:A,B:] &
for x being object st x in [:A,B:] holds P[x,f.x] from CLASSES1
:sch 1(A1);
A3: [:A,B:],A*^B are_equipotent
proof
take f;
thus f is one-to-one
proof
let x,y be object;
assume
A4: x in dom f & y in dom f;
then
A5: x`2 in B & y`2 in B by A2,MCART_1:10;
x`1 in A & y`1 in A by A2,A4,MCART_1:10;
then reconsider x1 = x`1, y1 = y`1 as Ordinal;
assume
A6: f.x = f.y;
A7: x = [x`1,x`2] & y = [y`1,y`2] by A2,A4,MCART_1:21;
A8: (ex O1, O2 being Ordinal st O1 = x`1 & O2 = x`2 & f.x = O1*^B+^O2 )
& ex O3, O4 being Ordinal st O3 = y`1 & O4 = y`2 & f.y = O3*^B+^O4 by A2,A4;
then x1 = y1 by A5,A6,ORDINAL3:48;
hence thesis by A7,A5,A8,A6,ORDINAL3:48;
end;
thus dom f = [:A,B:] by A2;
thus rng f c= A*^B
proof
let y be object;
A9: 1*^B = B by ORDINAL2:39;
assume y in rng f;
then consider x being object such that
A10: x in dom f and
A11: y = f.x by FUNCT_1:def 3;
consider x1, x2 being Ordinal such that
A12: x1 = x`1 and
A13: x2 = x`2 & f.x = x1*^B+^x2 by A2,A10;
x1+^1 = succ x1 by ORDINAL2:31;
then
A14: x1*^B+^1*^B = (succ x1)*^B by ORDINAL3:46;
succ x1 c= A by A12,A2,A10,MCART_1:10,ORDINAL1:21;
then
A15: x1*^B+^1*^B c= A*^B by A14,ORDINAL2:41;
y in x1*^B+^1*^B by A11,A13,A9,A2,A10,MCART_1:10,ORDINAL2:32;
hence thesis by A15;
end;
let y be object;
assume
A16: y in A*^B;
then reconsider C = y as Ordinal;
A17: C = (C div^ B)*^B+^(C mod^ B) & [C div^ B,C mod^ B]`1 = C div^ B by
ORDINAL3:65;
C div^ B in A & C mod^ B in B by A16,ORDINAL3:67;
then
A18: [C div^ B,C mod^ B] in [:A,B:] by ZFMISC_1:87;
then
[C div^ B,C mod^ B]`2 = C mod^ B & ex O1, O2 being Ordinal st O1 = [C
div^ B,C mod^ B]`1 & O2 = [C div^ B,C mod^ B]`2 & f.[C div^ B,C mod^ B] = O1*^B
+^ O2 by A2;
hence thesis by A2,A18,A17,FUNCT_1:def 3;
end;
hence A*^B,[:A,B:] are_equipotent;
thus thesis by A3,CARD_1:5;
end;
deffunc plus(set,set) = [:$1,{0}:] \/ [:$2,{1}:];
deffunc plus(set,set,object,object) = [:$1,{$3}:] \/ [:$2,{$4}:];
theorem Th11:
X1,Y1 are_equipotent & X2,Y2 are_equipotent & x1 <> x2 & y1 <>
y2 implies [:X1,{x1}:] \/ [:X2,{x2}:],[:Y1,{y1}:] \/ [:Y2,{y2}:] are_equipotent
& card ([:X1,{x1}:] \/ [:X2,{x2}:]) = card ([:Y1,{y1}:] \/ [:Y2,{y2}:])
proof
assume that
A1: X1,Y1 are_equipotent and
A2: X2,Y2 are_equipotent and
A3: x1 <> x2 and
A4: y1 <> y2;
{x2},{y2} are_equipotent by CARD_1:28;
then
A5: [:X2,{x2}:],[:Y2,{y2}:] are_equipotent by A2,Th7;
A6: now
assume [:Y1,{y1}:] meets [:Y2,{y2}:];
then consider y being object such that
A7: y in [:Y1,{y1}:] and
A8: y in [:Y2,{y2}:] by XBOOLE_0:3;
y`2 in {y1} by A7,MCART_1:10;
then
A9: y`2 = y1 by TARSKI:def 1;
y`2 in {y2} by A8,MCART_1:10;
hence contradiction by A4,A9,TARSKI:def 1;
end;
A10: now
assume [:X1,{x1}:] meets [:X2,{x2}:];
then consider x being object such that
A11: x in [:X1,{x1}:] and
A12: x in [:X2,{x2}:] by XBOOLE_0:3;
x`2 in {x1} by A11,MCART_1:10;
then
A13: x`2 = x1 by TARSKI:def 1;
x`2 in {x2} by A12,MCART_1:10;
hence contradiction by A3,A13,TARSKI:def 1;
end;
{x1},{y1} are_equipotent by CARD_1:28;
then [:X1,{x1}:],[:Y1,{y1}:] are_equipotent by A1,Th7;
hence [:X1,{x1}:] \/ [:X2,{x2}:],[:Y1,{y1}:] \/ [:Y2,{y2}:]
are_equipotent by A5,A10,A6,CARD_1:31;
hence thesis by CARD_1:5;
end;
theorem Th12:
card(A+^B) = card A +` card B
proof
A1: A+^B,plus(A,B) are_equipotent by Lm1;
A,card A are_equipotent & B,card B are_equipotent by CARD_1:def 2;
then
A2: plus(A,B),plus( card A, card B) are_equipotent by Th11;
plus( card A, card B),card A +^ card B are_equipotent by Lm1;
then plus(A,B),card A +^ card B are_equipotent by A2,WELLORD2:15;
then A+^B,card A +^ card B are_equipotent by A1,WELLORD2:15;
hence thesis by CARD_1:5;
end;
theorem Th13:
card(A*^B) = card A *` card B
proof
thus card (A*^B) = card [:A,B:] by Th10
.= card A *` card B by Th6;
end;
theorem
[:X,{0}:] \/ [:Y,{1}:],[:Y,{0}:] \/ [:X,{1}:] are_equipotent & card([:
X,{0}:] \/ [:Y,{1}:]) = card([:Y,{0}:] \/ [:X,{1}:]) by Th11;
theorem Th15:
[:X1,X2:] \/ [:Y1,Y2:],[:X2,X1:] \/ [:Y2,Y1:] are_equipotent &
card ([:X1,X2:] \/ [:Y1,Y2:]) = card ([:X2,X1:] \/ [:Y2,Y1:])
proof
deffunc f(object) = [$1`2,$1`1];
consider f such that
A1: dom f = [:X1,X2:] \/ [:Y1,Y2:] &
for x being object st x in [:X1,X2:] \/ [:Y1,Y2
:] holds f.x = f(x) from FUNCT_1:sch 3;
thus [:X1,X2:] \/ [:Y1,Y2:],[:X2,X1:] \/ [:Y2,Y1:] are_equipotent
proof
take f;
thus f is one-to-one
proof
let x1,x2 be object;
assume that
A2: x1 in dom f and
A3: x2 in dom f and
A4: f.x1 = f.x2;
x1 in [:X1,X2:] or x1 in [:Y1,Y2:] by A1,A2,XBOOLE_0:def 3;
then
A5: x1 = [x1`1,x1`2] by MCART_1:21;
x2 in [:X1,X2:] or x2 in [:Y1,Y2:] by A1,A3,XBOOLE_0:def 3;
then
A6: x2 = [x2`1,x2`2] by MCART_1:21;
A7: f.x1 = [x1`2,x1`1] & f.x2 = [x2`2,x2`1] by A1,A2,A3;
then x1`1 = x2`1 by A4,XTUPLE_0:1;
hence thesis by A4,A7,A5,A6,XTUPLE_0:1;
end;
thus dom f = [:X1,X2:] \/ [:Y1,Y2:] by A1;
thus rng f c= [:X2,X1:] \/ [:Y2,Y1:]
proof
let x be object;
assume x in rng f;
then consider y being object such that
A8: y in dom f and
A9: x = f.y by FUNCT_1:def 3;
y in [:X1,X2:] or y in [:Y1,Y2:] by A1,A8,XBOOLE_0:def 3;
then
A10: y`1 in X1 & y`2 in X2 or y`1 in Y1 & y`2 in Y2 by MCART_1:10;
x = [y`2,y`1] by A1,A8,A9;
then x in [:X2,X1:] or x in [:Y2,Y1:] by A10,ZFMISC_1:87;
hence thesis by XBOOLE_0:def 3;
end;
let x be object;
A11: [x`2,x`1]`1 = x`2 & [x`2,x`1]`2 = x`1;
assume x in [:X2,X1:] \/ [:Y2,Y1:];
then
A12: x in [:X2,X1:] or x in [:Y2,Y1:] by XBOOLE_0:def 3;
then x`1 in X2 & x`2 in X1 or x`1 in Y2 & x`2 in Y1 by MCART_1:10;
then [x`2,x`1] in [:X1,X2:] or [x`2,x`1] in [:Y1,Y2:] by ZFMISC_1:87;
then
A13: [x`2,x`1] in [:X1,X2:] \/ [:Y1,Y2:] by XBOOLE_0:def 3;
x = [x`1,x`2] by A12,MCART_1:21;
then f.[x`2,x`1] = x by A1,A13,A11;
hence thesis by A1,A13,FUNCT_1:def 3;
end;
hence thesis by CARD_1:5;
end;
theorem Th16:
x <> y implies card X +` card Y = card([:X,{x}:] \/ [:Y,{y}:])
proof
assume
A1: x <> y;
X,card X are_equipotent & Y,card Y are_equipotent by CARD_1:def 2;
then card plus(X,Y,x,y) = card plus(card X,card Y,x,y) by A1,Th11;
hence thesis by A1,Lm1;
end;
theorem
M+`0 = M
proof
thus M+`0 = card plus(M,{}) by Lm1
.= card M by CARD_1:69
.= M;
end;
Lm4: x <> y implies [:X,{x}:] misses [:Y,{y}:]
proof
assume
A1: x <> y;
assume not thesis;
then consider z being object such that
A2: z in [:X,{x}:] and
A3: z in [:Y,{y}:] by XBOOLE_0:3;
z`2 = x by A2,MCART_1:13;
hence contradiction by A1,A3,MCART_1:13;
end;
theorem Th18:
(K+`M)+`N = K+`(M+`N)
proof
A1: card(K+`M+`N) = K+`M+`N;
A2: K+`M+`N,[:K+`M,{0}:] \/ [:N,{2}:] are_equipotent by Th9;
[:M,{1}:] misses [:N,{2}:] by Lm4;
then
A3: [:M,{1}:] /\ [:N,{2}:] = {};
[:K,{0}:] misses [:N,{2}:] by Lm4;
then [:K,{0}:] /\ [:N,{2}:] = {};
then ([:K,{0}:] \/ [:M,{1}:]) /\ [:N,{2}:] = {} \/ {} by A3,XBOOLE_1:23
.= {};
then
A4: ([:K,{0}:] \/ [:M,{1}:]) misses [:N,{2}:];
K+`M,[:K,{0}:] \/ [:M,{1}:] are_equipotent & K+`M,[:K+`M,{0}:]
are_equipotent by CARD_1:69,Th9;
then
A5: [:K+`M,{0}:],[:K,{0}:] \/ [:M,{1}:] are_equipotent by WELLORD2:15;
[:K,{0}:] misses [:N,{2}:] by Lm4;
then
A6: [:K,{0}:] /\ [:N,{2}:] = {};
[:K,{0}:] misses [:M,{1}:] by Lm4;
then [:K,{0}:] /\ [:M,{1}:] = {};
then [:K,{0}:] /\ ([:M,{1}:] \/ [:N,{2}:]) = {} \/ {} by A6,XBOOLE_1:23
.= {};
then
A7: [:K,{0}:] misses ([:M,{1}:] \/ [:N,{2}:]);
M+`N,[:M,{1}:] \/ [:N,{2}:] are_equipotent & M+`N,[:M+`N,{2}:]
are_equipotent by CARD_1:69,Th9;
then
A8: [:M+`N,{2}:],[:M,{1}:] \/ [:N,{2}:] are_equipotent by WELLORD2:15;
[:K,{0}:] misses [:M+`N,{2}:] by Lm4;
then
A9: [:K,{0}:] \/ ([:M,{1}:] \/ [:N,{2}:]),[:K,{0}:] \/ [:M+`N,{2}:]
are_equipotent by A7,A8,CARD_1:31;
[:K+`M,{0}:] misses [:N,{2}:] by Lm4;
then
A10: [:K+`M,{0}:] \/ [:N,{2}:], [:K,{0}:] \/ [:M,{1}:] \/ [:N,{2}:]
are_equipotent by A4,A5,CARD_1:31;
[:K,{0}:] \/ ([:M,{1}:] \/ [:N,{2}:]) = [:K,{0}:] \/ [:M,{1}:] \/ [:N,{
2}:] by XBOOLE_1:4;
then [:K+`M,{0}:] \/ [:N,{2}:],[:K,{0}:] \/ [:M+`N,{2}:] are_equipotent by
A10,A9,WELLORD2:15;
then
A11: K+`M+`N,[:K,{0}:] \/ [:M+`N,{2}:] are_equipotent by A2,WELLORD2:15;
[:K,{0}:] \/ [:M+`N,{2}:],K+`(M+`N) are_equipotent by Th9;
then K+`M+`N,K+`(M+`N) are_equipotent by A11,WELLORD2:15;
hence thesis by A1,CARD_1:def 2;
end;
theorem
K*`0 = 0;
theorem Th20:
K*`1 = K
proof
K = card K;
hence thesis by CARD_1:69,ORDINAL3:15;
end;
theorem Th21:
(K*`M)*`N = K*`(M*`N)
proof
thus (K*`M)*`N = card [:[:K,M:],N:] by Th6
.= card [:K,[:M,N:]:] by Th5
.= K*`(M*`N) by Th6;
end;
theorem Th22:
2*`K = K+`K
proof
thus 2*`K = card([:{{}},K:] \/ [:{1},K:]) by CARD_1:50,ZFMISC_1:109
.= card([:K,{{}}:] \/ [:K,{1}:]) by Th15
.= card K +` card K by Th16
.= K +` card K
.= K +` K;
end;
theorem Th23:
K*`(M+`N) = K*`M +` K*`N
proof
A1: [:card [:K,M:],{0}:],[:[:K,M:],{0}:] are_equipotent by Th6;
M,[:M,{0}:] are_equipotent by CARD_1:69;
then
A2: [:K,M:],[:K,[:M,{0}:]:] are_equipotent by Th7;
[:[:K,M:],{0}:],[:K,M:] are_equipotent by CARD_1:69;
then [:[:K,M:],{0}:],[:K,[:M,{0}:]:] are_equipotent by A2,WELLORD2:15;
then
A3: [:card [:K,M:],{0}:],[:K,[:M,{0}:]:] are_equipotent by A1,WELLORD2:15;
A4: [:card [:K,N:],{1}:],[:[:K,N:],{1}:] are_equipotent by Th6;
[:M,{0}:] misses [:N,{1}:] by Lm4;
then
A5: [:K,[:M,{0}:]:] misses [:K,[:N,{1}:]:] by ZFMISC_1:104;
N,[:N,{1}:] are_equipotent by CARD_1:69;
then
A6: [:K,N:],[:K,[:N,{1}:]:] are_equipotent by Th7;
A7: K*`(M+`N) = card [:K,card plus(M,N):] by Th9
.= card [:K,plus(M,N):] by Th6
.= card ([:K,[:M,{0}:]:] \/ [:K,[:N,{1}:]:]) by ZFMISC_1:97;
[:[:K,N:],{1}:],[:K,N:] are_equipotent by CARD_1:69;
then [:[:K,N:],{1}:],[:K,[:N,{1}:]:] are_equipotent by A6,WELLORD2:15;
then
A8: [:card [:K,N:],{1}:],[:K,[:N,{1}:]:] are_equipotent by A4,WELLORD2:15;
[:card [:K,M:],{0}:] misses [:card [:K,N:],{1}:] by Lm4;
then
[:card [:K,M:],{0}:] \/ [:card [:K,N:],{1}:], [:K,[:M,{0}:]:] \/ [:K,[:
N,{1}:]:] are_equipotent by A3,A8,A5,CARD_1:31;
hence K*`(M+`N) = card([:card [:K,M:],{0}:] \/ [:card [:K,N:],{1}:]) by A7,
CARD_1:5
.= K*`M +` K*`N by Th9;
end;
theorem
exp(K,0) = 1
proof
thus exp(K,0) = card {{}} by FUNCT_5:57
.= 1 by CARD_1:30;
end;
theorem
K <> 0 implies exp(0,K) = 0;
theorem
exp(K,1) = K & exp(1,K) = 1
proof
thus exp(K,1) = card K by FUNCT_5:58,ORDINAL3:15
.= K;
thus exp(1,K)
= card {K --> {}} by FUNCT_5:59,ORDINAL3:15
.= 1 by CARD_1:30;
end;
theorem
exp(K,M+`N) = exp(K,M)*`exp(K,N)
proof
A1: [:M,{0}:] misses [:N,{1}:] by ZFMISC_1:108;
[:M,{0}:],M are_equipotent by CARD_1:69;
then
A2: Funcs([:M,{0}:],K),Funcs(M,K) are_equipotent by FUNCT_5:60;
[:N,{1}:],N are_equipotent by CARD_1:69;
then
A3: Funcs([:N,{1}:],K),Funcs(N,K) are_equipotent by FUNCT_5:60;
M+`N,[:M,{0}:] \/ [:N,{1}:] are_equipotent by Th9;
hence exp(K,M+`N) = card Funcs([:M,{0}:] \/ [:N,{1}:],K) by FUNCT_5:60
.= card [:Funcs([:M,{0}:],K),Funcs([:N,{1}:],K):] by A1,FUNCT_5:62
.= card [:Funcs(M,K),Funcs(N,K):] by A2,A3,Th7
.= exp(K,M)*`exp(K,N) by Th6;
end;
theorem
exp(K*`M,N) = exp(K,N)*`exp(M,N)
proof
card(K*`M) = K*`M & card N = card N;
hence exp(K*`M,N) = card Funcs(N,[:K,M:]) by FUNCT_5:61
.= card [:Funcs(N,K),Funcs(N,M):] by FUNCT_5:64
.= exp(K,N)*`exp(M,N) by Th6;
end;
theorem
exp(K,M*`N) = exp(exp(K,M),N)
proof
A1: Funcs(M,K),card Funcs(M,K) are_equipotent by CARD_1:def 2;
[:M,N:],M*`N are_equipotent & [:N,M:],[:M,N:] are_equipotent by Lm2,
CARD_1:def 2;
then [:N,M:],M*`N are_equipotent by WELLORD2:15;
hence exp(K,M*`N) = card Funcs([:N,M:],K) by FUNCT_5:60
.= card Funcs(N,Funcs(M,K)) by FUNCT_5:63
.= exp(exp(K,M),N) by A1,FUNCT_5:60;
end;
::$N The Number of Subsets of a Set
::$L https://en.wikipedia.org/wiki/Subset The Number of Subsets of a Set
theorem
exp(2,card X) = card bool X
proof
card card X = card X & card 2 = card {{},1} by CARD_1:50;
hence exp(2,card X) = card Funcs(X,{{},1}) by FUNCT_5:61
.= card bool X by FUNCT_5:65;
end;
theorem
exp(K,2) = K*`K by CARD_1:50,FUNCT_5:66;
theorem
exp(K+`M,2) = K*`K +` 2*`K*`M +` M*`M
proof
thus exp(K+`M,2) = (K+`M)*`(K+`M) by CARD_1:50,FUNCT_5:66
.= K*`(K+`M) +` M*`(K+`M) by Th23
.= K*`K +` K*`M +` M*`(K+`M) by Th23
.= K*`K +` K*`M +` (M*`K +` M*`M) by Th23
.= K*`K +` K*`M +` K*`M +` M*`M by Th18
.= K*`K +` (K*`M +` K*`M) +` M*`M by Th18
.= K*`K +` 2*`(K*`M) +` M*`M by Th22
.= K*`K +` 2*`K*`M +` M*`M by Th21;
end;
theorem Th33:
card(X \/ Y) c= card X +` card Y
proof
consider f such that
A1: dom f = plus(X,Y) &
for x being object st x in plus(X,Y) holds f.x = g(x) from
FUNCT_1:sch 3;
X \/ Y c= rng f
proof
let x be object;
assume x in X \/ Y;
then
A2: x in X or x in Y by XBOOLE_0:def 3;
per cases;
suppose
x in X;
then [x,0] in [:X,{0}:] by ZFMISC_1:106;
then
A3: [x,0] in plus(X,Y) by XBOOLE_0:def 3;
[x,0]`1 = x;
then x = f.[x,0] by A1,A3;
hence thesis by A1,A3,FUNCT_1:def 3;
end;
suppose
not x in X;
then [x,1] in [:Y,{1}:] by A2,ZFMISC_1:106;
then
A4: [x,1] in plus(X,Y) by XBOOLE_0:def 3;
[x,1]`1 = x;
then x = f.[x,1] by A1,A4;
hence thesis by A1,A4,FUNCT_1:def 3;
end;
end;
then card(X \/ Y) c= card plus(X,Y) by A1,CARD_1:12;
hence thesis by Th16;
end;
theorem Th34:
X misses Y implies card (X \/ Y) = card X +` card Y
proof
assume
A1: X misses Y;
X,[:X,{0}:] are_equipotent & [:X,{0}:],[:card X,{0}:] are_equipotent
by CARD_1:69
,Th6;
then
A2: X,[:card X,{0}:] are_equipotent by WELLORD2:15;
Y,[:Y,{1}:] are_equipotent & [:Y,{1}:],[:card Y,{1}:] are_equipotent
by CARD_1:69,Th6;
then
A3: Y,[:card Y,{1}:] are_equipotent by WELLORD2:15;
[:card X,{0}:] misses [:card Y,{1}:] by Lm4;
then X \/ Y,[:card X,{0}:] \/ [:card Y,{1}:] are_equipotent by A1,A2,A3,
CARD_1:31;
hence card (X \/ Y) = card ([:card X,{0}:] \/ [:card Y,{1}:]) by CARD_1:5
.= card X +` card Y by Th9;
end;
reserve m,n for Nat;
theorem Th35:
n+m = n +^ m
proof
defpred P[Nat] means n+$1 = n +^ $1;
A1: for m st P[m] holds P[m+1]
proof
let m such that
A2: P[m];
thus n+(m+1) = Segm(n+m+1)
.= succ Segm(n + m) by NAT_1:38
.= succ(n +^ m) by A2
.= n +^ succ Segm m by ORDINAL2:28
.= n +^ Segm (m+1) by NAT_1:38
.= n +^ (m+1);
end;
A3: P[0] by ORDINAL2:27;
for m holds P[m] from NAT_1:sch 2(A3,A1);
hence thesis;
end;
theorem Th36:
n*m = n *^ m
proof
defpred P[Nat] means $1*m = $1 *^ m;
A1: for n st P[n] holds P[n+1]
proof
let n such that
A2: P[n];
thus (n+1)*m = n*m+1*m .= n *^ m +^ m by A2,Th35
.= n *^ m +^ 1 *^ m by ORDINAL2:39
.= ( n +^ 1) *^ m by ORDINAL3:46
.= (succ Segm n) *^ m by ORDINAL2:31
.= Segm (n+1) *^ m by NAT_1:38
.= (n+1) *^ m;
end;
A3: P[0] by ORDINAL2:35;
for n holds P[n] from NAT_1:sch 2(A3,A1);
hence thesis;
end;
theorem Th37:
card(n+m) = card n +` card m
by Th35;
theorem Th38:
card(n*m) = card n *` card m
proof
thus card(n*m) = card( n *^ m) by Th36
.= card n *` card m by Th13;
end;
theorem Th39:
for X,Y being finite set st X misses Y holds card (X \/ Y) = card X + card Y
proof
let X,Y be finite set;
assume X misses Y;
then card card (X \/ Y) = card card X +` card card Y by Th34
.= card (card X + card Y) by Th37;
hence thesis;
end;
theorem Th40:
for X being finite set st not x in X holds card (X \/ {x}) = card X + 1
proof
let X be finite set;
A1: card {x} = 1 by CARD_1:30;
assume not x in X;
hence thesis by A1,Th39,ZFMISC_1:50;
end;
theorem Th41:
for X being set holds card X = 1 iff ex x being object st X = {x}
proof
let X be set;
card {0} = 1 by CARD_1:30;
hence card X = 1 implies ex x being object st X = {x} by CARD_1:29;
given x being object such that
A1: X = {x};
thus thesis by A1,CARD_1:30;
end;
theorem Th42:
for X,Y being finite set holds card(X \/ Y) <= card X + card Y
proof
let X,Y be finite set;
card X = card card X & card Y = card card Y;
then card X +` card Y = card(card X + card Y) by Th37;
then
card Segm card(X \/ Y) = card(X \/ Y) &
card (X \/ Y) c= card Segm(card X + card Y) by Th33;
hence thesis by NAT_1:40;
end;
theorem Th43:
for X,Y being finite set st Y c= X holds card (X \ Y) = card X - card Y
proof
let X,Y be finite set;
defpred P[set] means ex S being finite set st S = $1 & card (X \ S) = card X
- card S;
card X - 0 = card X & X \ {} = X;
then
A1: P[{}] by CARD_1:27;
assume
A2: Y c= X;
A3: for X1,Z being set st X1 in Y & Z c= Y & P[Z] holds P[Z \/ {X1}]
proof
let X1,Z be set such that
A4: X1 in Y and
A5: Z c= Y and
A6: P[Z] and
A7: not P[Z \/ {X1}];
A8: card {X1} = 1 by CARD_1:30;
A9: now
assume X1 in Z;
then {X1} c= Z by ZFMISC_1:31;
then Z = Z \/ {X1} by XBOOLE_1:12;
hence P[Z \/ {X1}] by A6;
end;
then
A10: X1 in X \ Z by A2,A4,A7,XBOOLE_0:def 5;
then consider m being Nat such that
A11: card (X \ Z) = m+1 by NAT_1:6;
reconsider Z1 = Z as finite set by A5;
A12: X \ Z, card (X \ Z) are_equipotent & X \ (Z \/ {X1}) = X \ Z \ {X1}
by CARD_1:def 2,XBOOLE_1:41;
card { X1} = 1 by CARD_1:30;
then
A13: card Z1 + card {X1} = card (Z1 \/ {X1}) by A7,A9,Th40;
Segm(m+1) = succ Segm m by NAT_1:38;
then m in m+1 & m = m+1 \ {m} by ORDINAL1:6,37;
then X \ (Z \/ {X1}), m are_equipotent by A10,A11,A12,CARD_1:34;
then card (X \ (Z \/ {X1})) = card X - card (Z1 \/ {X1}) by A6,A13,A11,A8,
CARD_1:def 2;
hence contradiction by A7;
end;
A14: Y is finite;
P[Y] from FINSET_1:sch 2(A14,A1,A3);
hence thesis;
end;
theorem
for X,Y being finite set holds card (X \/ Y) = card X + card Y - card
(X /\ Y)
proof
let X,Y be finite set;
Y \ X = Y \ X /\ Y by XBOOLE_1:47;
then
A1: card (Y \ X) = card Y - card (X /\ Y) by Th43,XBOOLE_1:17;
card (X \/ (Y \ X)) = card X + card (Y \ X) by Th39,XBOOLE_1:79;
hence thesis by A1,XBOOLE_1:39;
end;
theorem
for X,Y being finite set holds card [:X,Y:] = card X * card Y
proof
let X,Y be finite set;
card card [:X,Y:] = card card X *` card card Y by Th6
.= card (card X * card Y) by Th38;
hence thesis;
end;
theorem :: GRAPH_5:1, AK, 21.02.2006
for f being finite Function holds card rng f <= card dom f
proof let f be finite Function;
Segm card rng f c= Segm card dom f by CARD_1:12;
hence thesis by NAT_1:39;
end;
theorem
for X,Y being finite set st X c< Y holds card X < card Y &
card X in Segm card Y
proof
let X,Y be finite set;
assume
A1: X c< Y;
then X c= Y;
then
A2: Y = X \/ (Y\X) by XBOOLE_1:45;
then
A3: card Y = card X + card (Y\X) by Th39,XBOOLE_1:79;
then
A4: card X <= card Y by NAT_1:11;
now
assume card (Y\X) = 0;
then Y \ X = {};
hence contradiction by A1,A2;
end;
then card X <> card Y by A3;
hence card X < card Y by A4,XXREAL_0:1;
hence thesis by NAT_1:44;
end;
theorem
(card X c= card Y or card X in card Y) & Y is finite implies X is finite
proof
assume that
A1: card X c= card Y or card X in card Y and
A2: Y is finite;
card X c= card Y by A1,ORDINAL1:def 2;
hence thesis by A2;
end;
reserve x1,x2,x3,x4,x5,x6,x7,x8 for object;
theorem Th49:
card {x1,x2} <= 2
proof
A1: {x1,x2} = {x1} \/ {x2} & 1+1 = 2 by ENUMSET1:1;
card {x1} = 1 & card {x2} = 1 by CARD_1:30;
hence thesis by A1,Th42;
end;
theorem Th50:
card {x1,x2,x3} <= 3
proof
card {x2,x3} <= 2 by Th49;
then
A1: 1 + card {x2,x3} <= 1+2 by XREAL_1:7;
card {x1} = 1 & {x1,x2,x3} = {x1} \/ {x2,x3} by CARD_1:30,ENUMSET1:2;
then card {x1,x2,x3} <= 1 + card {x2,x3} by Th42;
hence thesis by A1,XXREAL_0:2;
end;
theorem Th51:
card {x1,x2,x3,x4} <= 4
proof
card {x2,x3,x4} <= 3 by Th50;
then
A1: 1 + card {x2,x3,x4} <= 1+3 by XREAL_1:7;
card {x1} = 1 & {x1,x2,x3,x4} = {x1} \/ {x2,x3,x4} by CARD_1:30,ENUMSET1:4;
then card {x1,x2,x3,x4} <= 1 + card {x2,x3,x4 } by Th42;
hence thesis by A1,XXREAL_0:2;
end;
theorem Th52:
card {x1,x2,x3,x4,x5} <= 5
proof
card {x2,x3,x4,x5} <= 4 by Th51;
then
A1: 1 + card {x2,x3,x4,x5} <= 1+4 by XREAL_1:7;
card {x1} = 1 & {x1,x2,x3,x4,x5} = {x1} \/ {x2,x3,x4,x5} by CARD_1:30
,ENUMSET1:7;
then card {x1,x2,x3,x4,x5} <= 1 + card {x2,x3,x4,x5} by Th42;
hence thesis by A1,XXREAL_0:2;
end;
theorem Th53:
card {x1,x2,x3,x4,x5,x6} <= 6
proof
card {x2,x3,x4,x5,x6} <= 5 by Th52;
then
A1: 1 + card {x2,x3,x4,x5,x6} <= 1+5 by XREAL_1:7;
card {x1} = 1 & {x1,x2,x3,x4,x5,x6} = {x1} \/ {x2,x3,x4,x5,x6} by CARD_1:30
,ENUMSET1:11;
then card {x1,x2,x3,x4,x5,x6} <= 1 + card {x2,x3,x4,x5,x6} by Th42;
hence thesis by A1,XXREAL_0:2;
end;
theorem Th54:
card {x1,x2,x3,x4,x5,x6,x7} <= 7
proof
card {x2,x3,x4,x5,x6,x7} <= 6 by Th53;
then
A1: 1 + card {x2,x3,x4,x5,x6,x7} <= 1+6 by XREAL_1:7;
card {x1} = 1 & {x1,x2,x3,x4,x5,x6,x7} = {x1} \/ {x2,x3,x4,x5,x6,x7} by
CARD_1:30,ENUMSET1:16;
then card {x1,x2,x3,x4,x5,x6,x7} <= 1 + card {x2,x3,x4,x5,x6,x7} by Th42;
hence thesis by A1,XXREAL_0:2;
end;
theorem
card {x1,x2,x3,x4,x5,x6,x7,x8} <= 8
proof
card {x2,x3,x4,x5,x6,x7,x8} <= 7 by Th54;
then
A1: 1 + card {x2,x3,x4,x5,x6,x7,x8} <= 1+7 by XREAL_1:7;
{x1,x2,x3,x4,x5,x6,x7,x8} = {x1} \/ {x2,x3,x4,x5,x6,x7,x8} & card {x1} =
1 by CARD_1:30,ENUMSET1:22;
then card {x1,x2,x3,x4,x5,x6,x7,x8} <= 1 + card {x2,x3,x4,x5,x6,x7,x8} by
Th42;
hence thesis by A1,XXREAL_0:2;
end;
theorem Th56:
x1 <> x2 implies card {x1,x2} = 2
proof
A1: card {x1} = 1 & card {x2} = 1 by CARD_1:30;
A2: {x1,x2} = {x1} \/ {x2} & 1+1 = 2 by ENUMSET1:1;
assume x1 <> x2;
hence thesis by A1,A2,Th39,ZFMISC_1:11;
end;
theorem Th57:
x1 <> x2 & x1 <> x3 & x2 <> x3 implies card {x1,x2,x3} = 3
proof
assume x1 <> x2 & x1 <> x3 & x2 <> x3;
then
A1: card {x1,x2} = 2 & not x3 in {x1,x2} by Th56,TARSKI:def 2;
{x1,x2,x3} = {x1,x2} \/ {x3} by ENUMSET1:3;
hence card {x1,x2,x3} = 2+1 by A1,Th40
.= 3;
end;
theorem Th58:
x1 <> x2 & x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 & x3 <> x4
implies card {x1,x2,x3,x4} = 4
proof
assume x1 <> x2 & x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 & x3 <> x4;
then
A1: card {x1,x2,x3} = 3 & not x4 in {x1,x2,x3} by Th57,ENUMSET1:def 1;
{x1,x2,x3,x4} = {x1,x2,x3} \/ {x4} by ENUMSET1:6;
hence card {x1,x2,x3,x4} = 3+1 by A1,Th40
.= 4;
end;
begin :: Addenda
:: from GROUP_3
theorem
for X being set st card X = 2
ex x,y being object st x <> y & X = {x,y}
proof
let X be set;
assume
A1: card X = 2;
then consider x being object such that
A2: x in X by CARD_1:27,XBOOLE_0:def 1;
X is finite by A1;
then reconsider Y = X as finite set;
{x} c= X by A2,ZFMISC_1:31;
then card(X \ {x}) = card Y - card{x} by Th43
.= 2 - 1 by A1,CARD_1:30;
then consider y being object such that
A3: X \ {x} = {y} by Th41;
take x,y;
x in {x} by TARSKI:def 1;
hence x <> y by A3,XBOOLE_0:def 5;
thus X c= {x,y}
proof
let z be object;
assume
A4: z in X;
per cases;
suppose
z = x;
hence thesis by TARSKI:def 2;
end;
suppose
z <> x;
then not z in {x} by TARSKI:def 1;
then z in {y} by A3,A4,XBOOLE_0:def 5;
then z = y by TARSKI:def 1;
hence thesis by TARSKI:def 2;
end;
end;
let z be object;
assume z in {x,y};
then
A5: z = x or z = y by TARSKI:def 2;
y in X \ {x} by A3,TARSKI:def 1;
hence thesis by A2,A5;
end;
:: from YELLOW_6, 2004.07.25
theorem
for f being Function holds card rng f c= card dom f
proof
let f be Function;
rng f = f.:dom f by RELAT_1:113;
hence thesis by CARD_1:66;
end;
:: from RLVECT_3
Lm5: now
let n;
assume
A1: for Z being finite set holds card Z = n & Z <> {} & (for X,Y st X in
Z & Y in Z holds X c= Y or Y c= X) implies union Z in Z;
let Z be finite set;
assume that
A2: card Z = n + 1 and
A3: Z <> {} and
A4: for X,Y st X in Z & Y in Z holds X c= Y or Y c= X;
set y = the Element of Z;
per cases;
suppose
n = 0;
then consider x being object such that
A5: Z = {x} by A2,Th41;
thus union Z in Z by A5,TARSKI:def 1;
end;
suppose
A6: n <> 0;
set Y = Z \ {y};
reconsider Y as finite set;
{y} c= Z by A3,ZFMISC_1:31;
then
A7: card Y = (n + 1) - card{y} by A2,Th43
.= n + 1 - 1 by CARD_1:30
.= n;
for a,b being set st a in Y & b in Y holds a c= b or b c= a by A4;
then
A8: union Y in Y by A1,A6,A7,CARD_1:27;
then
A9: union Y in Z;
Z = (Z \ {y}) \/ {y}
proof
thus Z c= (Z \ {y}) \/ {y}
proof
let x be object;
assume x in Z;
then x in Z \ {y} or x in {y} by XBOOLE_0:def 5;
hence thesis by XBOOLE_0:def 3;
end;
let x be object;
assume x in (Z \ {y}) \/ {y};
then
A10: x in (Z \ {y}) or x in {y} by XBOOLE_0:def 3;
{y} c= Z by A3,ZFMISC_1:31;
hence thesis by A10;
end;
then
A11: union Z = union Y \/ union {y} by ZFMISC_1:78
.= union Y \/ y;
A12: y in Z by A3;
y c= union Y or union Y c= y by A4,A8;
hence union Z in Z by A9,A12,A11,XBOOLE_1:12;
end;
end;
Lm6: for Z being finite set holds Z <> {} & (for X,Y st X in Z & Y in Z holds
X c= Y or Y c= X) implies union Z in Z
proof
defpred P[Nat] means for Z being finite set st card Z = $1 & Z <>
{} & (for X,Y st X in Z & Y in Z holds X c= Y or Y c= X) holds union Z in Z;
let Z be finite set;
A1: card Z = card Z;
A2: P[0];
A3: for k be Nat st P[k] holds P[k+1] by Lm5;
for n holds P[n] from NAT_1:sch 2(A2,A3);
hence thesis by A1;
end;
theorem
Z <> {} & Z is finite & (for X,Y st X in Z & Y in Z holds X c= Y or Y
c= X) implies union Z in Z by Lm6;
theorem
x1,x2,x3,x4,x5 are_mutually_distinct implies card {x1,x2,x3,x4,x5} = 5
proof
A1: {x1,x2,x3,x4,x5} = {x1,x2,x3,x4} \/ {x5} by ENUMSET1:10;
assume
A2: x1,x2,x3,x4,x5 are_mutually_distinct;
then
A3: x3 <> x5 & x4 <> x5 by ZFMISC_1:def 7;
A4: x2 <> x4 & x3 <> x4 by A2,ZFMISC_1:def 7;
A5: x1 <> x4 & x2 <> x3 by A2,ZFMISC_1:def 7;
x1 <> x5 & x2 <> x5 by A2,ZFMISC_1:def 7;
then
A6: not x5 in {x1,x2,x3,x4} by A3,ENUMSET1:def 2;
x1 <> x2 & x1 <> x3 by A2,ZFMISC_1:def 7;
then card {x1,x2,x3,x4} = 4 by A5,A4,Th58;
hence card {x1,x2,x3,x4,x5} = 4+1 by A6,A1,Th40
.= 5;
end;
:: from MATRIX_1, 2007.07.22, A.T, generalized
theorem
for M1, M2 being set st card M1 = 0 & card M2 = 0 holds M1 = M2
proof
let M1, M2 be set;
assume that
A1: card M1 = 0 and
A2: card M2 = 0;
M1 = {} by A1;
hence thesis by A2;
end;
:: missing, 2007.06.14, A.T.
registration
let x,y;
cluster [x,y] -> non natural;
coherence
proof
assume [x,y] is natural;
then reconsider n = [x,y] as Nat;
card n <= 2 by Th49;
then
n <= 2;
then n = 0 or ... or n = 2;
then per cases;
suppose
n = 0;
hence contradiction;
end;
suppose
n = 1;
hence contradiction by CARD_1:49,ZFMISC_1:4;
end;
suppose
n = 2;
hence contradiction by CARD_1:50,ZFMISC_1:6;
end;
end;
end;
begin :: from CARD_3, 2011.04.16, A.T.
reserve A,B,C for Ordinal,
K,L,M,N for Cardinal,
x,y,y1,y2,z,u for object,X,Y,Z,Z1,Z2 for set,
n for Nat,
f,f1,g,h for Function,
Q,R for Relation;
theorem
Sum(M --> N) = M*`N
proof
thus Sum(M --> N) = card [:N,M:] by CARD_3:25
.= M*`N by Lm2;
end;
theorem
Product(N --> M) = exp(M,N) by CARD_3:11;
scheme FinRegularity { X()->finite set, P[object,object] }:
ex x st x in X() & for y st y in X() & y <> x holds not P[y,x]
provided
A1: X() <> {} and
A2: for x,y st P[x,y] & P[y,x] holds x = y and
A3: for x,y,z st P[x,y] & P[y,z] holds P[x,z]
proof
defpred Q[Nat] means
for X being finite set st card X = $1 & X <> {}
ex x st x in X & for y st y in X & y <> x holds not P[y,x];
A4: Q[0];
A5: Q[n] implies Q[n+1]
proof
assume
A6: for X being finite set st card X = n & X <> {}
ex x st x in X & for y st y in X & y <> x holds not P[y,x];
let X be finite set;
assume that
A7: card X = n+1 and
A8: X <> {};
set x = the Element of X;
A9: now
assume X\{x} = {};
then
A10: X c= {x} by XBOOLE_1:37;
thus thesis
proof
take x;
thus x in X by A8;
thus thesis by A10,TARSKI:def 1;
end;
end;
now
assume
A11: X\{x} <> {};
{x} c= X by A8,ZFMISC_1:31;
then
A12: card (X\{x}) = (n+1) - card {x} by A7,Th43;
card {x} = 1 by CARD_1:30;
then consider y such that
A13: y in X\{x} and
A14: for z st z in X\{x} & z <> y holds not P[z,y] by A6,A11,A12;
A15: now
assume
A16: P[x,y];
thus thesis
proof
take x;
thus x in X by A8;
let z;
assume that
A17: z in X and
A18: z <> x and
A19: P[z,x];
not z in {x} by A18,TARSKI:def 1;
then
A20: z in X \ {x} by A17,XBOOLE_0:def 5;
A21: not y in {x} by A13,XBOOLE_0:def 5;
A22: z = y by A3,A14,A16,A19,A20;
y <> x by A21,TARSKI:def 1;
hence contradiction by A2,A16,A19,A22;
end;
end;
now
assume
A23: not P[x,y];
thus thesis
proof
take y;
thus y in X by A13;
let z such that
A24: z in X and
A25: z <> y;
z in {x} or not z in {x};
then z = x or z in X \ {x} by A24,TARSKI:def 1,XBOOLE_0:def 5;
hence thesis by A14,A23,A25;
end;
end;
hence thesis by A15;
end;
hence thesis by A9;
end;
A26: Q[n] from NAT_1:sch 2(A4,A5);
card X() = card X();
hence thesis by A1,A26;
end;
scheme MaxFinSetElem { X()->finite set, P[object,object] }:
ex x st x in X() & for y st y in X() holds P[x,y]
provided
A1: X() <> {} and
A2: for x,y holds P[x,y] or P[y,x] and
A3: for x,y,z st P[x,y] & P[y,z] holds P[x,z]
proof
defpred Q[Nat] means
for X being finite set st card X = $1 & X <> {}
ex x st x in X & for y st y in X holds P[x,y];
A4: Q[0];
A5: Q[n] implies Q[n+1]
proof
assume
A6: for X being finite set st card X = n & X <> {}
ex x st x in X & for y st y in X holds P[x,y];
let X be finite set;
assume that
A7: card X = n+1 and
A8: X <> {};
set x = the Element of X;
A9: now
assume X\{x} = {};
then
A10: X c= {x} by XBOOLE_1:37;
thus thesis
proof
take x;
thus x in X by A8;
let y;
assume y in X;
then y = x by A10,TARSKI:def 1;
hence thesis by A2;
end;
end;
now
assume
A11: X\{x} <> {};
{x} c= X by A8,ZFMISC_1:31;
then
A12: card (X\{x}) = (n+1) - card {x} by A7,Th43;
card {x} = 1 by CARD_1:30;
then consider y such that
A13: y in X\{x} and
A14: for z st z in X\{x} holds P[y,z] by A6,A11,A12;
A15: P[x,y] or P[y,x] by A2;
A16: P[x,x] by A2;
P[y,y] by A2;
then consider z such that
A17: z = x or z = y and
A18: P[z,x] and
A19: P[z,y] by A15,A16;
thus thesis
proof
take z;
thus z in X by A13,A17;
let u;
A20: u in {x} or not u in {x};
assume u in X;
then u = x or u in X\{x} by A20,TARSKI:def 1,XBOOLE_0:def 5;
then P[z,u] or P[y,u] by A14,A18;
hence thesis by A3,A19;
end;
end;
hence thesis by A9;
end;
A21: Q[n] from NAT_1:sch 2(A4,A5);
card X() = card X();
hence thesis by A1,A21;
end;
Lm7: Rank n is finite implies Rank (n+1) is finite
proof
Segm(n+1) = succ Segm n by NAT_1:38;
then Rank (n+1) = bool Rank n by CLASSES1:30;
hence thesis;
end;
Lm8: 1 = card 1;
theorem
Rank n is finite
proof
defpred P[Nat] means Rank $1 is finite;
A1: P[0] by CLASSES1:29;
A2: for n st P[n] holds P[n+1] by Lm7;
for n holds P[n] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
theorem
0 in M iff 1 c= M
proof 0+1 = 1;
then nextcard card Segm 0 = card Segm 1 by NAT_1:42;
hence thesis by CARD_3:90;
end;
theorem
1 in M iff 2 c= M
proof 1+1 = 2;
then nextcard card Segm 1 = card Segm 2 by NAT_1:42;
hence thesis by CARD_3:90;
end;
reserve n,k for Nat;
theorem Th69:
A is limit_ordinal iff for B,n st B in A holds B+^ n in A
proof
thus A is limit_ordinal implies for B,n st B in A holds B+^ n in A
proof
assume
A1: A is limit_ordinal;
let B,n;
defpred P[Nat] means B+^ $1 in A;
assume B in A;
then
A2: P[0] by ORDINAL2:27;
A3: P[k] implies P[k+1]
proof Segm(k+1) = succ Segm k by NAT_1:38;
then B+^(k+1) = succ (B+^ k) by ORDINAL2:28;
hence thesis by A1,ORDINAL1:28;
end;
P[k] from NAT_1:sch 2(A2,A3);
hence thesis;
end;
assume
A4: for B,n st B in A holds B+^ n in A;
now
let B;
assume B in A;
then B+^ 1 in A by A4;
hence succ B in A by ORDINAL2:31;
end;
hence thesis by ORDINAL1:28;
end;
theorem Th70:
A+^succ n = succ A +^ n & A +^ (n+1) = succ A +^ n
proof
defpred P[Nat] means A+^succ $1 = succ A +^ $1;
A+^succ 0 = succ A by ORDINAL2:31
.= succ A +^ 0 by ORDINAL2:27;
then
A1: P[0];
A2: P[k] implies P[k+1]
proof
assume
A3: P[k];
A4: Segm(k+1) = succ Segm k by NAT_1:38;
hence A+^succ (k+1) = succ (succ A +^ k) by A3,ORDINAL2:28
.= succ A +^ k +^ 1 by ORDINAL2:31
.= succ A +^ ( k +^ 1) by ORDINAL3:30
.= succ A +^ (k+1) by A4,ORDINAL2:31;
end;
A5: P[k] from NAT_1:sch 2(A1,A2);
thus
A6: A+^succ n = succ A +^ n by A5;
Segm(n+1) = succ Segm n by NAT_1:38;
hence thesis by A6;
end;
theorem Th71:
ex n st A*^succ 1 = A +^ n
proof
defpred P[Ordinal] means ex n st $1*^2 = $1+^ n;
{}+^{} = {} by ORDINAL2:27;
then
A1: P[0] by ORDINAL2:35;
A2: for A st P[A] holds P[succ A]
proof
let A;
given n such that
A3: A*^2 = A+^ n;
take n+1;
(succ A)*^2 = A*^2+^2 by ORDINAL2:36
.= succ(A*^succ 1+^1) by ORDINAL2:28
.= succ succ(A+^ n) by A3,ORDINAL2:31
.= succ (A+^succ Segm n) by ORDINAL2:28
.= succ (A+^ Segm(n+1)) by NAT_1:38
.= A+^succ (n+1) by ORDINAL2:28;
hence thesis by Th70;
end;
A4: for A st A <> 0 & A is limit_ordinal & for B st B in A holds P[B]
holds P[A]
proof
let A;
assume that
A5: A <> 0 and
A6: A is limit_ordinal and
A7: for B st B in A holds P[B];
take 0;
deffunc f(Ordinal) = $1*^2;
consider phi being Ordinal-Sequence such that
A8: dom phi = A and
A9: for B st B in A holds phi.B = f(B) from ORDINAL2:sch 3;
A10: A*^2 = union sup phi by A5,A6,A8,A9,ORDINAL2:37
.= union sup rng phi by ORDINAL2:26;
thus A*^2 c= A+^ 0
proof
let B;
assume B in A*^2;
then consider X such that
A11: B in X and
A12: X in sup rng phi by A10,TARSKI:def 4;
reconsider X as Ordinal by A12;
consider C being Ordinal such that
A13: C in rng phi and
A14: X c= C by A12,ORDINAL2:21;
consider x being object such that
A15: x in dom phi and
A16: C = phi.x by A13,FUNCT_1:def 3;
reconsider x as Ordinal by A15;
A17: ex n st x*^2 = x+^ n by A7,A8,A15;
C = x*^2 by A8,A9,A15,A16;
then
A18: C in A by A6,A8,A15,A17,Th69;
A+^{} = A by ORDINAL2:27;
hence thesis by A11,A14,A18,ORDINAL1:10;
end;
A19: 1 in succ 1 by ORDINAL1:6;
A20: A+^ 0 = A by ORDINAL2:27;
A21: A = A*^1 by ORDINAL2:39;
1 c= 2 by A19,ORDINAL1:def 2;
hence thesis by A20,A21,ORDINAL2:42;
end;
for A holds P[A] from ORDINAL2:sch 1(A1,A2,A4);
hence thesis;
end;
theorem Th72:
A is limit_ordinal implies A *^ succ 1 = A
proof consider n such that
A1: A*^2 = A+^ n by Th71;
assume A is limit_ordinal;
then
A2: A+^ n is limit_ordinal by A1,ORDINAL3:40;
now
assume n <> 0;
then consider k being Nat such that
A3: n = k+1 by NAT_1:6;
reconsider k as Element of NAT by ORDINAL1:def 12;
Segm n = succ Segm k by A3,NAT_1:38;
then A+^ n = succ(A+^ k) by ORDINAL2:28;
hence contradiction by A2,ORDINAL1:29;
end;
hence thesis by A1,ORDINAL2:27;
end;
Lm9: omega is limit_ordinal by ORDINAL1:def 11;
theorem Th73:
omega c= A implies 1+^A = A
proof
deffunc f(Ordinal) = 1+^$1;
consider phi being Ordinal-Sequence such that
A1: dom phi = omega & for B st B in omega holds phi.B = f(B)
from ORDINAL2:sch 3;
A2: 1+^omega = sup phi by A1,Lm9,ORDINAL2:29
.= sup rng phi by ORDINAL2:26;
A3: 1+^omega c= omega
proof
let B;
assume B in 1+^omega;
then consider C being Ordinal such that
A4: C in rng phi and
A5: B c= C by A2,ORDINAL2:21;
consider x being object such that
A6: x in dom phi and
A7: C = phi.x by A4,FUNCT_1:def 3;
reconsider x as Ordinal by A6;
reconsider x9 = x as Cardinal by A1,A6;
reconsider x as finite Ordinal by A1,A6;
A8: C = 1+^x by A1,A6,A7;
succ x in omega by A1,A6,Lm9,ORDINAL1:28;
then C in omega by A8,ORDINAL2:31;
hence thesis by A5,ORDINAL1:12;
end;
assume omega c= A;
then
A9: ex B st A = omega+^B by ORDINAL3:27;
omega c= 1+^omega by ORDINAL3:24;
then omega = 1+^omega by A3;
hence thesis by A9,ORDINAL3:30;
end;
registration
cluster infinite -> limit_ordinal for Cardinal;
coherence
proof
let M be Cardinal;
assume M is infinite;
then
A1: not M in omega;
assume not thesis;
then consider A such that
A2: M = succ A by ORDINAL1:29;
omega = succ A or omega in succ A by A1,A2,CARD_1:4;
then
A3: omega c= A by Lm9,ORDINAL1:22,29;
card (A+^1) = card 1 +` card A by Th12
.= card (1+^A) by Th12
.= card A by A3,Th73;
then card succ A = card A by ORDINAL2:31;
then
A4: A,succ A are_equipotent by CARD_1:5;
A5: not succ A c= A by ORDINAL1:5,6;
ex B st succ A = B & for A st A,B are_equipotent holds B c= A by A2,
CARD_1:def 1;
hence contradiction by A4,A5;
end;
end;
theorem Th74:
not M is finite implies M+`M = M
proof
assume not M is finite;
then M*^succ 1 = M by Th72;
then card M = (card 2)*`card M by Th13
.= card (succ 1*^ M) by Th13
.= card (1*^ M+^ M) by ORDINAL2:36
.= M+`M by ORDINAL2:39;
hence thesis;
end;
theorem Th75:
not M is finite & (N c= M or N in M) implies M+`N = M & N+`M = M
proof
assume that
A1: not M is finite and
A2: N c= M or N in M;
A3: M+`M = M by A1,Th74;
N c= M by A2,CARD_1:3;
then
A4: M +^ N c= M +^ M by ORDINAL2:33;
A5: M c= M +^ N by ORDINAL3:24;
A6: card M = M;
A7: M+`N c= M by A3,A4,CARD_1:11;
M c= M+`N by A5,A6,CARD_1:11;
hence thesis by A7;
end;
theorem
not X is finite & (X,Y are_equipotent or Y,X are_equipotent) implies
X \/ Y,X are_equipotent & card (X \/ Y) = card X
proof
assume that
A1: not X is finite and
A2: X,Y are_equipotent or Y,X are_equipotent;
A3: card X = card Y by A2,CARD_1:5;
A4: card X c= card (X \/ Y) by CARD_1:11,XBOOLE_1:7;
A5: card (X \/ Y) c= card X +` card Y by Th33;
card X +` card Y = card X by A1,A3,Th74;
then card X = card (X \/ Y) by A4,A5;
hence thesis by CARD_1:5;
end;
theorem
not X is finite & Y is finite implies
X \/ Y,X are_equipotent & card (X \/ Y) = card X
proof
assume that
A1: not X is finite and
A2: Y is finite;
card Y in card X by A1,A2,CARD_3:86;
then
A3: card X +` card Y = card X by A1,Th75;
A4: card (X \/ Y) c= card X +` card Y by Th33;
card X c= card (X \/ Y) by CARD_1:11,XBOOLE_1:7;
then card X = card (X \/ Y) by A3,A4;
hence thesis by CARD_1:5;
end;
theorem
not X is finite & (card Y in card X or card Y c= card X) implies
X \/ Y,X are_equipotent & card (X \/ Y) = card X
proof
assume that
A1: not X is finite and
A2: card Y in card X or card Y c= card X;
A3: card X +` card Y = card X by A1,A2,Th75;
A4: card (X \/ Y) c= card X +` card Y by Th33;
card X c= card (X \/ Y) by CARD_1:11,XBOOLE_1:7;
then card X = card (X \/ Y) by A3,A4;
hence thesis by CARD_1:5;
end;
registration let M,N be finite Cardinal;
cluster M+`N -> finite;
coherence
proof
M+`N = card (card M + card N) by Th37;
hence thesis;
end;
end;
theorem
for M,N being finite Cardinal holds M+`N is finite;
theorem
not M is finite implies not M+`N is finite & not N+`M is finite
proof
assume
A1: not M is finite;
M c= N or N c= M;
then M c= N & not N is finite or M+`N = M & N+`M = M by A1,Th75;
hence thesis by A1,Th75;
end;
theorem
for M,N being finite Cardinal holds M*`N is finite;
theorem Th82:
K in L & M in N or K c= L & M in N or K in L & M c= N or K c= L & M c= N
implies K+`M c= L+`N & M+`K c= L+`N
proof
assume that
A1: K in L & M in N or K c= L & M in N or K in L & M c= N or K c= L & M c=
N;
A2: K c= L by A1,CARD_1:3;
A3: M c= N by A1,CARD_1:3;
A4: K+`M = card ( K +^ M);
A5: K +^ M c= L +^ N by A2,A3,ORDINAL3:18;
hence K+`M c= L+`N by CARD_1:11;
thus thesis by A4,A5,CARD_1:11;
end;
theorem
M in N or M c= N implies K+`M c= K+`N & K+`M c= N+`K &
M+`K c= K+`N & M+`K c= N+`K by Th82;
theorem Th84:
X is countable & Y is countable implies X \/ Y is countable
proof
assume that
A1: card X c= omega and
A2: card Y c= omega;
A3: card (X \/ Y) c= card X +` card Y by Th33;
A4: omega +` omega = omega by Th74;
card X +` card Y c= omega +` omega by A1,A2,Th82;
hence card (X \/ Y) c= omega by A3,A4;
end;
theorem Th85:
(card dom f c= M & for x st x in dom f holds card (f.x) c= N) implies
card Union f c= M*`N
proof
assume that
A1: card dom f c= M and
A2: for x st x in dom f holds card (f.x) c= N;
A3: card Union f c= Sum Card f by CARD_3:39;
A4: dom Card f = dom f by CARD_3:def 2;
A5: dom(dom f --> N) = dom f by FUNCOP_1:13;
now
let x be object;
assume
A6: x in dom Card f;
then
A7: (Card f).x = card (f.x) by A4,CARD_3:def 2;
(dom f --> N).x = N by A4,A6,FUNCOP_1:7;
hence (Card f).x c= (dom f --> N).x by A2,A4,A6,A7;
end;
then Sum Card f c= Sum(dom f --> N) by A4,A5,CARD_3:30;
then
A8: card Union f c= Sum(dom f --> N) by A3;
A9: [:card dom f,N:] c= [:M,N:] by A1,ZFMISC_1:95;
Sum(dom f --> N) = card [:N,dom f:] by CARD_3:25
.= card [:N,card dom f:] by Th6
.= card [:card dom f,N:] by Th4;
then
A10: Sum(dom f --> N) c= card [:M,N:] by A9,CARD_1:11;
thus thesis by A8,A10;
end;
theorem
(card X c= M & for Y st Y in X holds card Y c= N) implies card union X c=
M*`N
proof
assume that
A1: card X c= M and
A2: for Y st Y in X holds card Y c= N;
now
let x;
assume x in dom id X;
then (id X).x in X by FUNCT_1:18;
hence card ((id X).x) c= N by A2;
end;
then card Union id X c= M*`N by A1,Th85;
hence thesis;
end;
theorem Th87:
for f st dom f is finite &
for x st x in dom f holds f.x is finite holds Union f is finite
proof
let f;
assume that
A1: dom f is finite and
A2: for x st x in dom f holds f.x is finite;
reconsider df = dom f as finite set by A1;
now
assume dom f <> {};
then
A3: df <> {};
defpred P[object,object] means card (f.$2) c= card (f.$1);
A4: for x,y holds P[x,y] or P[y,x];
A5: for x,y,z being object st P[x,y] & P[y,z] holds P[x,z] by XBOOLE_1:1;
consider x such that
A6: x in df & for y st y in df holds P[x,y] from MaxFinSetElem(A3,A4,
A5);
reconsider fx = f.x as finite set by A2,A6;
A7: card Union f c= (card card df) *` (card (f.x)) by A6,Th85;
card (f.x) = card card fx;
then card Union f c= card ((card df) * (card fx)) by A7,Th38;
hence thesis;
end;
hence thesis by RELAT_1:42,ZFMISC_1:2;
end;
theorem
(omega)*`(card n) c= omega & (card n)*`(omega) c= omega
proof
defpred P[Nat] means (omega)*`(card $1) c= omega;
A1: P[0];
A2: for k being Nat holds P[k] implies P[k+1]
proof
let k be Nat;
assume
A3: P[k];
card (k+1) = Segm(k+1)
.= succ Segm k by NAT_1:38;
then card (k+1) = card succ k;
then (omega)*`(card (k+1)) =
card (succ k *^ omega) by Th13,CARD_1:47
.= card ( k *^ omega +^ omega) by ORDINAL2:36
.= card ( k *^ omega) +` omega by Th12,CARD_1:47
.= (omega)*`(card k) +` omega by Th13,CARD_1:47
.= omega by A3,Th75;
hence thesis;
end;
A4: for k being Nat holds P[k] from NAT_1:sch 2(A1,A2);
hence (omega)*`(card n) c= omega;
thus thesis by A4;
end;
theorem Th89:
K in L & M in N or K c= L & M in N or K in L & M c= N or K c= L & M c= N
implies K*`M c= L*`N & M*`K c= L*`N
proof
assume that
A1: K in L & M in N or K c= L & M in N or K in L & M c= N or K c= L & M c=
N;
A2: K c= L by A1,CARD_1:3;
A3: M c= N by A1,CARD_1:3;
A4: K*`M = card [:K,M:];
A5: [:K,M:] c= [:L,N:] by A2,A3,ZFMISC_1:96;
hence K*`M c= L*`N by CARD_1:11;
thus thesis by A4,A5,CARD_1:11;
end;
theorem
M in N or M c= N implies
K*`M c= K*`N & K*`M c= N*`K & M*`K c= K*`N & M*`K c= N*`K by Th89;
theorem Th91:
K in L & M in N or K c= L & M in N or K in L & M c= N or K c= L & M c= N
implies K = 0 or exp(K,M) c= exp(L,N)
proof
assume that
A1: K in L & M in N or K c= L & M in N or K in L & M c= N or K c= L & M c=
N;
A2: K c= L by A1,CARD_1:3;
A3: M c= N by A1,CARD_1:3;
now
assume L <> {};
then
A4: Funcs(N\M,L) <> {};
0 c= card Funcs(N\M,L);
then 0 in card Funcs(N\M,L) by A4,CARD_1:3;
then
A5: nextcard Segm card 0 c= card Funcs(N\M,L) by CARD_1:def 3;
0+1 = 1;
then
A6: Segm 1 c= card Funcs(N\M,L) by A5,Lm8,NAT_1:42;
A7: M misses (N\M) by XBOOLE_1:79;
A8: N = M \/ (N\M) by A3,XBOOLE_1:45;
Funcs(M,K) c= Funcs(M,L) by A2,FUNCT_5:56;
then
A9: exp(K,M) c= card Funcs(M,L) by CARD_1:11;
A10: exp(L,N) = card [:Funcs(M,L),Funcs(N\M,L):] by A7,A8,FUNCT_5:62;
A11: card [:Funcs(M,L),Funcs(N\M,L):] = card [:card Funcs(M,L),card Funcs(N\
M,L):] by Th6;
card Funcs(M,L) *` card Funcs(N\M,L) = card [:card Funcs(M,L),card
Funcs(N\M,L):];
then 1 *` card Funcs(M,L) c= exp(L,N) by A6,A10,A11,Th89;
then card Funcs(M,L) c= exp(L,N) by Th20;
hence thesis by A9;
end;
hence thesis by A1;
end;
theorem
M in N or M c= N implies K = 0 or
exp(K,M) c= exp(K,N) & exp(M,K) c= exp(N,K)
proof
assume that
A1: M in N or M c= N and
A2: K <> 0;
thus exp(K,M) c= exp(K,N) by A1,A2,Th91;
M = 0 implies exp(M,K) = 0 by A2;
hence thesis by A1,Th91;
end;
theorem Th93:
M c= M+`N & N c= M+`N
proof
A1: M c= M +^ N by ORDINAL3:24;
A2: N c= M +^ N by ORDINAL3:24;
A3: card N = N;
card M = M;
then
A4: M c= card ( M +^ N) by A1,CARD_1:11;
N c= card ( M +^ N) by A2,A3,CARD_1:11;
hence thesis by A4;
end;
theorem
N <> 0 implies M c= M*`N & M c= N*`M
proof
assume
A1: N <> 0;
A2: card M = M;
card N = N;
then
A3: M*`N = card ( M *^ N) by A2,Th13;
M c= M *^ N by A1,ORDINAL3:36;
hence thesis by A2,A3,CARD_1:11;
end;
theorem Th95:
K in L & M in N implies K+`M in L+`N & M+`K in L+`N
proof
A1: for K,L,M,N st K in L & M in N & L c= N holds K+`M in L+`N
proof
let K,L,M,N such that
A2: K in L and
A3: M in N and
A4: L c= N;
per cases;
suppose
A5: N is finite;
then reconsider N as finite Cardinal;
reconsider L,M,K as finite Cardinal by A2,A3,A4,A5,CARD_3:92;
A6: card Segm K = K;
A7: card Segm L = L;
A8: card Segm M = M;
A9: card Segm N = N;
A10: K+`M = card Segm(card K + card M) by Th37;
A11: L+`N = card Segm(card L + card N) by Th37;
A12: card K < card L by A2,A6,A7,NAT_1:41;
card M < card N by A3,A8,A9,NAT_1:41;
then card K + card M < card L + card N by A12,XREAL_1:8;
hence thesis by A10,A11,NAT_1:41;
end;
suppose
A13: N is not finite;
then
A14: L+`N = N by A4,Th75;
A15: omega c= N by A13,CARD_3:85;
K c= M & (M is finite or M is not finite) or
M c= K & (K is finite or K is not finite);
then
A16: K is finite & M is finite or K+`M = M or K+`M = K & K in N
by A2,A4,Th75;
K is finite & M is finite implies thesis by A14,A15,CARD_1:61;
hence thesis by A3,A4,A13,A16,Th75;
end;
end;
L c= N or N c= L;
hence thesis by A1;
end;
theorem
K+`M in K+`N implies M in N
proof
assume that
A1: K+`M in K+`N and
A2: not M in N;
N c= M by A2,CARD_1:4;
then K+`N c= K+`M by Th82;
hence thesis by A1,CARD_1:4;
end;
theorem
card X +` card Y = card X & card Y in card X implies card (X \ Y) = card X
proof
assume that
A1: card X +` card Y = card X and
A2: card Y in card X;
A3: card X c= card (X \/ Y) by CARD_1:11,XBOOLE_1:7;
card (X \/ Y) c= card X by A1,Th33;
then
A4: card (X \/ Y) = card X by A3;
(X \ Y) \/ Y = X \/ Y by XBOOLE_1:39;
then
A5: card X = card (X \ Y) +` card Y by A4,Th34,XBOOLE_1:79;
then
A6: card (X \ Y) c= card X by Th93;
A7: now
assume not card X is finite;
then
A8: card X +` card X = card X by Th74;
assume not thesis;
then card (X \ Y) in card X by A6,CARD_1:3;
then card X in card X by A2,A5,A8,Th95;
hence contradiction;
end;
now
assume card X is finite;
then reconsider X,Y as finite set by A2,CARD_3:92;
card Y = card card Y;
then card (card X + card Y) = card card X by A1,Th37;
then card X + card Y = card X + 0;
then Y = {};
hence thesis;
end;
hence thesis by A7;
end;
theorem
K*`M in K*`N implies M in N
proof
assume that
A1: K*`M in K*`N and
A2: not M in N;
N c= M by A2,CARD_1:4;
then K*`N c= K*`M by Th89;
hence thesis by A1,CARD_1:4;
end;
theorem
X is countable & Y is countable implies X \+\ Y is countable
proof
assume that
A1: X is countable and
A2: Y is countable;
A3: X \ Y is countable by A1;
Y \ X is countable by A2;
hence thesis by A3,Th84;
end;
registration
let A be finite set, B be set, f be Function of A, Fin B;
cluster Union f -> finite;
coherence
proof
now
let x be object;
assume
A1: x in dom f;
then reconsider A as non empty set;
reconsider x9 = x as Element of A by A1;
reconsider f9 = f as Function of A, Fin B;
f9.x9 is finite;
hence f.x is finite;
end;
hence thesis by Th87;
end;
end;
registration let f be finite finite-yielding Function;
cluster product f -> finite;
coherence
proof
Funcs(dom f, Union f) is finite by FRAENKEL:6;
hence thesis by FINSET_1:1,FUNCT_6:1;
end;
end;
::from COMPL_SP, 2011.07.30, A.T.
theorem
for F be Function st dom F is infinite & rng F is finite ex x st
x in rng F & F"{x} is infinite
proof
let F be Function such that
A1: dom F is infinite and
A2: rng F is finite;
deffunc f(object)=F"{$1};
consider g be Function such that
A3: dom g = rng F &
for x being object st x in rng F holds g.x = f(x) from FUNCT_1:
sch 3;
A4: dom F c= Union g
proof
let x be object such that
A5: x in dom F;
A6: F.x in rng F by A5,FUNCT_1:def 3;
then
A7: g.(F.x) in rng g by A3,FUNCT_1:def 3;
F.x in {F.x} by TARSKI:def 1;
then
A8: x in F"{F.x} by A5,FUNCT_1:def 7;
g.(F.x)=F"{F.x} by A3,A6;
then x in union rng g by A8,A7,TARSKI:def 4;
hence thesis;
end;
assume
A9: for x st x in rng F holds F"{x} is finite;
now
let x such that
A10: x in dom g;
g.x=F"{x} by A3,A10;
hence g.x is finite by A9,A3,A10;
end;
then Union g is finite by A2,A3,Th87;
hence thesis by A1,A4;
end;
:: from PRE_POLY, CARD_FIN etc., 2012.06.27, A.T.
theorem
for X,Y being finite set st X c= Y & card X=card Y
holds X=Y
proof let X,Y be finite set such that
A1: X c= Y and
A2: card X=card Y;
card (Y\X)=card Y-card X by A1,Th43;
then Y\X={} by A2;
then Y c= X by XBOOLE_1:37;
hence thesis by A1;
end;
scheme { X()->finite set, P[object,object] }:
ex x being set st x in X() &
for y being set st y in X() & y <> x holds not P[y,x]
provided
A1: X() <> {} and
A2: for x,y being set st P[x,y] & P[y,x] holds x = y and
A3: for x,y,z being set st P[x,y] & P[y,z] holds P[x,z]
proof
A4: for x,y being object st P[x,y] & P[y,x] holds x = y
proof let x,y be object;
reconsider x,y as set by TARSKI:1;
P[x,y] & P[y,x] implies x = y by A2;
hence thesis;
end;
A5: for x,y,z being object st P[x,y] & P[y,z] holds P[x,z]
proof let x,y,z be object;
reconsider x,y,z as set by TARSKI:1;
P[x,y] & P[y,z] implies P[x,z] by A3;
hence thesis;
end;
consider x being object such that
A6: x in X() and
A7: for y being object st y in X() & y <> x holds not P[y,x]
from FinRegularity(A1,A4,A5);
reconsider x as set by TARSKI:1;
take x;
thus thesis by A6,A7;
end;