:: Countable Sets and Hessenberg's Theorem
:: by Grzegorz Bancerek
::
:: Received September 5, 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 NUMBERS, XBOOLE_0, NAT_1, ORDINAL1, CARD_1, FUNCT_1, FINSET_1,
CARD_3, REAL_1, NEWTON, ARYTM_3, RELAT_1, XXREAL_0, SUBSET_1, ZFMISC_1,
MCART_1, TARSKI, CARD_2, FINSEQ_2, FINSEQ_1, ORDINAL4, PARTFUN1, FUNCT_4,
RECDEF_2;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, CARD_1, NUMBERS,
XXREAL_0, XCMPLX_0, XREAL_0, NAT_1, NAT_D, RELAT_1, FUNCT_1, FINSEQ_1,
FINSET_1, WELLORD2, XTUPLE_0, MCART_1, DOMAIN_1, CARD_2, FINSEQ_2,
RELSET_1, FUNCT_2, BINOP_1, FUNCT_4, PARTFUN1, NEWTON, CARD_3;
constructors PARTFUN1, WELLORD2, BINOP_1, DOMAIN_1, FUNCOP_1, FUNCT_4,
ORDINAL3, XXREAL_0, NAT_1, NAT_D, MEMBERED, CARD_2, CARD_3, NEWTON,
FINSUB_1, RELSET_1, FINSEQ_2, XTUPLE_0;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FINSET_1,
XXREAL_0, NAT_1, CARD_1, FINSEQ_1, FINSEQ_2, CARD_3, XCMPLX_0, RELSET_1,
XTUPLE_0, NEWTON, XREAL_0;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
definitions TARSKI, FUNCT_1, WELLORD2, RELAT_1, XBOOLE_0, CARD_3;
equalities BINOP_1, CARD_3, XTUPLE_0, ORDINAL1;
expansions TARSKI, FUNCT_1, WELLORD2, XBOOLE_0, CARD_3;
theorems TARSKI, ZFMISC_1, NAT_1, ORDINAL1, ORDINAL3, WELLORD2, FUNCT_1,
FUNCT_2, FUNCT_4, PARTFUN1, MCART_1, CARD_3, ORDERS_1, CARD_1, CARD_2,
NEWTON, FINSEQ_1, FINSEQ_2, RELAT_1, XBOOLE_0, XBOOLE_1, XCMPLX_1,
XREAL_1, XXREAL_0, NAT_D, XTUPLE_0;
schemes NAT_1, FUNCT_1, XBOOLE_0, BINOP_1, CLASSES1;
begin
reserve X,Y,Z,x,y,y1,y2 for set,
D for non empty set,
k,n,n1,n2,m2,m1 for Nat,
L,K,M,N for Cardinal,
f,g for Function;
theorem
X is finite implies X is countable;
theorem
omega is countable;
reserve r for Real;
theorem Th3:
r <> 0 or n = 0 iff r|^n <> 0
proof
defpred P[Nat] means r <> 0 or $1 = 0 iff r|^$1 <> 0;
A1: P[k] implies P[k+1]
proof
A2: r|^(k+1) = r|^k*r by NEWTON:6;
assume P[k];
hence thesis by A2;
end;
A3: P[0] by NEWTON:4;
P[k] from NAT_1:sch 2(A3,A1);
hence thesis;
end;
Lm1: (2|^n1)*(2*m1+1) = (2|^n2)*(2*m2+1) implies n1 <= n2
proof
assume
A1: (2|^n1)*(2*m1+1) = (2|^n2)*(2*m2+1);
assume
A2: n1 > n2;
then consider n being Nat such that
A3: n1 = n2+n by NAT_1:10;
n <> 0 by A2,A3;
then consider k being Nat such that
A4: n = k+1 by NAT_1:6;
A5: 2|^n2 <> 0 by Th3;
reconsider k as Element of NAT by ORDINAL1:def 12;
2|^n1 = (2|^n2)*(2|^(k+1)) by A3,A4,NEWTON:8;
then (2|^n1)*(2*m1+1) = 2|^n2*(2|^(k+1)*(2*m1+1));
then 2|^(k+1)*(2*m1+1) = 2*m2+1 by A1,A5,XCMPLX_1:5;
then 2*m2+1 = 2|^k*(2|^1)*(2*m1+1) by NEWTON:8
.= 2*(2|^k)*(2*m1+1)
.= 2*((2|^k)*(2*m1+1));
then
A6: 2 divides 2*m2+1 by NAT_D:def 3;
2 divides 2*m2 by NAT_D:def 3;
hence contradiction by A6,NAT_D:7,10;
end;
theorem Th4:
(2|^n1)*(2*m1+1) = (2|^n2)*(2*m2+1) implies n1 = n2 & m1 = m2
proof
A1: 2|^n1 <> 0 by Th3;
assume
A2: (2|^n1)*(2*m1+1) = (2|^n2)*(2*m2+1);
then n1 <= n2 & n2 <= n1 by Lm1;
hence n1 = n2 by XXREAL_0:1;
then 2*m1+1 = 2*m2+1 by A2,A1,XCMPLX_1:5;
hence thesis;
end;
Lm2: x in [:NAT,NAT:] implies ex n1,n2 being Element of NAT st x = [n1,n2]
proof
assume
A1: x in [:NAT,NAT:];
then reconsider n1 = x`1, n2 = x`2 as Element of NAT by MCART_1:10;
take n1,n2;
thus thesis by A1,MCART_1:21;
end;
theorem Th5:
[:NAT,NAT:],NAT are_equipotent & card NAT = card [:NAT,NAT:]
proof
[:NAT,{0}:] c= [:NAT,NAT:] by ZFMISC_1:95;
then card [:NAT,{0}:] c= card [:NAT,NAT:] by CARD_1:11;
then
A1: card NAT c= card [:NAT,NAT:] by CARD_1:69;
deffunc f(Element of NAT,Element of NAT) = (2|^$1)*(2*$2+1);
consider f being Function of [:NAT,NAT:],NAT such that
A2: for n,m being Element of NAT holds f.(n,m) = f(n,m) from BINOP_1:sch
4;
A3: f is one-to-one
proof
let x,y be object;
assume x in dom f;
then consider n1,m1 being Element of NAT such that
A4: x = [n1,m1] by Lm2;
assume y in dom f;
then consider n2,m2 being Element of NAT such that
A5: y = [n2,m2] by Lm2;
assume
A6: f.x = f.y;
A7: (2|^n1)*(2*m1+1) = f.(n1,m1) by A2
.= f.(n2,m2) by A4,A5,A6
.= (2|^n2)*(2*m2+1) by A2;
then n1 = n2 by Th4;
hence thesis by A4,A5,A7,Th4;
end;
dom f = [:NAT,NAT:] & rng f c= NAT by FUNCT_2:def 1;
then card [:NAT,NAT:] c= card NAT by A3,CARD_1:10;
then card NAT = card [:NAT,NAT:] by A1;
hence thesis by CARD_1:5;
end;
theorem Th6:
(omega)*`(omega) = omega by Th5,CARD_2:def 2;
theorem Th7:
X is countable & Y is countable implies [:X,Y:] is countable
proof
assume card X c= omega & card Y c= omega;
then [:card X,card Y:] c= [:omega,omega:] by ZFMISC_1:96;
then card [:card X,card Y:] c= card [:omega,omega:] by CARD_1:11;
then card [:card X,card Y:] c= (omega)*`omega by CARD_2:def 2;
hence card [:X,Y:] c= omega by Th6,CARD_2:7;
end;
theorem Th8:
1-tuples_on D,D are_equipotent & card (1-tuples_on D) = card D
proof
deffunc f(object) = <*$1*>;
consider f such that
A1: dom f = D &
for x being object st x in D holds f.x = f(x) from FUNCT_1:sch 3;
D,1-tuples_on D are_equipotent
proof
take f;
thus f is one-to-one
proof
let x,y be object;
assume x in dom f & y in dom f;
then
A2: f.x = <*x*> & f.y = <*y*> by A1;
<*x*>.1 = x;
hence thesis by A2,FINSEQ_1:def 8;
end;
thus dom f = D by A1;
thus rng f c= 1-tuples_on D
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;
reconsider y as Element of D by A1,A3;
x = <*y*> by A1,A4;
then x in the set of all <*d*> where d is Element of D ;
hence thesis by FINSEQ_2:96;
end;
let x be object;
assume x in 1-tuples_on D;
then reconsider y = x as Element of 1-tuples_on D;
consider z being Element of D such that
A5: y = <*z*> by FINSEQ_2:97;
x = f.z by A1,A5;
hence thesis by A1,FUNCT_1:def 3;
end;
hence thesis by CARD_1:5;
end;
reserve p,q for FinSequence,
k,m,n,n1,n2,n3 for Nat;
theorem Th9:
[:n-tuples_on D, m-tuples_on D:],(n+m)-tuples_on D
are_equipotent & card [:n-tuples_on D, m-tuples_on D:] = card ((n+m)-tuples_on
D)
proof
defpred P[object,object] means
ex p be Element of n-tuples_on D,q be Element of m
-tuples_on D st $1 = [p,q] & $2 = p^q;
set A = [:n-tuples_on D, m-tuples_on D:];
set B = (n+m)-tuples_on D;
A1: for x being object st x in A ex y being object st P[x,y]
proof
let x be object;
assume
A2: x in A;
then reconsider p = x`1 as Element of n-tuples_on D by MCART_1:10;
reconsider q = x`2 as Element of m-tuples_on D by A2,MCART_1:10;
reconsider y = p^q as set;
take y;
x = [x`1,x`2] by A2,MCART_1:21;
hence thesis;
end;
consider f such that
A3: dom f = A &
for x being object st x in A holds P[x,f.x] from CLASSES1:sch 1(A1);
thus [:n-tuples_on D, m-tuples_on D:],(n+m)-tuples_on D are_equipotent
proof
take f;
thus f is one-to-one
proof
let x,y be object;
assume x in dom f;
then consider
p1 be Element of n-tuples_on D, q1 be Element of m-tuples_on D
such that
A4: x = [p1,q1] and
A5: f.x = p1^q1 by A3;
assume y in dom f;
then consider
p2 be Element of n-tuples_on D, q2 be Element of m-tuples_on D
such that
A6: y = [p2,q2] and
A7: f.y = p2^q2 by A3;
assume
A8: f.x = f.y;
A9: len p1 = n & len p2 = n by CARD_1:def 7;
then consider p such that
A10: p1^p = p2 by A5,A7,A8,FINSEQ_1:47;
consider q such that
A11: p2^q = p1 by A5,A7,A8,A9,FINSEQ_1:47;
len p1+0 = len(p1^p)+len q by A10,A11,FINSEQ_1:22
.= len p1+len p+len q by FINSEQ_1:22
.= len p1+(len p+len q);
then p = {};
then p1 = p2 by A10,FINSEQ_1:34;
hence thesis by A4,A5,A6,A7,A8,FINSEQ_1:33;
end;
thus dom f = A by A3;
thus rng f c= B
proof
let x be object;
assume x in rng f;
then consider y being object such that
A12: y in dom f & x = f.y by FUNCT_1:def 3;
ex p being Element of n-tuples_on D, q being Element of m-tuples_on
D st y = [p,q] & x = p^q by A3,A12;
then x is Tuple of n+m, D;
then x is Element of (n+m)-tuples_on D by FINSEQ_2:131;
hence thesis;
end;
let x be object;
assume x in B;
then reconsider x as Element of B;
consider p being Element of n-tuples_on D, q being Element of m-tuples_on
D such that
A13: x = p^q by FINSEQ_2:106;
consider p1 being Element of n-tuples_on D, q1 being Element of m
-tuples_on D such that
A14: [p,q] = [p1,q1] and
A15: f.[p,q] = p1^q1 by A3;
p1 = p & q1 = q by A14,XTUPLE_0:1;
hence thesis by A3,A13,A15,FUNCT_1:def 3;
end;
hence thesis by CARD_1:5;
end;
theorem Th10:
D is countable implies n-tuples_on D is countable
proof
defpred P[Nat] means $1-tuples_on D is countable;
assume card D c= omega;
then card (1-tuples_on D) c= omega by Th8;
then
A1: 1-tuples_on D is countable;
A2: for k being Nat holds P[k] implies P[k+1]
proof
let k be Nat;
assume P[k];
then [:k-tuples_on D, 1-tuples_on D:] is countable by A1,Th7;
then
A3: card [:k-tuples_on D, 1-tuples_on D:] c= omega;
card [:k-tuples_on D, 1-tuples_on D:] = card ((k+1)-tuples_on D) by
Th9;
hence thesis by A3,CARD_3:def 14;
end;
{ <*>D } is countable;
then
A4: P[0] by FINSEQ_2:94;
for k being Nat holds P[k] from NAT_1:sch 2(A4,A2);
hence thesis;
end;
theorem Th11:
for f st dom f is countable & for x st x in dom f holds f.x is
countable holds Union f is countable
proof
let f such that
A1: card dom f c= omega and
A2: for x st x in dom f holds f.x is countable;
for x being object st x in dom f holds card (f.x) c= omega
by A2,CARD_3:def 14;
hence card Union f c= omega by A1,Th6,CARD_2:86;
end;
theorem
(X is countable & for Y st Y in X holds Y is countable) implies union
X is countable
proof
assume that
A1: card X c= omega and
A2: for Y st Y in X holds Y is countable;
for Y st Y in X holds card Y c= omega by A2,CARD_3:def 14;
hence card union X c= omega by A1,Th6,CARD_2:87;
end;
theorem
D is countable implies D* is countable
proof
defpred P[object,object] means ex n st $1 = n & $2 = n-tuples_on D;
A1: for x being object st x in NAT ex y being object st P[x,y]
proof
let x be object;
assume x in NAT;
then reconsider n = x as Element of NAT;
reconsider y = n-tuples_on D as set;
take y,n;
thus thesis;
end;
consider f such that
A2: dom f = NAT &
for x being object st x in NAT holds P[x,f.x] from CLASSES1:sch 1(
A1);
A3: D* = union the set of all k-tuples_on D by FINSEQ_2:108;
A4: Union f = D*
proof
thus Union f c= D*
proof
let x be object;
assume x in Union f;
then consider X such that
A5: x in X and
A6: X in rng f by TARSKI:def 4;
consider y being object such that
A7: y in dom f and
A8: X = f.y by A6,FUNCT_1:def 3;
reconsider y as Element of NAT by A2,A7;
ex n st y = n & X = n-tuples_on D by A2,A8;
then X in the set of all k-tuples_on D ;
hence thesis by A3,A5,TARSKI:def 4;
end;
let x be object;
assume x in D*;
then consider X such that
A9: x in X & X in the set of all k-tuples_on D by A3,TARSKI:def 4;
consider n such that
A10: X = n-tuples_on D by A9;
A11: n in NAT by ORDINAL1:def 12;
then ex k st n = k & f.n = k-tuples_on D by A2;
then X in rng f by A2,A10,FUNCT_1:def 3,A11;
hence thesis by A9,TARSKI:def 4;
end;
assume
A12: D is countable;
now
let x;
assume x in dom f;
then ex n st x = n & f.x = n-tuples_on D by A2;
hence f.x is countable by A12,Th10;
end;
hence thesis by A2,A4,Th11;
end;
theorem
omega c= card (D*)
proof
defpred P[object,object] means ex p st $1 = p & $2 = len p;
A1: {} in D* & len {} = 0 by FINSEQ_1:49;
A2: for x being object st x in D* ex y being object st P[x,y]
proof
let x be object;
assume x in D*;
then reconsider p = x as Element of (D*);
reconsider p as FinSequence;
reconsider y = len p as set;
take y,p;
thus thesis;
end;
consider f such that
A3: dom f = D* &
for x being object st x in D* holds P[x,f.x] from CLASSES1:sch 1(A2);
defpred P[Nat] means $1 in f.:(D*);
A4: for n being Nat holds P[n] implies P[n+1]
proof
set y = the Element of D;
let n be Nat;
assume n in f.:(D*);
then consider x being object such that
A5: x in dom f and
A6: x in D* and
A7: n = f.x by FUNCT_1:def 6;
consider p such that
A8: x = p and
A9: n = len p by A3,A5,A7;
reconsider p as FinSequence of D by A6,A8,FINSEQ_1:def 11;
A10: len (p^<*y*>) = n+len <*y*> by A9,FINSEQ_1:22
.= n+1 by FINSEQ_1:40;
A11: p^<*y*> in D* by FINSEQ_1:def 11;
then ex q being FinSequence st p^<*y*> = q & f.(p^<*y*>) = len q by A3;
hence thesis by A3,A11,A10,FUNCT_1:def 6;
end;
ex p st {} = p & f.{} = len p by A3,FINSEQ_1:49;
then
A12: P[0] by A3,A1,FUNCT_1:def 6;
A13: for n being Nat holds P[n] from NAT_1:sch 2(A12,A4);
NAT c= f.:(D*)
by A13;
hence thesis by CARD_1:47,66;
end;
scheme
FraenCoun1 { f(object)->set, P[set] } :
{ f(n) : P[n] } is countable;
consider f such that
A1: dom f = NAT &
for x being object st x in NAT holds f.x = f(x) from FUNCT_1:sch 3;
{ f(n) : P[n] } c= rng f
proof
let x be object;
assume x in { f(n) : P[n] };
then consider n such that
A2: x = f(n) and
P[n];
A3: n in NAT by ORDINAL1:def 12;
then f.n = x by A1,A2;
hence thesis by A1,FUNCT_1:def 3,A3;
end;
hence thesis by A1,CARD_3:93;
end;
scheme
FraenCoun2 { f(object,object)->set, P[set,set] } :
{ f(n1,n2) : P[n1,n2] } is
countable proof
consider N being Function such that
N is one-to-one and
A1: dom N = NAT and
A2: rng N = [:NAT,NAT:] by Th5,WELLORD2:def 4;
deffunc g(object) = f((N.$1)`1,(N.$1)`2);
consider f such that
A3: dom f = NAT &
for x being object st x in NAT holds f.x = g(x) from FUNCT_1:sch 3;
{ f(n1,n2) : P[n1,n2] } c= rng f
proof
let x be object;
assume x in { f(n1,n2) : P[n1,n2] };
then consider n1,n2 such that
A4: x = f(n1,n2) and
P[n1,n2];
n1 in NAT & n2 in NAT by ORDINAL1:def 12;
then [n1,n2] in [:NAT,NAT:] by ZFMISC_1:87;
then consider y being object such that
A5: y in dom N and
A6: [n1,n2] = N.y by A2,FUNCT_1:def 3;
[n1,n2]`1 = n1 & [n1,n2]`2 = n2;
then x = f.y by A1,A3,A4,A5,A6;
hence thesis by A1,A3,A5,FUNCT_1:def 3;
end;
hence thesis by A3,CARD_3:93;
end;
scheme
FraenCoun3 { f(object,object,object)->set, P[set,set,set] } :
{ f(n1,n2,n3) : P[n1,n2
,n3] } is countable proof
[:NAT,NAT:],[:[:NAT,NAT:],NAT:] are_equipotent by Th5,CARD_2:8;
then
A1: NAT,[:[:NAT,NAT:],NAT:] are_equipotent by Th5,WELLORD2:15;
[:[:NAT,NAT:],NAT:] = [:NAT,NAT,NAT:] by ZFMISC_1:def 3;
then consider N being Function such that
N is one-to-one and
A2: dom N = NAT and
A3: rng N = [:NAT,NAT,NAT:] by A1;
deffunc g(object) = f((N.$1)`1`1,(N.$1)`1`2,(N.$1)`2);
consider f such that
A4: dom f = NAT &
for x being object st x in NAT holds f.x = g(x) from FUNCT_1:sch 3;
{ f(n1,n2,n3) : P[n1,n2,n3] } c= rng f
proof
let x be object;
assume x in { f(n1,n2,n3) : P[n1,n2,n3] };
then consider n1,n2,n3 such that
A5: x = f(n1,n2,n3) and
P[n1,n2,n3];
reconsider n1,n2,n3 as Element of NAT by ORDINAL1:def 12;
A6: [n1,n2,n3]`3_3 = n3 & [n1,n2,n3]`1_3 = [n1,n2,n3]`1`1;
consider y being object such that
A7: y in dom N and
A8: [n1,n2,n3] = N.y by A3,FUNCT_1:def 3;
[n1,n2,n3]`1_3 = n1 & [n1,n2,n3]`2_3 = n2;
then x = f.y by A2,A4,A5,A7,A8,A6;
hence thesis by A2,A4,A7,FUNCT_1:def 3;
end;
hence thesis by A4,CARD_3:93;
end;
reserve f,f1,f2 for Function,
X1,X2 for set;
::$N Hessenberg's theorem
theorem Th15:
not M is finite implies M*`M = M
proof
defpred P[object] means
ex f st f = $1 & f is one-to-one & dom f = [:rng f,rng
f:];
consider X such that
A1: for x being object holds x in X iff x in PFuncs([:M,M:],M) & P[x]
from XBOOLE_0:sch 1;
A2: x in X implies x is Function
proof
assume x in X;
then ex f st f = x & f is one-to-one & dom f = [:rng f,rng f:] by A1;
hence thesis;
end;
A3: for Z st Z <> {} & Z c= X & Z is c=-linear holds union Z in X
proof
let Z;
assume that
Z <> {} and
A4: Z c= X and
A5: Z is c=-linear;
union Z is Relation-like Function-like
proof
set F = union Z;
thus for x being object st x in F ex y1,y2 being object st [y1,y2] = x
proof
let x be object;
assume x in F;
then consider Y such that
A6: x in Y and
A7: Y in Z by TARSKI:def 4;
reconsider f = Y as Function by A2,A4,A7;
for x being object st x in f
ex y1,y2 being object st [y1,y2] = x by RELAT_1:def 1;
hence thesis by A6;
end;
let x,y1,y2 be object;
assume [x,y1] in F;
then consider X1 such that
A8: [x,y1] in X1 and
A9: X1 in Z by TARSKI:def 4;
assume [x,y2] in F;
then consider X2 such that
A10: [x,y2] in X2 and
A11: X2 in Z by TARSKI:def 4;
reconsider f1 = X1, f2 = X2 as Function by A2,A4,A9,A11;
X1,X2 are_c=-comparable by A5,A9,A11,ORDINAL1:def 8;
then X1 c= X2 or X2 c= X1;
then
[x,y2] in X1 &
(for x,y1,y2 being object st [x,y1] in f1 & [x,y2] in f1 holds y1
= y2) or [x,y1] in X2 &
for x,y1,y2 being object st [x,y1] in f2 & [x,y2] in f2 holds y1 =
y2 by A8,A10,FUNCT_1:def 1;
hence thesis by A8,A10;
end;
then reconsider f = union Z as Function;
A12: f is one-to-one
proof
let x1,x2 be object;
assume that
A13: x1 in dom f and
A14: x2 in dom f;
[x1,f.x1] in f by A13,FUNCT_1:1;
then consider X1 such that
A15: [x1,f.x1] in X1 and
A16: X1 in Z by TARSKI:def 4;
[x2,f.x2] in f by A14,FUNCT_1:1;
then consider X2 such that
A17: [x2,f.x2] in X2 and
A18: X2 in Z by TARSKI:def 4;
consider f2 such that
A19: f2 = X2 and
A20: f2 is one-to-one and
dom f2 = [:rng f2,rng f2:] by A1,A4,A18;
consider f1 such that
A21: f1 = X1 and
A22: f1 is one-to-one and
dom f1 = [:rng f1,rng f1:] by A1,A4,A16;
X1, X2 are_c=-comparable by A5,A16,A18,ORDINAL1:def 8;
then X1 c= X2 or X2 c= X1;
then x1 in dom f1 & x2 in dom f1 & f.x1 = f1.x1 & f.x2 = f1.x2 or x1 in
dom f2 & x2 in dom f2 & f.x1 = f2.x1 & f.x2 = f2.x2 by A15,A17,A21,A19,
FUNCT_1:1;
hence thesis by A22,A20;
end;
A23: dom f = [:rng f,rng f:]
proof
thus dom f c= [:rng f,rng f:]
proof
let x be object;
assume x in dom f;
then [x,f.x] in f by FUNCT_1:def 2;
then consider Y such that
A24: [x,f.x] in Y and
A25: Y in Z by TARSKI:def 4;
consider g being Function such that
A26: g = Y and
g is one-to-one and
A27: dom g = [:rng g,rng g:] by A1,A4,A25;
g c= f by A25,A26,ZFMISC_1:74;
then rng g c= rng f by RELAT_1:11;
then
A28: dom g c= [:rng f,rng f:] by A27,ZFMISC_1:96;
x in dom g by A24,A26,FUNCT_1:1;
hence thesis by A28;
end;
let x1,x2 be object;
assume
A29: [x1,x2] in [:rng f,rng f:];
[x1,x2]`1 in rng f by A29,MCART_1:10;
then consider y1 being object such that
A30: y1 in dom f & [x1,x2]`1 = f.y1 by FUNCT_1:def 3;
[x1,x2] `2 in rng f by A29,MCART_1:10;
then consider y2 being object such that
A31: y2 in dom f & [x1,x2]`2 = f.y2 by FUNCT_1:def 3;
[y2,[x1,x2]`2] in f by A31,FUNCT_1:1;
then consider X2 such that
A32: [y2,[x1,x2]`2] in X2 and
A33: X2 in Z by TARSKI:def 4;
consider f2 such that
A34: f2 = X2 and
f2 is one-to-one and
A35: dom f2 = [:rng f2,rng f2:] by A1,A4,A33;
f2 c= f by A33,A34,ZFMISC_1:74;
then
A36: dom f2 c= dom f by RELAT_1:11;
[y1,[x1,x2]`1] in f by A30,FUNCT_1:1;
then consider X1 such that
A37: [y1,[x1,x2]`1] in X1 and
A38: X1 in Z by TARSKI:def 4;
consider f1 such that
A39: f1 = X1 and
f1 is one-to-one and
A40: dom f1 = [:rng f1,rng f1:] by A1,A4,A38;
X1, X2 are_c=-comparable by A5,A38,A33,ORDINAL1:def 8;
then X1 c= X2 or X2 c= X1;
then y1 in dom f1 & y2 in dom f1 & f1.y1 = [x1,x2]`1 & f1.y2 = [x1,x2]
`2 or y1 in dom f2 & y2 in dom f2 & f2.y1 = [x1,x2]`1 & f2.y2 = [x1,x2]`2 by
A37,A32,A39,A34,FUNCT_1:1;
then [x1,x2]`1 in rng f1 & [x1,x2]`2 in rng f1 or [x1,x2]`1 in rng f2 &
[x1,x2]`2 in rng f2 by FUNCT_1:def 3;
then
A41: [x1,x2] in dom f1 or [x1,x2] in dom f2 by A40,A35,ZFMISC_1:87;
f1 c= f by A38,A39,ZFMISC_1:74;
then dom f1 c= dom f by RELAT_1:11;
hence thesis by A41,A36;
end;
A42: rng f c= M
proof
let y be object;
assume y in rng f;
then consider x being object such that
A43: x in dom f & y = f.x by FUNCT_1:def 3;
[x,y] in union Z by A43,FUNCT_1:def 2;
then consider Y such that
A44: [x,y] in Y and
A45: Y in Z by TARSKI:def 4;
Y in PFuncs([:M,M:],M) by A1,A4,A45;
then consider g being Function such that
A46: Y = g and
dom g c= [:M,M:] and
A47: rng g c= M by PARTFUN1:def 3;
x in dom g & g.x = y by A44,A46,FUNCT_1:1;
then y in rng g by FUNCT_1:def 3;
hence thesis by A47;
end;
dom f c= [:M,M:]
proof
let x be object;
assume x in dom f;
then [x,f.x] in union Z by FUNCT_1:def 2;
then consider Y such that
A48: [x,f.x] in Y and
A49: Y in Z by TARSKI:def 4;
Y in PFuncs([:M,M:],M) by A1,A4,A49;
then consider g being Function such that
A50: Y = g and
A51: dom g c= [:M,M:] and
rng g c= M by PARTFUN1:def 3;
x in dom g by A48,A50,FUNCT_1:1;
hence thesis by A51;
end;
then f in PFuncs([:M,M:],M) by A42,PARTFUN1:def 3;
hence thesis by A1,A12,A23;
end;
consider f such that
A52: f is one-to-one and
A53: dom f = [:omega,omega:] & rng f = omega by Th5;
assume
A54: not M is finite;
then not M in omega;
then
A55: omega c= M by CARD_1:4;
then [:omega,omega:] c= [:M,M:] by ZFMISC_1:96;
then f in PFuncs([:M,M:],M) by A53,A55,PARTFUN1:def 3;
then X <> {} by A1,A52,A53;
then consider Y such that
A56: Y in X and
A57: for Z st Z in X & Z <> Y holds not Y c= Z by A3,ORDERS_1:67;
consider f such that
A58: f = Y and
A59: f is one-to-one and
A60: dom f = [:rng f,rng f:] by A1,A56;
set A = rng f;
A61: [:A,A:],A are_equipotent by A59,A60;
Y in PFuncs([:M,M:],M) by A1,A56;
then
A62: ex f st Y = f & dom f c= [:M,M:] & rng f c= M by PARTFUN1:def 3;
set N = card A;
A63: card M = M;
then
A64: N c= M by A58,A62,CARD_1:11;
A65: now
(omega \ A) misses A by XBOOLE_1:79;
then
A66: (omega \ A) /\ A = {};
then [:(omega \ A) /\ A,A /\ (omega \ A):] = {} by ZFMISC_1:90;
then
A67: [:omega \ A,A:] /\ [:A,omega \ A:] = {} by ZFMISC_1:100;
[:(omega \ A) /\ (omega \ A),(omega \ A) /\ A:] = {} by A66,ZFMISC_1:90;
then [:omega \ A,omega \ A:] /\ [:omega \ A,A:] = {} by ZFMISC_1:100;
then
A68: [:omega \ A,omega \ A:] misses [:omega \ A,A:];
[:A /\ A,(omega \ A) /\ A:] = {} by A66,ZFMISC_1:90;
then
A69: [:A,omega \ A:] /\ [:A,A:] = {} by ZFMISC_1:100;
[:(omega \ A) /\ A,A /\ A:] = {} by A66,ZFMISC_1:90;
then
A70: {} \/ {} = {} & [:omega \ A,A:] /\ [:A,A:] = {} by ZFMISC_1:100;
[:(omega \ A) /\ A,(omega \ A) /\ A:] = {} by A66,ZFMISC_1:90;
then [:omega \ A,omega \ A:] /\ [:A,A:] = {} by ZFMISC_1:100;
then
A71: ([:omega \ A,omega \ A:] \/ [:omega \ A,A:]) /\ [:A,A:] = {} by A70,
XBOOLE_1:23;
A72: omega c= omega +` N & omega +` omega = omega by CARD_2:75,94;
assume
A73: A is finite;
then N in omega by CARD_3:42;
then omega +` N c= omega +` omega by CARD_2:83;
then
A74: omega = omega +` N by A72;
N = card card A;
then (omega)*`N c= omega by A73,CARD_2:89;
then
A75: omega +` (omega)*`N = omega by CARD_2:76;
A76: omega = card (omega \ A) by A73,A74,CARD_2:98,CARD_3:42;
[:(omega \ A) /\ A,(omega \ A) /\ (omega \ A):] = {} by A66,ZFMISC_1:90;
then [:omega \ A,omega \ A:] /\ [:A,omega \ A:] = {} by ZFMISC_1:100;
then ([:omega \ A,omega \ A:] \/ [:omega \ A,A:]) /\ [:A,omega \ A:] = {}
\/ {} by A67,XBOOLE_1:23
.= {};
then ([:omega \ A,omega \ A:] \/ [:omega \ A,A:]) misses [:A,omega \ A:];
then card ([:omega \ A,omega \ A:] \/ [:omega \ A,A:] \/ [:A,omega \ A:])
= card ([:omega \ A,omega \ A:] \/ [:omega \ A,A:]) +` card [:A,omega \ A:] by
CARD_2:35
.= card [:omega \ A,omega \ A:] +` card [:omega \ A,A:] +` card [:A,
omega \ A:] by A68,CARD_2:35
.= card [:omega \ A,omega \ A:] +` card [:omega,N:] +` card [:A,omega
\ A:] by A76,CARD_2:7
.= card [:omega,omega:] +` card [:omega,N:] +` card [:A,omega \ A:] by
A76,CARD_2:7
.= omega +` card [:omega,N:] +` card [:N,omega:] by A76,Th5,CARD_2:7
.= omega +` (omega)*`N +` card [:N,omega:] by CARD_2:def 2
.= omega +` (omega)*`N +` N*`(omega) by CARD_2:def 2;
then [:omega \ A,omega \ A:] \/ [:omega \ A,A:] \/ [:A,omega \ A:],omega
\ A are_equipotent by A76,A75,CARD_1:5;
then consider g being Function such that
A77: g is one-to-one and
A78: dom g = [:omega \ A,omega \ A:] \/ [:omega \ A,A:] \/ [:A,omega \ A:] and
A79: rng g = omega \ A;
A80: dom (g+*f) = dom g \/ dom f by FUNCT_4:def 1;
then
A81: dom (g+*f) = [:omega \ A,(omega \ A) \/ A:] \/ [:A,omega \ A:] \/ [:
A,A:] by A60,A78,ZFMISC_1:97
.= [:omega \ A,(omega \ A) \/ A:] \/ ([:A,omega \ A:] \/ [:A,A:]) by
XBOOLE_1:4
.= [:omega \ A,(omega \ A) \/ A:] \/ [:A,(omega \ A) \/ A:] by
ZFMISC_1:97
.= [:(omega \ A) \/ A,(omega \ A) \/ A:] by ZFMISC_1:97
.= [:omega \/ A,(omega \ A) \/ A:] by XBOOLE_1:39
.= [:omega \/ A,omega \/ A:] by XBOOLE_1:39;
{} \/ {} = {};
then dom g /\ dom f = {} by A60,A78,A71,A69,XBOOLE_1:23;
then
A82: dom g misses dom f;
then g c= g+*f by FUNCT_4:32;
then rng f c= rng (g+*f) & rng g c= rng (g+*f) by FUNCT_4:18,RELAT_1:11;
then rng (g+*f) c= rng g \/ rng f & rng g \/ rng f c= rng (g+*f) by
FUNCT_4:17,XBOOLE_1:8;
then
A83: rng (g+*f) = rng g \/ rng f
.= omega \/ A by A79,XBOOLE_1:39;
A84: g+*f is one-to-one
proof
rng f misses rng g by A79,XBOOLE_1:79;
then
A85: rng f /\ rng g = {};
let x,y be object;
assume that
A86: x in dom (g+*f) and
A87: y in dom (g+*f);
A88: y in dom g or y in dom f by A80,A87,XBOOLE_0:def 3;
x in dom f or x in dom g by A80,A86,XBOOLE_0:def 3;
then (g+*f).x = f.x & (g+*f).y = f.y & (f.x = f.y implies x = y) or (g
+*f).x = g.x & (g+*f).y = g.y & (g.x = g.y implies x = y) or (g+*f).x = f.x & (
g+*f).y = g.y & f.x in rng f & g.y in rng g or (g+*f).x = g.x & (g+*f).y = f.y
& g.x in rng g & f.y in rng f by A59,A77,A82,A88,FUNCT_1:def 3,FUNCT_4:13
,16;
hence thesis by A85,XBOOLE_0:def 4;
end;
set x = the Element of omega \ A;
omega \ A <> {} by A73,A74,CARD_1:68,CARD_3:42;
then
A89: x in omega & not x in A by XBOOLE_0:def 5;
A90: omega \/ A c= M by A55,A58,A62,XBOOLE_1:8;
then [:omega \/ A,omega \/ A:] c= [:M,M:] by ZFMISC_1:96;
then g+*f in PFuncs([:M,M:],M) by A83,A81,A90,PARTFUN1:def 3;
then g+*f in X by A1,A83,A81,A84;
then g+*f = f by A57,A58,FUNCT_4:25;
hence contradiction by A83,A89,XBOOLE_0:def 3;
end;
A91: now
N*`N = card [:N,N:] by CARD_2:def 2;
then
A92: N*`N = card [:A,A:] by CARD_2:7;
[:A,A:],A are_equipotent by A59,A60;
then
A93: N*`N = N by A92,CARD_1:5;
assume N <> M;
then
A94: N in M by A64,CARD_1:3;
M+`N = M by A54,A64,CARD_2:76;
then card (M \ A) = M by A63,A94,CARD_2:98;
then consider h being Function such that
A95: h is one-to-one & dom h = A and
A96: rng h c= M \ A by A64,CARD_1:10;
set B = rng h;
A,B are_equipotent by A95;
then
A97: N = card B by CARD_1:5;
A misses (M \ A) & A /\ B c= A /\ (M \ A) by A96,XBOOLE_1:26,79;
then A /\ B c= {};
then A /\ B = {};
then
A98: A misses B;
(A \/ B) \ A = B \ A by XBOOLE_1:40
.= B by A98,XBOOLE_1:83;
then
A99: [:B,B:] c= [:(A \/ B) \ A,A \/ B:] by ZFMISC_1:96;
[:(A \/ B) \ A,A \/ B:] c= [:(A \/ B) \ A,A \/ B:] \/ [:A \/ B,(A \/
B ) \ A :] & [:A \/ B,A \/ B:] \ [:A,A:] = [:(A \/ B) \ A,A \/ B:] \/ [:A \/ B,
(A \/ B ) \ A:] by XBOOLE_1:7,ZFMISC_1:103;
then
A100: [:B,B:] c= [:A \/ B,A \/ B:] \ [:A,A:] by A99;
N+`N = N by A65,CARD_2:75;
then card (A \/ B) = N by A97,A98,CARD_2:35;
then card [:A \/ B,A \/ B:] = card [:N,N:] by CARD_2:7
.= N by A93,CARD_2:def 2;
then
A101: card ([:A \/ B,A \/ B:] \ [:A,A:]) c= N by CARD_1:11;
N = card [:N,N:] by A93,CARD_2:def 2;
then N = card [:B,B:] by A97,CARD_2:7;
then N c= card ([:A \/ B,A \/ B:] \ [:A,A:]) by A100,CARD_1:11;
then card ([:A \/ B,A \/ B:] \ [:A,A:]) = N by A101;
then [:A \/ B,A \/ B:] \ [:A,A:],B are_equipotent by A97,CARD_1:5;
then consider g such that
A102: g is one-to-one and
A103: dom g = [:A \/ B,A \/ B:] \ [:A,A:] and
A104: rng g = B;
A105: dom (g+*f) = dom g \/ dom f by FUNCT_4:def 1;
then A c= A \/ B & dom (g+*f) = [:A \/ B,A \/ B:] \/ [:A,A:] by A60,A103,
XBOOLE_1:7,39;
then
A106: dom (g+*f) = [:A \/ B,A \/ B:] by XBOOLE_1:12,ZFMISC_1:96;
A107: ([:A \/ B,A \/ B:] \ [:A,A:]) misses [:rng f,rng f:] by XBOOLE_1:79;
A108: g+*f is one-to-one
proof
let x,y be object;
assume that
A109: x in dom (g+*f) and
A110: y in dom (g+*f);
A111: y in dom g or y in dom f by A105,A110,XBOOLE_0:def 3;
x in dom f or x in dom g by A105,A109,XBOOLE_0:def 3;
then
A112: (g+*f).x = f.x & (g+*f).y = f.y & (f.x = f.y implies x = y) or (g
+*f).x = g.x & (g+*f).y = g.y & (g.x = g.y implies x = y) or (g+*f).x = f.x & (
g+*f).y = g.y & f.x in rng f & g.y in rng g or (g+*f).x = g.x & (g+*f).y = f.y
& g.x in rng g & f.y in rng f by A59,A60,A102,A103,A107,A111,
FUNCT_1:def 3,FUNCT_4:13,16;
A misses (M \ A) & A /\ B c= A /\ (M \ A) by A96,XBOOLE_1:26,79;
then
A113: rng f /\ rng g c= {} by A104;
assume (g+*f).x = (g+*f).y;
hence thesis by A113,A112,XBOOLE_0:def 4;
end;
set x = the Element of B;
A114: B <> {} by A65,A97;
then x in M \ A by A96;
then
A115: not x in rng f by XBOOLE_0:def 5;
g c= g+*f by A60,A103,FUNCT_4:32,XBOOLE_1:79;
then rng f c= rng (g+*f) & rng g c= rng (g+*f) by FUNCT_4:18,RELAT_1:11;
then
A116: rng g \/ rng f c= rng(g+*f) by XBOOLE_1:8;
rng(g+*f) c= rng g \/ rng f by FUNCT_4:17;
then
A117: rng (g+*f) = rng g \/ rng f by A116;
B c= M by A96,XBOOLE_1:1;
then
A118: A \/ B c= M by A58,A62,XBOOLE_1:8;
then [:A \/ B,A \/ B:] c= [:M,M:] by ZFMISC_1:96;
then g+*f in PFuncs([:M,M:],M) by A104,A117,A106,A118,PARTFUN1:def 3;
then
A119: g+*f in X by A1,A104,A117,A106,A108;
x in rng (g+*f) by A104,A117,A114,XBOOLE_0:def 3;
hence contradiction by A57,A58,A119,A115,FUNCT_4:25;
end;
then M*`M = card [:N,N:] by CARD_2:def 2
.= card [:A,A:] by CARD_2:7;
hence thesis by A91,A61,CARD_1:5;
end;
theorem Th16:
not M is finite & 0 in N & (N c= M or N in M) implies M*`N = M & N*`M = M
proof
A1: 1*`M = M by CARD_2:21;
assume not M is finite;
then
A2: M*`M = M by Th15;
assume 0 in N;
then 1 c= N by CARD_2:68;
then
A3: 1*`M c= N*`M by CARD_2:90;
assume N c= M or N in M;
then N*`M c= M*`M by CARD_2:90;
hence thesis by A2,A3,A1;
end;
theorem Th17:
not M is finite & (N c= M or N in M) implies M*`N c= M & N*`M c= M
proof
assume not M is finite & (N c= M or N in M);
then M*`N = M or not 0 in N by Th16;
then M*`N c= M or N = 0 & M*`0 = 0 & 0 c= M
by CARD_2:20,ORDINAL3:8;
hence thesis;
end;
theorem
not X is finite implies [:X,X:],X are_equipotent & card [:X,X:] = card X
proof
assume not X is finite;
then (card X)*`(card X) = card X by Th15;
then card [:card X,card X:] = card X by CARD_2:def 2;
then card [:X,X:] = card X by CARD_2:7;
hence thesis by CARD_1:5;
end;
theorem
not X is finite & Y is finite & Y <> {} implies [:X,Y:],X
are_equipotent & card [:X,Y:] = card X
proof
assume that
A1: not X is finite and
A2: Y is finite & Y <> {};
card Y c= card X & 0 in card Y by A1,A2,ORDINAL3:8;
then (card X)*`(card Y) = card X by A1,Th16;
then card [:card X,card Y:] = card X by CARD_2:def 2;
then card [:X,Y:] = card X by CARD_2:7;
hence thesis by CARD_1:5;
end;
theorem
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;
assume that
A2: K in L and
A3: M in N and
A4: L c= N;
A5: now
assume
A6: N is finite;
then reconsider N as finite Cardinal;
reconsider L,M,K as finite Cardinal by A2,A3,A4,A6,CARD_3:92;
A7: card Segm N = N;
card Segm M = M;
then card M < card N by A3,A7,NAT_1:41;
then
A8: card K * card M <= card K * card N by XREAL_1:64;
A9: card Segm L = L;
A10: L*`N = card Segm(card L * card N) by CARD_2:39;
card Segm K = K;
then card K < card L by A2,A9,NAT_1:41;
then card K * card N < card L * card N by A3,XREAL_1:68;
then
A11: card K * card M < card L * card N by A8,XXREAL_0:2;
K*`M = card Segm(card K * card M) by CARD_2:39;
hence thesis by A10,A11,NAT_1:41;
end;
A12: 0 in L by A2,ORDINAL3:8;
now
assume
A13: not N is finite;
then
A14: L*`N = N by A4,A12,Th16;
A15: omega c= N by A13,CARD_3:85;
A16: now
assume K is finite & M is finite;
then reconsider K,M as finite Cardinal;
K*`M = card (card K * card M) by CARD_2:39
.= (card K * card M);
hence thesis by A14,A15;
end;
K c= M & (M is finite or not M is finite) or M c= K & (K is finite
or not K is finite);
then
K is finite & M is finite or K*`M c= M or K*`M c= K & K in N by A2,A4
,Th17;
hence thesis by A3,A14,A16,ORDINAL1:12;
end;
hence thesis by A5;
end;
L c= N or N c= L;
hence thesis by A1;
end;
theorem Th21:
not X is finite implies card X = (omega)*`card X
proof
assume
A1: not X is finite;
then omega c= card X by CARD_3:85;
hence thesis by A1,Th16;
end;
theorem
X <> {} & X is finite & not Y is finite implies card Y *` card X = card Y
proof
assume that
A1: X <> {} & X is finite and
A2: not Y is finite;
card X in card Y & 0 in card X by A1,A2,CARD_3:86,ORDINAL3:8;
hence thesis by A2,Th16;
end;
theorem Th23:
not D is finite & n <> 0 implies n-tuples_on D,D are_equipotent
& card (n-tuples_on D) = card D
proof
assume that
A1: not D is finite and
A2: n <> 0;
defpred P[Nat] means $1 <> 0 implies card ($1-tuples_on D) = card D;
A3: for k being Nat holds P[k] implies P[k+1]
proof
let k be Nat;
0-tuples_on D = { <*>D } by FINSEQ_2:94;
then
A4: 0 in card (0-tuples_on D) & card (0-tuples_on D) c= card D by A1,ORDINAL3:8
;
A5: card ((k+1)-tuples_on D) = card [:(k-tuples_on D),1-tuples_on D:] by Th9
.= card [:card (k-tuples_on D),card (1-tuples_on D):] by CARD_2:7
.= card [:card (k-tuples_on D),card D:] by Th8
.= card (k-tuples_on D) *` card D by CARD_2:def 2;
assume P[k];
hence thesis by A1,A5,A4,Th16;
end;
A6: P[0];
for k being Nat holds P[k] from NAT_1:sch 2(A6,A3);
then card (n-tuples_on D) = card D by A2;
hence thesis by CARD_1:5;
end;
theorem
not D is finite implies card D = card (D*)
proof
defpred P[set] means not contradiction;
deffunc f(Nat) = $1-tuples_on D;
A1: D* = union the set of all k-tuples_on D by FINSEQ_2:108;
assume
A2: not D is finite;
A3: for X st X in the set of all k-tuples_on D holds card X c= card D
proof
let X;
assume X in the set of all k-tuples_on D;
then consider k such that
A4: X = k-tuples_on D;
0-tuples_on D = { <*>D } by FINSEQ_2:94;
then card (0-tuples_on D) c= card D & k = 0 or k <> 0 by A2;
hence thesis by A2,A4,Th23;
end;
1-tuples_on D in the set of all k-tuples_on D;
then card (1-tuples_on D) c= card (D*) by A1,CARD_1:11,ZFMISC_1:74;
then
A5: card D c= card (D*) by Th8;
{f(k): P[k]} is countable from FraenCoun1;
then card the set of all k-tuples_on D c= omega;
then card union the set of all k-tuples_on D c= omega *` card D by A3,
CARD_2:87;
then card (D*) c= card D by A2,A1,Th21;
hence thesis by A5;
end;