Copyright (c) 1990 Association of Mizar Users
environ
vocabulary ORDINAL1, CARD_1, FUNCT_1, FINSET_1, TARSKI, ORDINAL2, BOOLE,
RELAT_1, CARD_2, ZFMISC_1, GROUP_1, ARYTM_3, MCART_1, FINSEQ_2, FINSEQ_1,
PROB_1, RLVECT_1, FUNCOP_1, CARD_3, FUNCT_2, PARTFUN1, FUNCT_4, CARD_4,
HAHNBAN;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, XCMPLX_0, XREAL_0,
REAL_1, NAT_1, RELAT_1, FUNCT_1, FINSEQ_1, FINSET_1, ORDINAL1, WELLORD2,
ORDINAL2, MCART_1, DOMAIN_1, CARD_1, CARD_2, FINSEQ_2, FUNCT_2, FUNCT_4,
FUNCOP_1, PARTFUN1, NEWTON, PROB_1, CARD_3;
constructors NAT_1, WELLORD2, DOMAIN_1, CARD_2, FUNCT_4, FUNCOP_1, PARTFUN1,
NEWTON, CARD_3, PROB_1, MEMBERED, XBOOLE_0;
clusters SUBSET_1, FUNCT_1, FINSEQ_1, ORDINAL1, CARD_1, CARD_3, FINSET_1,
FINSEQ_2, RELSET_1, NAT_1, XREAL_0, MEMBERED, ZFMISC_1, XBOOLE_0,
NUMBERS, ORDINAL2;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
definitions TARSKI, FUNCT_1, WELLORD2, ZF_REFLE, RELAT_1, XBOOLE_0;
theorems AXIOMS, TARSKI, ZFMISC_1, REAL_1, NAT_1, ORDINAL1, ORDINAL2,
ORDINAL3, WELLORD2, FUNCT_1, FUNCT_2, FUNCT_4, FUNCT_5, FUNCOP_1,
PARTFUN1, MCART_1, PROB_1, ORDERS_2, CARD_1, CARD_2, CARD_3, NEWTON,
FINSEQ_1, FINSET_1, FINSEQ_2, RELAT_1, RELSET_1, XBOOLE_0, XBOOLE_1,
XCMPLX_1;
schemes NAT_1, FUNCT_1, FUNCT_2, ORDINAL2, CARD_3, XBOOLE_0;
begin
reserve X,Y,Z,x,y,y1,y2 for set, D for non empty set,
k,m,n,n1,n2,n3,m2,m1 for Nat,
A,B for Ordinal, L,K,M,N for Cardinal,
f,g for Function;
Lm1: 0 = Card 0 & 1 = Card 1 & 2 = Card 2 by CARD_1:def 5;
theorem
Th1: X is finite iff Card X is finite
proof X,Card X are_equipotent by CARD_1:def 5;
hence thesis by CARD_1:68;
end;
theorem
Th2: X is finite iff Card X <` alef 0
proof
thus X is finite implies Card X <` alef 0
by CARD_1:83,84,CARD_3:58;
assume A1:Card X in alef 0;
reconsider A = Card X as Ordinal;
ex n st n = A by A1,CARD_1:83;
hence thesis by Th1;
end;
theorem
X is finite implies Card X in alef 0 & Card X in omega by Th2,CARD_1:83;
theorem
X is finite iff ex n st Card X = Card n
proof
hereby
assume X is finite;
then reconsider X' = X as finite set;
Card X = Card card X' by CARD_1:def 11;
hence ex n st Card X = Card n;
end;
given n such that
A1: Card X = Card n;
thus thesis by A1,Th1;
end;
theorem
Th5: succ A \ {A} = A
proof
thus succ A \ {A} c= A
proof let x; assume x in succ A \ {A};
then x in succ A & not x in {A} by XBOOLE_0:def 4;
then (x in A or x = A) & x <> A by ORDINAL1:13,TARSKI:def 1;
hence thesis;
end;
let x; assume x in A;
then x in succ A & x <> A by ORDINAL1:13;
then x in succ A & not x in {A} by TARSKI:def 1;
hence thesis by XBOOLE_0:def 4;
end;
theorem
Th6: A,n are_equipotent implies A = n
proof
defpred P[Nat] means for A st A,$1 are_equipotent holds A = $1;
A1: P[0] by CARD_1:46;
A2: for n st P[n] holds P[n+1]
proof let n such that
A3: P[n];
let A; assume
A4: A,n+1 are_equipotent;
then A5: (n+1) = succ n & succ n <> {} & (n+1),A are_equipotent
by CARD_1:52;
A <> {} by A4,CARD_1:46;
then A6: {} in A by ORDINAL3:10;
now assume A is_limit_ordinal;
then omega c= A & (n+1) in omega & Card (n+1) = (n+1)
by A6,CARD_1:def 5,ORDINAL2:def 5;
then Card omega <=` Card A & Card A = Card (n+1) &
Card (n+1) <` Card omega
by A4,CARD_1:21,27,84;
hence contradiction by CARD_1:14;
end;
then consider B such that
A7: A = succ B by ORDINAL1:42;
B in A & n in (n+1) by A5,A7,ORDINAL1:10;
then A \ {B},(n+1) \ { n} are_equipotent & A\{B} = B &
(n+1) \ { n} = n by A5,A7,Th5,CARD_1:61;
hence thesis by A3,A5,A7;
end;
for n holds P[n] from Ind(A1,A2);
hence thesis;
end;
theorem
Th7: A is finite iff A in omega
proof
thus A is finite implies A in omega
proof assume A is finite;
then consider n such that
A1: A,n are_equipotent by CARD_1:74;
A = n by A1,Th6;
hence thesis;
end;
assume A in omega;
then ex n st n = A;
hence thesis;
end;
theorem
not A is finite iff omega c= A
proof (omega c= A iff not A in omega) & (A is finite iff A in omega)
by Th7,ORDINAL1:7,26;
hence thesis;
end;
theorem
M is finite iff M in alef 0 by Th7,CARD_1:83;
canceled;
theorem
Th11: not M is finite iff alef 0 c= M
proof
(M is finite iff M in alef 0) &
(M <` alef 0 iff not alef 0 <=` M) by Th7,CARD_1:14,83;
hence thesis;
end;
canceled;
theorem
Th13: N is finite & not M is finite implies N <` M & N <=` M
proof assume N is finite & not M is finite;
then A1: N <` alef 0 & alef 0 <=` M by Th7,Th11,CARD_1:83;
hence N <` M;
thus thesis by A1,CARD_1:13;
end;
theorem
not X is finite iff ex Y st Y c= X & Card Y = alef 0
proof
thus not X is finite implies ex Y st Y c= X & Card Y = alef 0
proof assume not X is finite;
then not Card X is finite by Th1;
then not Card X <` alef 0 by Th7,CARD_1:83;
then A1: alef 0 <=` Card X by CARD_1:14;
Card X,X are_equipotent by CARD_1:def 5;
then consider f such that
A2: f is one-to-one & dom f = Card X & rng f = X by WELLORD2:def 4;
take Y = f.:(alef 0);
thus Y c= X by A2,RELAT_1:144;
alef 0,Y are_equipotent
proof take f|(alef 0);
thus thesis by A1,A2,FUNCT_1:84,RELAT_1:91,148;
end;
hence Card Y = alef 0 by CARD_1:def 5;
end;
given Y such that
A3: Y c= X & Card Y = alef 0;
Card Y <=` Card X by A3,CARD_1:27;
then not Card X <` alef 0 by A3,CARD_1:14;
hence thesis by Th2;
end;
theorem
Th15: not omega is finite & not NAT is finite
proof A1:not Card omega <` alef 0 by CARD_1:83,84;
hence not omega is finite by Th2;
thus thesis by A1,Th2;
end;
theorem
not alef 0 is finite by Th15,CARD_1:83;
theorem
X = {} iff Card X = 0 by CARD_1:47,CARD_2:59;
canceled;
theorem
Th19: 0 <=` M
proof M = 0 or 0 <` M by ORDINAL3:10;
hence thesis by CARD_1:13;
end;
theorem
Th20: Card X = Card Y iff nextcard X = nextcard Y
proof
thus Card X = Card Y implies nextcard X = nextcard Y by CARD_1:34;
assume
A1: nextcard X = nextcard Y & Card X <> Card Y;
then Card X <` Card Y or Card Y <` Card X by ORDINAL1:24;
then nextcard X <=` Card Y & Card Y <` nextcard Y or
nextcard Y <=` Card X & Card X <` nextcard X by CARD_1:def 6;
hence thesis by A1,ORDINAL1:22;
end;
theorem
M = N iff nextcard N = nextcard M
proof Card N = N & Card M = M by CARD_1:def 5;
hence thesis by Th20;
end;
theorem
Th22: N <` M iff nextcard N <=` M
proof N <` nextcard N & Card N = N by CARD_1:32,def 5;
hence thesis by CARD_1:def 6;
end;
theorem
N <` nextcard M iff N <=` M
proof
(not N <=` M iff M <` N) & (N <` nextcard M iff not nextcard M <=` N)
by CARD_1:14;
hence thesis by Th22;
end;
theorem
Th24: 0 <` M iff 1 <=` M
proof 0+1 = 1;
then nextcard Card 0 = Card 1 by CARD_1:76;
hence thesis by Lm1,Th22;
end;
theorem
1 <` M iff 2 <=` M
proof 1+1 = 2;
then nextcard Card 1 = Card 2 by CARD_1:76;
hence thesis by Lm1,Th22;
end;
theorem
Th26: M is finite & (N <=` M or N <` M) implies N is finite
proof assume
A1: M is finite & (N <=` M or N <` M);
then N <=` M by CARD_1:13;
hence thesis by A1,FINSET_1:13;
end;
set two = succ one;
theorem
Th27: 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:44;
A3: P[k] implies P[k+1]
proof (k+1) = succ k by CARD_1:52;
then B+^(k+1) = succ (B+^ k) by ORDINAL2:45;
hence thesis by A1,ORDINAL1:41;
end;
P[k] from Ind(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 & 1 = 0+1 by A4;
hence succ B in A by ORDINAL2:48,def 4;
end;
hence thesis by ORDINAL1:41;
end;
theorem
Th28: A+^succ n = succ A +^ n & A +^ (n+1) = succ A +^ n
proof
defpred P[Nat] means A+^succ $1 = succ A +^ $1;
A1: P[0] proof
thus A+^succ 0 = succ A by ORDINAL2:48,def 4
.= succ A +^ 0 by ORDINAL2:44;
end;
A2: P[k] implies P[k+1]
proof assume
A3: P[k];
A4: k+1 = succ k by CARD_1:52;
hence A+^succ (k+1) = succ (succ A +^ k) by A3,ORDINAL2:45
.= succ A +^ k +^ one by ORDINAL2:48
.= succ A +^ ( k +^ one) by ORDINAL3:33
.= succ A +^ (k+1) by A4,ORDINAL2:48;
end;
P[k] from Ind(A1,A2);
hence A+^succ n = succ A +^ n;
hence thesis by CARD_1:52;
end;
theorem
Th29: ex n st A*^succ one = A +^ n
proof
defpred P[Ordinal] means ex n st $1*^two = $1+^ n;
{}+^{} = {} & {}*^two = {} by ORDINAL2:44,52;
then A1: P[{}] by CARD_1:51;
A2: for A st P[A] holds P[succ A]
proof let A; given n such that
A3: A*^two = A+^ n;
take n+1;
(succ A)*^two = A*^two+^two by ORDINAL2:53
.= succ(A*^two+^one) by ORDINAL2:45
.= succ succ(A+^ n) by A3,ORDINAL2:48
.= succ (A+^succ n) by ORDINAL2:45
.= succ (A+^ (n+1)) by CARD_1:52
.= A+^succ (n+1) by ORDINAL2:45;
hence thesis by Th28;
end;
A4: for A st A <> {} & A is_limit_ordinal & for B st B in A holds P[B]
holds P[A]
proof let A; assume that
A5: A <> {} & A is_limit_ordinal and
A6: for B st B in A holds P[B];
take 0;
deffunc f(Ordinal) = $1*^two;
consider phi being Ordinal-Sequence such that
A7: dom phi = A and
A8: for B st B in A holds phi.B = f(B) from OS_Lambda;
A9: A*^two = union sup phi by A5,A7,A8,ORDINAL2:54
.= union sup rng phi by ORDINAL2:35;
thus A*^two c= A+^ 0
proof let B; assume B in A*^two;
then consider X such that
A10: B in X & X in sup rng phi by A9,TARSKI:def 4;
reconsider X as Ordinal by A10,ORDINAL1:23;
consider C being Ordinal such that
A11: C in rng phi & X c= C by A10,ORDINAL2:29;
consider x such that
A12: x in dom phi & C = phi.x by A11,FUNCT_1:def 5;
reconsider x as Ordinal by A12,ORDINAL1:23;
A13: ex n st x*^two = x+^ n by A6,A7,A12;
C = x*^two by A7,A8,A12;
then C in A by A5,A7,A12,A13,Th27;
then X in A & A+^{} = A by A11,ORDINAL1:22,ORDINAL2:44;
hence thesis by A10,ORDINAL1:19;
end;
one in two by ORDINAL1:10;
then A+^ 0 = A & A = A*^one & one c= two
by ORDINAL1:def 2,ORDINAL2:44,56;
hence thesis by ORDINAL2:59;
end;
for A holds P[A] from Ordinal_Ind(A1,A2,A4);
hence thesis;
end;
theorem
Th30: A is_limit_ordinal implies A *^ succ one = A
proof consider n such that
A1: A*^two = A+^ n by Th29;
assume A is_limit_ordinal;
then A2: A+^ n is_limit_ordinal by A1,ORDINAL3:48;
now assume n <> 0;
then consider k such that
A3: n = k+1 by NAT_1:22;
n = succ k by A3,CARD_1:52;
then A+^ n = succ(A+^ k) by ORDINAL2:45;
hence contradiction by A2,ORDINAL1:42;
end;
hence thesis by A1,ORDINAL2:44;
end;
theorem
Th31: omega c= A implies one+^A = A
proof
deffunc f(Ordinal) = one+^$1;
consider phi being Ordinal-Sequence such that
A1: dom phi = omega & for B st B in omega holds phi.B = f(B) from OS_Lambda;
A2: one+^omega = sup phi by A1,ORDINAL2:19,46
.= sup rng phi by ORDINAL2:35;
A3: one+^omega c= omega
proof let B; assume B in one+^omega;
then consider C being Ordinal such that
A4: C in rng phi & B c= C by A2,ORDINAL2:29;
consider x such that
A5: x in dom phi & C = phi.x by A4,FUNCT_1:def 5;
reconsider x as Ordinal by A5,ORDINAL1:23;
reconsider x' = x as Cardinal by A1,A5,CARD_1:65;
reconsider x as finite Ordinal by A1,A5,Th7;
Card card x = Card x & Card card x = card x & Card x' = x &
0+1 = one
by CARD_1:def 5,ORDINAL2:def 4;
then x+^one = (card x+1) & one+^x = (1+card x) by CARD_2:49;
then C = one+^x & one+^x = x+^one & succ x in omega
by A1,A5,ORDINAL1:41,ORDINAL2:19;
then C in omega by ORDINAL2:48;
hence thesis by A4,ORDINAL1:22;
end;
assume omega c= A;
then A6: ex B st A = omega+^B by ORDINAL3:30;
omega c= one+^omega by ORDINAL3:27;
then omega = one+^omega by A3,XBOOLE_0:def 10;
hence one+^A = A by A6,ORDINAL3:33;
end;
theorem
Th32: M is infinite implies M is_limit_ordinal
proof assume M is infinite;
then A1: not M <` alef 0 by Th7,CARD_1:83;
assume not thesis;
then consider A such that
A2: M = succ A by ORDINAL1:42;
omega <> M & omega c= M iff omega c< M
by XBOOLE_0:def 8;
then omega = succ A or omega in succ A by A1,A2,CARD_1:14,83,ORDINAL1:21;
then A3: omega c= A by ORDINAL1:34,42,ORDINAL2:19;
Card (A+^one) = Card one +` Card A by CARD_2:24
.= Card (one+^A) by CARD_2:24
.= Card A by A3,Th31;
then Card succ A = Card A & A in succ A by ORDINAL1:10,ORDINAL2:48;
then A,succ A are_equipotent & not succ A c= A & ex B st succ A = B &
for A st A,B are_equipotent holds B c= A
by A2,CARD_1:21,def 1,ORDINAL1:7;
hence contradiction;
end;
theorem
Th33: not M is finite implies M+`M = M
proof assume not M is finite;
then M is_limit_ordinal by Th32;
then ( M)*^two = M by Th30;
then Card M = (Card two)*`Card M by CARD_2:25
.= Card (two*^ M) by CARD_2:25
.= Card (one*^ M+^ M) by ORDINAL2:53
.= Card ( M+^ M) by ORDINAL2:56
.= M+`M by CARD_2:def 1;
hence thesis by CARD_1:def 5;
end;
theorem
Th34: not M is finite & (N <=` M or N <` M) implies M+`N = M & N+`M = M
proof assume
not M is finite & (N <=` M or N <` M);
then A1: M+`M = M & M+`M = Card ( M +^ M) & M+`N = Card ( M +^ N) &
N c= M & N = N & M = M by Th33,CARD_1:13,CARD_2:def 1;
then M +^ N c= M +^ M & M c= M +^ N & Card M = M
by CARD_1:def 5,ORDINAL2:50,ORDINAL3:27;
then M+`N <=` M & M <=` M+`N & M+`N = N+`M by A1,CARD_1:27;
hence M+`N = M & N+`M = M by XBOOLE_0:def 10;
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 not X is finite & (X,Y are_equipotent or Y,X are_equipotent);
then not Card X is finite & Card X = Card Y & X c= X \/ Y
by Th1,CARD_1:21,XBOOLE_1:7;
then Card X <=` Card (X \/ Y) & Card (X \/ Y) <=` Card X +` Card Y &
Card X +` Card Y = Card X by Th33,CARD_1:27,CARD_2:47;
then Card X = Card (X \/ Y) by XBOOLE_0:def 10;
hence thesis by CARD_1:21;
end;
theorem
not X is finite & Y is finite implies
X \/ Y,X are_equipotent & Card (X \/ Y) = Card X
proof assume not X is finite & Y is finite;
then A1: not Card X is finite & Card Y is finite by Th1;
then Card Y <` Card X & X c= X \/ Y by Th13,XBOOLE_1:7;
then Card X +` Card Y = Card X & Card (X \/ Y) <=` Card X +` Card Y &
Card X <=` Card (X \/ Y) by A1,Th34,CARD_1:27,CARD_2:47;
then Card X = Card (X \/ Y) by XBOOLE_0:def 10;
hence thesis by CARD_1:21;
end;
theorem
not X is finite & (Card Y <` Card X or Card Y <=` Card X) implies
X \/ Y,X are_equipotent & Card (X \/ Y) = Card X
proof assume not X is finite & (Card Y <` Card X or Card Y <=` Card X);
then A1: not Card X is finite & Card Y <=` Card X by Th1,CARD_1:13;
X c= X \/ Y by XBOOLE_1:7;
then Card X +` Card Y = Card X & Card (X \/ Y) <=` Card X +` Card Y &
Card X <=` Card (X \/ Y) by A1,Th34,CARD_1:27,CARD_2:47;
then Card X = Card (X \/ Y) by XBOOLE_0:def 10;
hence thesis by CARD_1:21;
end;
theorem
for M,N being finite Cardinal holds M+`N is finite
proof let M,N be finite Cardinal;
Card M = Card card M & Card N = Card card N & Card M = M & Card N = N
by CARD_1:def 5;
then M+`N = Card (card M + card N) by CARD_2:51;
hence M+`N is finite;
end;
theorem
not M is finite implies not M+`N is finite & not N+`M is finite
proof assume
A1: not M is finite;
M,N are_c=-comparable by ORDINAL1:25;
then M <=` N or N <=` M by XBOOLE_0:def 9;
then M <=` N & not N is finite or M+`N = M & N+`M = M by A1,Th26,Th34;
hence thesis by A1,Th34;
end;
theorem
for M,N being finite Cardinal holds M*`N is finite
proof let M,N be finite Cardinal;
Card M = Card card M & Card N = Card card N & Card M = M & Card N = N
by CARD_1:def 5;
then M*`N = Card (card M * card N) by CARD_2:52;
hence M*`N is finite;
end;
theorem Th41:
K <` L & M <` N or K <=` L & M <` N or K <` L & M <=` N or K <=` L & M <=` N
implies
K+`M <=` L+`N & M+`K <=` L+`N
proof assume
K <` L & M <` N or K <=` L & M <` N or K <` L & M <=` N or K <=` L & M
<=`
N;
then K <=` L & M <=` N & K = K & L = L & M = M & N = N
by CARD_1:13;
then A1: K+`M = Card ( K +^ M) & L+`N = Card ( L +^ N) &
K +^ M c= L +^ N by CARD_2:def 1,ORDINAL3:21;
hence K+`M <=` L+`N by CARD_1:27;
thus thesis by A1,CARD_1:27;
end;
theorem
M <` N or M <=` N implies K+`M <=` K+`N & K+`M <=` N+`K &
M+`K <=` K+`N & M+`K <=` N+`K by Th41;
definition let X;
attr X is countable means:
Def1: Card X <=` alef 0;
end;
theorem
Th43: X is finite implies X is countable
proof assume X is finite;
then consider n such that
A1: X,n are_equipotent by CARD_1:74;
n c= omega by ORDINAL1:def 2;
then Card n = Card X & Card n <=` Card omega by A1,CARD_1:21,27;
hence Card X <=` alef 0 by CARD_1:83,84;
end;
theorem
Th44: omega is countable & NAT is countable
proof
thus Card omega <=` alef 0 by CARD_1:83,84;
thus Card NAT <=` alef 0 by CARD_1:83,84;
end;
theorem
Th45: X is countable iff ex f st dom f = NAT & X c= rng f
proof
thus X is countable implies ex f st dom f = NAT & X c= rng f
proof assume Card X <=` alef 0;
hence thesis by CARD_1:28,83,84;
end;
assume ex f st dom f = NAT & X c= rng f;
hence Card X <=` alef 0 by CARD_1:28,83,84;
end;
theorem
Th46: Y c= X & X is countable implies Y is countable
proof assume Y c= X;
then A1: Card Y <=` Card X by CARD_1:27;
assume Card X <=` alef 0;
hence Card Y <=` alef 0 by A1,XBOOLE_1:1;
end;
theorem
Th47: X is countable & Y is countable implies X \/ Y is countable
proof assume Card X <=` alef 0 & Card Y <=` alef 0;
then Card (X \/ Y) <=` Card X +` Card Y & alef 0 +` alef 0 = alef 0 &
Card X +` Card Y <=` alef 0 +` alef 0
by Th15,Th33,Th41,CARD_1:83,CARD_2:47;
hence Card (X \/ Y) <=` alef 0 by XBOOLE_1:1;
end;
theorem
X is countable implies X /\ Y is countable & Y /\ X is countable
proof X /\ Y c= X & Y /\ X c= X by XBOOLE_1:17;
hence thesis by Th46;
end;
theorem
Th49: X is countable implies X \ Y is countable
proof X \ Y c= X by XBOOLE_1:36;
hence thesis by Th46;
end;
theorem
X is countable & Y is countable implies X \+\ Y is countable
proof assume X is countable & Y is countable;
then X \ Y is countable & Y \ X is countable by Th49;
then (X \ Y) \/ (Y \ X) is countable by Th47;
hence X \+\ Y is countable by XBOOLE_0:def 6;
end;
reserve r for Real;
theorem
Th51: 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[0] by NEWTON:9;
A2: P[k] implies P[k+1]
proof assume
A3: P[k];
r|^(k+1) = r|^k*r by NEWTON:11;
hence thesis by A3,XCMPLX_1:6;
end;
P[k] from Ind(A1,A2);
hence thesis;
end;
definition let m,n be Nat;
redefine func m|^n -> Nat;
coherence
proof
defpred P[Nat] means m|^$1 is Nat;
A1: P[0] by NEWTON:9;
A2: P[k] implies P[k+1]
proof assume m|^k is Nat;
then reconsider x = m|^k as Nat;
m|^(k+1) = x*m by NEWTON:11;
hence thesis;
end;
P[k] from Ind(A1,A2);
hence thesis;
end;
end;
Lm2: (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 such that
A3: n1 = n2+n by NAT_1:28;
n <> 0 by A2,A3;
then consider k such that
A4: n = k+1 by NAT_1:22;
2|^n1 = (2|^n2)*(2|^(k+1)) & 2 <> 0 by A3,A4,NEWTON:13;
then (2|^n1)*(2*m1+1) = 2|^n2*(2|^(k+1)*(2*m1+1)) & 2|^n2 <> 0
by Th51,XCMPLX_1:4;
then 2|^(k+1)*(2*m1+1) = 2*m2+1 by A1,XCMPLX_1:5;
then 2*m2+1 = 2|^k*(2|^1)*(2*m1+1) by NEWTON:13
.= 2*(2|^k)*(2*m1+1) by NEWTON:10
.= 2*((2|^k)*(2*m1+1)) by XCMPLX_1:4;
then 2 divides 2*m2+1 & 2 divides 2*m2 by NAT_1:def 3;
then 2 divides 1 & 0 < 1 by NAT_1:57;
hence contradiction by NAT_1:54;
end;
theorem
Th52: (2|^n1)*(2*m1+1) = (2|^n2)*(2*m2+1) implies n1 = n2 & m1 = m2
proof assume
A1: (2|^n1)*(2*m1+1) = (2|^n2)*(2*m2+1);
then n1 <= n2 & n2 <= n1 by Lm2;
hence
A2: n1 = n2 by AXIOMS:21; 2|^n1 <> 0 by Th51;
then 2*m1+1 = 2*m2+1 by A1,A2,XCMPLX_1:5;
then 2*m1 = 2*m2 & 2 <> 0 by XCMPLX_1:2;
hence m1 = m2 by XCMPLX_1:5;
end;
Lm3: x in [:NAT,NAT:] implies ex n1,n2 st x = [n1,n2]
proof assume A1: x in [:NAT,NAT:];
then reconsider n1 = x`1, n2 = x`2 as Nat by MCART_1:10;
take n1,n2; thus thesis by A1,MCART_1:23;
end;
theorem
Th53: [:NAT,NAT:],NAT are_equipotent & Card NAT = Card [:NAT,NAT:]
proof
deffunc f(Nat,Nat) = (2|^$1)*(2*$2+1);
consider f being Function of [:NAT,NAT:],NAT such that
A1: f.[n,m] = f(n,m) from Lambda2D;
A2: dom f = [:NAT,NAT:] & rng f c= NAT by FUNCT_2:def 1,RELSET_1:12;
f is one-to-one
proof let x,y; assume x in dom f;
then consider n1,m1 being Nat such that
A3: x = [n1,m1] by A2,Lm3;
assume y in dom f;
then consider n2,m2 being Nat such that
A4: y = [n2,m2] by A2,Lm3;
assume f.x = f.y;
then (2|^n1)*(2*m1+1) = f.y by A1,A3 .= (2|^n2)*(2*m2+1) by A1,A4;
then n1 = n2 & m1 = m2 by Th52;
hence thesis by A3,A4;
end;
then A5: Card [:NAT,NAT:] <=` Card NAT by A2,CARD_1:26;
[:NAT,{0}:] c= [:NAT,NAT:] by ZFMISC_1:118;
then Card [:NAT,{0}:] <=` Card [:NAT,NAT:] by CARD_1:27;
then Card NAT <=` Card [:NAT,NAT:] by CARD_2:13;
then Card NAT = Card [:NAT,NAT:] by A5,XBOOLE_0:def 10;
hence thesis by CARD_1:21;
end;
theorem
Th54: (alef 0)*`(alef 0) = alef 0
proof
thus (alef 0)*`(alef 0) = alef 0 by Th53,CARD_1:83,84,CARD_2:def 2;
end;
theorem
Th55: X is countable & Y is countable implies [:X,Y:] is countable
proof assume Card X c= alef 0 & Card Y c= alef 0;
then [:Card X,Card Y:] c= [:alef 0,alef 0:] by ZFMISC_1:119;
then Card [:Card X,Card Y:] <=` Card [:alef 0,alef 0:] by CARD_1:27;
then Card [:Card X,Card Y:] <=` (alef 0)*`alef 0 by CARD_2:def 2;
hence Card [:X,Y:] <=` alef 0 by Th54,CARD_2:14;
end;
theorem
Th56: 1-tuples_on D,D are_equipotent & Card (1-tuples_on D) = Card D
proof
deffunc f(set) = <*$1*>;
consider f such that
A1: dom f = D & for x st x in D holds f.x = f(x) from Lambda;
D,1-tuples_on D are_equipotent
proof take f;
thus f is one-to-one
proof let x,y; assume x in dom f & y in dom f;
then f.x = <*x*> & f.y = <*y*> & <*x*>.1 = x & <*y*>.1 = y
by A1,FINSEQ_1:def 8;
hence thesis;
end;
thus dom f = D by A1;
thus rng f c= 1-tuples_on D
proof let x; assume x in rng f;
then consider y such that
A2: y in dom f & x = f.y by FUNCT_1:def 5;
reconsider y as Element of D by A1,A2;
x = <*y*> by A1,A2;
then x in { <*d*> where d is Element of D : not contradiction };
hence thesis by FINSEQ_2:116;
end;
let x; 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
A3: y = <*z*> by FINSEQ_2:117;
z in dom f & x = f.z by A1,A3;
hence thesis by FUNCT_1:def 5;
end;
hence thesis by CARD_1:21;
end;
reserve p,q for FinSequence;
theorem
Th57: [: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[set,set] 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,y1,y2 st x in A & P[x,y1] & P[x,y2] holds y1 = y2
proof let x,y1,y2 such that x in A;
given p1 be Element of n-tuples_on D,
q1 be Element of m-tuples_on D such that
A2: x = [p1,q1] & y1 = p1^q1;
given p2 be Element of n-tuples_on D,
q2 be Element of m-tuples_on D such that
A3: x = [p2,q2] & y2 = p2^q2;
p1 = p2 & q1 = q2 by A2,A3,ZFMISC_1:33;
hence thesis by A2,A3;
end;
A4: for x st x in A ex y st P[x,y]
proof let x; assume A5: x in A;
then A6: x = [x`1,x`2] & x`1 in n-tuples_on D & x`2 in m-tuples_on D
by MCART_1:10,23;
reconsider p = x`1 as Element of n-tuples_on D by A5,MCART_1:10;
reconsider q = x`2 as Element of m-tuples_on D by A5,MCART_1:10;
reconsider y = p^q as set;
take y; thus thesis by A6;
end;
consider f such that
A7: dom f = A & for x st x in A holds P[x,f.x] from FuncEx(A1,A4);
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; 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
A8: x = [p1,q1] & f.x = p1^q1 by A7;
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
A9: y = [p2,q2] & f.y = p2^q2 by A7;
assume A10: f.x = f.y;
then A11: p1^q1 = p2^q2 & len p1 = n & len p2 = n & len q1 = m & len q2 =
m
by A8,A9,FINSEQ_2:109;
then consider p such that
A12: p1^p = p2 by FINSEQ_1:64;
consider q such that
A13: p2^q = p1 by A11,FINSEQ_1:64;
len p1+0 = len(p1^p)+len q by A12,A13,FINSEQ_1:35
.= len p1+len p+len q by FINSEQ_1:35
.= len p1+(len p+len q) by XCMPLX_1:1;
then len p + len q = 0 by XCMPLX_1:2;
then len p = 0 by NAT_1:23;
then p = {} by FINSEQ_1:25;
then p1 = p2 by A12,FINSEQ_1:47;
hence thesis by A8,A9,A10,FINSEQ_1:46;
end;
thus dom f = A by A7;
thus rng f c= B
proof let x; assume x in rng f;
then consider y such that
A14: y in dom f & x = f.y by FUNCT_1:def 5;
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 A7,A14;
then x is Element of (n+m)-tuples_on D by FINSEQ_2:127;
hence thesis;
end;
let x; 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
A15: x = p^q by FINSEQ_2:126;
consider p1 being Element of n-tuples_on D,
q1 being Element of m-tuples_on D such that
A16: [p,q] = [p1,q1] & f.[p,q] = p1^q1 by A7;
p1 = p & q1 = q by A16,ZFMISC_1:33;
hence thesis by A7,A15,A16,FUNCT_1:def 5;
end;
hence thesis by CARD_1:21;
end;
theorem
Th58: D is countable implies n-tuples_on D is countable
proof assume
Card D <=` alef 0;
then Card (1-tuples_on D) <=` alef 0 by Th56;
then A1: 1-tuples_on D is countable by Def1;
defpred P[Nat] means $1-tuples_on D is countable;
{ <*>D } is countable by Th43;
then A2: P[0] by FINSEQ_2:112;
A3: P[k] implies P[k+1]
proof assume P[k];
then [:k-tuples_on D, 1-tuples_on D:] is countable &
[:k-tuples_on D, 1-tuples_on D:],(k+1)-tuples_on D are_equipotent
by A1,Th55,Th57;
then Card [:k-tuples_on D, 1-tuples_on D:] <=` alef 0 &
Card [:k-tuples_on D, 1-tuples_on D:] = Card ((k+1)-tuples_on D)
by Def1,CARD_1:21;
hence thesis by Def1;
end;
P[k] from Ind(A2,A3);
hence thesis;
end;
theorem
Th59: (Card dom f <=` M & for x st x in dom f holds Card (f.x) <=` N) implies
Card Union f <=` M*`N
proof assume
A1: Card dom f c= M & for x st x in dom f holds Card (f.x) <=` N;
A2: Card Union f <=` Sum
Card f & dom Card f = dom f & dom(dom f --> N) = dom f
by CARD_3:54,def 2,FUNCOP_1:19;
now let x; assume x in dom Card f;
then (Card f).x = Card (f.x) & (dom f --> N).x = N & Card (f.x) <=` N
by A1,A2,CARD_3:def 2,FUNCOP_1:13;
hence (Card f).x c= (dom f --> N).x;
end;
then Sum Card f <=` Sum(dom f --> N) by A2,CARD_3:43;
then A3: Card Union f <=` Sum(dom f --> N) & [:Card dom f,N:] c= [:M,N:]
by A1,A2,XBOOLE_1:1,ZFMISC_1:118;
Sum(dom f --> N) = Card Union disjoin (dom f --> N) by CARD_3:def 7
.= Card [:N,dom f:] by CARD_3:36
.= Card [:N,Card dom f:] by CARD_2:14
.= Card [:Card dom f,N:] by CARD_2:11;
then Sum(dom f --> N) <=` Card [:M,N:] & Card [:M,N:] = M*`N
by A3,CARD_1:27,CARD_2:def 2;
hence thesis by A3,XBOOLE_1:1;
end;
theorem Th60:
(Card X <=` M & for Y st Y in X holds Card Y <=` N) implies Card union X <=`
M*`N
proof assume
A1: Card X <=` M & for Y st Y in X holds Card Y <=` N;
A2: dom id X = X by RELAT_1:71;
now let x; assume
x in dom id X;
then (id X).x in X by A2,FUNCT_1:35;
hence Card ((id X).x) <=` N by A1;
end;
then Card Union id X <=` M*`N & Union id X = union rng id X & rng id X = X
by A1,A2,Th59,PROB_1:def 3,RELAT_1:71;
hence thesis;
end;
theorem
Th61: 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 <=` alef 0 & for x st x in dom f holds f.x is countable;
now let x; assume x in dom f;
then f.x is countable by A1;
hence Card (f.x) <=` alef 0 by Def1;
end;
hence Card Union f <=` alef 0 by A1,Th54,Th59;
end;
theorem
(X is countable & for Y st Y in X holds Y is countable) implies
union X is countable
proof assume
A1: Card X <=` alef 0 & for Y st Y in X holds Y is countable;
now let Y; assume Y in X;
then Y is countable by A1;
hence Card Y <=` alef 0 by Def1;
end;
hence Card union X <=` alef 0 by A1,Th54,Th60;
end;
theorem
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
A1: dom f is finite & for x st x in dom f holds f.x is finite;
then reconsider df = dom f as finite set;
A2: Card dom f = Card card df by CARD_1:def 11;
now assume dom f <> {};
then A3: df <> {};
defpred P[set,set] means Card (f.$2) <=` Card (f.$1);
for x,y holds
Card (f.x) c= Card (f.y) or Card (f.y) c= Card (f.x)
proof
let x,y;
Card (f.x), Card (f.y) are_c=-comparable by ORDINAL1:25;
hence thesis by XBOOLE_0:def 9;
end;
then A4: for x,y holds P[x,y] or P[y,x];
A5: for x,y,z being set 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 A1,A6;
Card Union f <=` (Card card df) *` (Card (f.x)) &
Card (f.x) = Card card (fx) by A2,A6,Th59,CARD_1:def 11;
then Card Union f <=` Card ((card df) * (card (fx))) &
Card ((card df) * (card (fx))) is finite
by CARD_2:52;
then Card Union f is finite by Th26;
hence thesis by Th1;
end;
hence thesis by CARD_3:14,RELAT_1:64;
end;
canceled;
theorem
D is countable implies D* is countable
proof assume
A1: D is countable;
defpred P[set,set] means ex n st $1 = n & $2 = n-tuples_on D;
A2: for x,y1,y2 st x in NAT & P[x,y1] & P[x,y2] holds y1 = y2;
A3: for x st x in NAT ex y st P[x,y]
proof let x; 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
A4: dom f = NAT & for x st x in NAT holds P[x,f.x] from FuncEx(A2,A3);
A5: now let x; assume x in dom f;
then ex n st x = n & f.x = n-tuples_on D by A4;
hence f.x is countable by A1,Th58;
end;
A6: Union f = union rng f & D* = union { k-tuples_on D : not contradiction }
by FINSEQ_2:128,PROB_1:def 3;
Union f = D*
proof
thus Union f c= D*
proof let x; assume x in Union f;
then consider X such that
A7: x in X & X in rng f by A6,TARSKI:def 4;
consider y such that
A8: y in dom f & X = f.y by A7,FUNCT_1:def 5;
reconsider y as Nat by A4,A8;
ex n st y = n & X = n-tuples_on D by A4,A8;
then X in { k-tuples_on D : not contradiction };
hence thesis by A6,A7,TARSKI:def 4;
end;
let x; assume x in D*;
then consider X such that
A9: x in X & X in { k-tuples_on D : not contradiction } by A6,TARSKI:def 4;
consider n such that
A10: X = n-tuples_on D by A9;
ex k st n = k & f.n = k-tuples_on D by A4;
then X in rng f by A4,A10,FUNCT_1:def 5;
hence x in Union f by A6,A9,TARSKI:def 4;
end;
hence thesis by A4,A5,Th44,Th61;
end;
theorem
alef 0 <=` Card (D*)
proof
defpred P[set,set] means ex p st $1 = p & $2 = len p;
A1: for x,y1,y2 st x in D* & P[x,y1] & P[x,y2] holds y1 = y2;
A2: for x st x in D* ex y st P[x,y]
proof
let x; 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 st x in D* holds P[x,f.x] from FuncEx(A1,A2);
defpred P[Nat] means $1 in f.:(D*);
A4: {} in D* by FINSEQ_1:66;
then len {} = 0 & ex p st {} = p & f.{} = len p by A3,FINSEQ_1:25;
then A5: P[0] by A3,A4,FUNCT_1:def 12;
A6: P[n] implies P[n+1]
proof assume n in f.:(D*);
then consider x such that
A7: x in dom f & x in D* & n = f.x by FUNCT_1:def 12;
consider p such that
A8: x = p & n = len p by A3,A7;
consider y being Element of D;
reconsider p as FinSequence of D by A7,A8,FINSEQ_1:def 11;
A9: p^<*y*> in D* by FINSEQ_1:def 11;
then A10: ex q being FinSequence st p^<*y*> = q & f.(p^<*y*>) = len q
by A3;
len (p^<*y*>) = n+len <*y*> by A8,FINSEQ_1:35 .= n+1 by FINSEQ_1:57;
hence n+1 in f.:(D*) by A3,A9,A10,FUNCT_1:def 12;
end;
A11: P[n] from Ind(A5,A6);
NAT c= f.:(D*)
proof let x; assume x in NAT;
then reconsider n = x as Nat;
n in f.:(D*) by A11;
hence thesis;
end;
hence thesis by CARD_1:83,84,CARD_2:2;
end;
scheme FraenCoun1 { f(set)->set, P[Nat] } :
{ f(n) : P[n] } is countable
proof
deffunc g(set) = f($1);
consider f such that
A1: dom f = NAT & for x st x in NAT holds f.x = g(x) from Lambda;
{ f(n) : P[n] } c= rng f
proof let x; assume x in { f(n) : P[n] };
then consider n such that
A2: x = f(n) & P[n];
f.n = x by A1,A2;
hence thesis by A1,FUNCT_1:def 5;
end;
hence thesis by A1,Th45;
end;
scheme FraenCoun2 { f(set,set)->set, P[set,set] } :
{ f(n1,n2) : P[n1,n2] } is countable
proof consider N being Function such that
A1: N is one-to-one & dom N = NAT & rng N = [:NAT,NAT:] by Th53,WELLORD2:def 4;
deffunc g(set) = f((N.$1)`1,(N.$1)`2);
consider f such that
A2: dom f = NAT & for x st x in NAT holds f.x = g(x) from Lambda;
{ f(n1,n2) : P[n1,n2] } c= rng f
proof let x; assume x in { f(n1,n2) : P[n1,n2] };
then consider n1,n2 such that
A3: x = f(n1,n2) & P[n1,n2];
consider y such that
A4: y in dom N & [n1,n2] = N.y by A1,FUNCT_1:def 5;
[n1,n2]`1 = n1 & [n1,n2]`2 = n2 by MCART_1:7;
then x = f.y by A1,A2,A3,A4;
hence thesis by A1,A2,A4,FUNCT_1:def 5;
end;
hence thesis by A2,Th45;
end;
scheme FraenCoun3 { f(set,set,set)->set, P[Nat,Nat,Nat] } :
{ f(n1,n2,n3) : P[n1,n2,n3] } is countable
proof
[:NAT,NAT:],[:[:NAT,NAT:],NAT:] are_equipotent
by Th53,CARD_2:15;
then NAT,[:[:NAT,NAT:],NAT:] are_equipotent &
[:[:NAT,NAT:],NAT:] = [:NAT,NAT,NAT:]
by Th53,WELLORD2:22,ZFMISC_1:def 3;
then consider N being Function such that
A1: N is one-to-one & dom N = NAT & rng N = [:NAT,NAT,NAT:] by WELLORD2:def 4;
deffunc g(set) = f((N.$1)`1`1,(N.$1)`1`2,(N.$1)`2);
consider f such that
A2: dom f = NAT & for x st x in NAT holds f.x = g(x) from Lambda;
{ f(n1,n2,n3) : P[n1,n2,n3] } c= rng f
proof let x; assume x in { f(n1,n2,n3) : P[n1,n2,n3] };
then consider n1,n2,n3 such that
A3: x = f(n1,n2,n3) & P[n1,n2,n3];
reconsider NAT' = NAT as non empty set;
reconsider n1,n2,n3 as Element of NAT';
consider y such that
A4: y in dom N & [n1,n2,n3] = N.y by A1,FUNCT_1:def 5;
[n1,n2,n3]`1 = n1 & [n1,n2,n3]`2 = n2 & [n1,n2,n3]`3 = n3 &
[n1,n2,n3]`1 = ([n1,n2,n3] qua set)`1`1 &
[n1,n2,n3]`2 = ([n1,n2,n3] qua set)`1`2 &
[n1,n2,n3]`3 = ([n1,n2,n3] qua set)`2
by MCART_1:47,50;
then x = f.y by A1,A2,A3,A4;
hence thesis by A1,A2,A4,FUNCT_1:def 5;
end;
hence thesis by A2,Th45;
end;
theorem
Th67: (alef 0)*`(Card n) <=` alef 0 & (Card n)*`(alef 0) <=` alef 0
proof
defpred P[Nat] means (alef 0)*`(Card $1) <=` alef 0;
(alef 0)*`(Card 0) = 0 & {} c= alef 0
by Lm1,CARD_2:32,XBOOLE_1:2;
then A1: P[0];
A2: P[k] implies P[k+1]
proof assume
A3: P[k];
A4: not alef 0 is finite by Th11;
Card (k+1) = (k+1) by CARD_1:def 5 .= succ k by CARD_1:52;
then Card (k+1) = Card succ k by CARD_1:def 5;
then (alef 0)*`(Card (k+1)) =
Card (succ k *^ omega) by CARD_1:83,84,CARD_2:25
.= Card ( k *^ omega +^ omega) by ORDINAL2:53
.= Card ( k *^ omega) +` alef 0 by CARD_1:83,84,CARD_2:24
.= (alef 0)*`(Card k) +` alef 0 by CARD_1:83,84,CARD_2:25
.= alef 0 by A3,A4,Th34;
hence thesis;
end;
A5: P[k] from Ind(A1,A2);
hence (alef 0)*`(Card n) <=` alef 0;
thus thesis by A5;
end;
theorem Th68:
K <` L & M <` N or K <=` L & M <` N or K <` L & M <=` N or K <=` L & M <=` N
implies
K*`M <=` L*`N & M*`K <=` L*`N
proof assume
K <` L & M <` N or K <=` L & M <` N or K <` L & M <=` N or K <=` L & M
<=`
N;
then K <=` L & M <=` N by CARD_1:13;
then A1: K*`M = Card [:K,M:] & L*`N = Card [:L,N:] & [:K,M:] c= [:L,N:]
by CARD_2:def 2,ZFMISC_1:119;
hence K*`M <=` L*`N by CARD_1:27;
thus thesis by A1,CARD_1:27;
end;
theorem
M <` N or M <=` N implies
K*`M <=` K*`N & K*`M <=` N*`K & M*`K <=` K*`N & M*`K <=` N*`K by Th68;
theorem Th70:
K <` L & M <` N or K <=` L & M <` N or K <` L & M <=` N or K <=` L & M <=` N
implies
K = 0 or exp(K,M) <=` exp(L,N)
proof assume
A1: K <` L & M <` N or K <=` L & M <` N or K <` L & M <=` N or K <=` L & M
<=`
N;
then A2: K <=` L & M <=` N by CARD_1:13;
now assume L <> {};
then Funcs(N\M,L) <> {} by FUNCT_2:11;
then not Funcs(N\M,L),{} are_equipotent & 0 c= Card Funcs(N\M,L)
by CARD_1:46,XBOOLE_1:2;
then Card Funcs(N\M,L) <> 0 & 0 <=` Card Funcs(N\M,L)
by CARD_1:21,47;
then 0 <` Card Funcs(N\M,L) & 0 = Card 0 by CARD_1:13,def 5;
then nextcard Card 0 <=` Card Funcs(N\M,L) & 0+1 = 1
by CARD_1:def 6;
then A3: 1 <=` Card Funcs(N\M,L) & Card Funcs(M,L) <=` Card Funcs(M,L)
by Lm1,CARD_1:76;
A4: M misses (N\M) by XBOOLE_1:79;
then exp(K,M) = Card Funcs(M,K) & exp(L,N) = Card Funcs(N,L) &
N = M \/ (N\M) & {} = M /\ (N\M) & Funcs(M,K) c= Funcs(M,L)
by A2,CARD_2:def 3,FUNCT_5:63,XBOOLE_0:def 7,XBOOLE_1:45;
then A5: exp(K,M) <=` Card Funcs(M,L) &
exp(L,N) = Card [:Funcs(M,L),Funcs(N\M,L):] &
Card [:Funcs(M,L),Funcs(N\M,L):] =
Card [:Card Funcs(M,L),Card Funcs(N\M,L):] &
Card Funcs(M,L) *` Card Funcs(N\M,L) =
Card [:Card Funcs(M,L),Card Funcs(N\M,L):]
by A4,CARD_1:27,CARD_2:14,def 2,FUNCT_5:69;
then 1 *` Card Funcs(M,L) <=` exp(L,N) by A3,Th68;
then Card Funcs(M,L) <=` exp(L,N) by CARD_2:33;
hence thesis by A5,XBOOLE_1:1;
end;
hence thesis by A1,CARD_1:13;
end;
theorem
M <` N or M <=` N implies K = 0 or
exp(K,M) <=` exp(K,N) & exp(M,K) <=` exp(N,K)
proof assume that
A1: M <` N or M <=` N and
A2: K <> 0;
thus exp(K,M) <=` exp(K,N) by A1,A2,Th70;
M = 0 implies exp(M,K) = 0 by A2,CARD_2:39;
hence thesis by A1,Th19,Th70;
end;
theorem
Th72: M <=` M+`N & N <=` M+`N
proof
M c= M +^ N & N c= M +^ N & M = M & N = N &
Card N = N & Card M = M by CARD_1:def 5,ORDINAL3:27;
then M <=` Card ( M +^ N) & N <=` Card ( M +^ N) by CARD_1:27;
hence thesis by CARD_2:def 1;
end;
theorem
N <> 0 implies M <=` M*`N & M <=` N*`M
proof assume
A1: N <> 0;
N = N & M = M & Card M = M & Card N = N
by CARD_1:def 5;
then M*`N = Card ( M *^ N) & N*`M = Card ( N *^ M) &
M c= M *^ N & M c= N *^ M & Card M = M
by A1,CARD_2:25,ORDINAL3:39;
hence thesis by CARD_1:27;
end;
theorem
Th74: K <` L & M <` N implies K+`M <` L+`N & M+`K <` L+`N
proof
A1: for K,L,M,N st K <` L & M <` N & L <=` N holds K+`M <` L+`N
proof let K,L,M,N such that
A2: K <` L & M <` N & L <=` N;
A3: now assume
A4: N is finite;
then reconsider N as finite Cardinal;
reconsider L,M,K as finite Cardinal by A2,A4,Th26;
Card K = Card card K & Card K = K & Card L = L & Card M = M &
Card N = N by CARD_1:def 5;
then A5: K+`M = Card (card K + card M) & L+`N = Card (card L + card N) &
card K < card L & card M < card N
by A2,CARD_1:73,CARD_2:51;
then card K + card M < card L + card N by REAL_1:67;
hence thesis by A5,CARD_1:73;
end;
now assume A6: not N is finite;
then A7: L+`N = N & omega c= N by A2,Th11,Th34,CARD_1:83;
K, M are_c=-comparable by ORDINAL1:25;
then K <=` M & (M is finite or not M is finite) or
M <=` K & (K is finite or not K is finite) by XBOOLE_0:def 9;
then A8: K is finite & M is finite or K+`M = M or K+`M = K & K <` N
by A2,Th26,Th34;
now assume K is finite & M is finite;
then reconsider K,M as finite Cardinal;
Card K = Card card K & Card M = Card card M &
Card K = K & Card M = M by CARD_1:def 5;
then K+`M = Card (card K + card M) by CARD_2:51
.= (card K + card M) by CARD_1:def 5;
hence thesis by A7,TARSKI:def 3;
end;
hence thesis by A2,A6,A8,Th34;
end;
hence K+`M <` L+`N by A3;
end;
L,N are_c=-comparable by ORDINAL1:25;
then K+`M = M+`K & L+`N = N+`L & (L <=` N or N <=` L)
by XBOOLE_0:def 9;
hence thesis by A1;
end;
theorem
K+`M <` K+`N implies M <` N
proof assume
A1: K+`M <` K+`N & not M <` N;
then N <=` M & K <=` K by CARD_1:14;
then K+`N <=` K+`M by Th41;
hence thesis by A1,CARD_1:14;
end;
theorem Th76:
Card X +` Card Y = Card X & Card Y <` Card X implies Card (X \ Y) = Card X
proof assume
A1: Card X +` Card Y = Card X & Card Y <` Card X;
X c= X \/ Y by XBOOLE_1:7;
then Card X <=` Card (X \/ Y) & Card (X \/ Y) <=` Card X
by A1,CARD_1:27,CARD_2:47;
then A2: Card (X \/ Y) = Card X by XBOOLE_0:def 10;
(X \ Y) misses Y & (X \ Y) \/ Y = X \/ Y by XBOOLE_1:39,79
;
then A3: Card X = Card (X \ Y) +` Card Y by A2,CARD_2:48;
then A4: Card (X \ Y) <=` Card X by Th72;
A5: now assume not Card X is finite;
then A6: Card X +` Card X = Card X by Th33;
assume not thesis;
then Card (X \ Y) <` Card X by A4,CARD_1:13;
then Card X <` Card X by A1,A3,A6,Th74;
hence contradiction;
end;
now assume
A7: Card X is finite;
then Card Y is finite by A1,Th26;
then reconsider X,Y as finite set by A7,Th1;
Card X = Card card X & Card Y = Card card Y by CARD_1:def 11;
then Card (card X + card Y) = Card card X by A1,CARD_2:51;
then card X + card Y = card X + 0 by CARD_1:71;
then card Y = 0 by XCMPLX_1:2;
then Y = {} by CARD_2:59;
hence thesis;
end;
hence Card (X \ Y) = Card X by A5;
end;
reserve f,f1,f2 for Function, X1,X2 for set;
:: Hessenberg's theorem
theorem
Th77: not M is finite implies M*`M = M
proof assume
A1: not M is finite;
defpred P[set] means ex f st f = $1 &
f is one-to-one & dom f = [:rng f,rng f:];
consider X such that
A2: x in X iff x in PFuncs([:M,M:],M) & P[x] from Separation;
A3: 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 A2;
hence thesis;
end;
(alef 0)*`(alef 0) = Card [:alef 0,alef 0:] by CARD_2:def 2;
then [:alef 0,alef 0:],(alef 0)*`(alef 0) are_equipotent by CARD_1:def 5;
then consider f such that
A4: f is one-to-one & dom f = [:alef 0,alef 0:] & rng f = alef 0
by Th54,WELLORD2:def 4;
not M <` alef 0 by A1,Th7,CARD_1:83;
then A5: alef 0 <=` M by CARD_1:14;
then [:alef 0,alef 0:] c= [:M,M:] by ZFMISC_1:119;
then f in PFuncs([:M,M:],M) by A4,A5,PARTFUN1:def 5;
then A6: X <> {} by A2,A4;
for Z st Z <> {} & Z c= X & Z is c=-linear holds union Z in X
proof let Z; assume that
A7: Z <> {} & Z c= X and
A8: Z is c=-linear;
union Z is Relation-like Function-like
proof set F = union Z;
thus for x st x in F ex y1,y2 st [y1,y2] = x
proof let x; assume x in F;
then consider Y such that
A9: x in Y & Y in Z by TARSKI:def 4;
reconsider f = Y as Function by A3,A7,A9;
f = f & for x st x in f ex y1,y2 st [y1,y2] = x
by RELAT_1:def 1;
hence thesis by A9;
end;
let x,y1,y2; assume [x,y1] in F;
then consider X1 such that
A10: [x,y1] in X1 & X1 in Z by TARSKI:def 4;
assume [x,y2] in F;
then consider X2 such that
A11: [x,y2] in X2 & X2 in Z by TARSKI:def 4;
reconsider f1 = X1, f2 = X2 as Function by A3,A7,A10,A11;
X1,X2 are_c=-comparable by A8,A10,A11,ORDINAL1:def 9;
then X1 c= X2 or X2 c= X1 by XBOOLE_0:def 9;
then [x,y2] in X1 & (for x,y1,y2 st [x,y1] in f1 &
[x,y2] in f1 holds y1 = y2) or
[x,y1] in X2 & (for x,y1,y2 st [x,y1] in f2 &
[x,y2] in f2 holds y1 = y2)
by A10,A11,FUNCT_1:def 1;
hence y1 = y2 by A10,A11;
end;
then reconsider f = union Z as Function;
A12: dom f c= [:M,M:]
proof let x; assume x in dom f;
then [x,f.x] in union Z by FUNCT_1:def 4;
then consider Y such that
A13: [x,f.x] in Y & Y in Z by TARSKI:def 4;
Y in PFuncs([:M,M:],M) by A2,A7,A13;
then consider g being Function such that
A14: Y = g & dom g c= [:M,M:] & rng g c= M by PARTFUN1:def 5;
x in dom g by A13,A14,FUNCT_1:8;
hence thesis by A14;
end;
rng f c= M
proof let y; assume y in rng f;
then consider x such that
A15: x in dom f & y = f.x by FUNCT_1:def 5;
[x,y] in union Z by A15,FUNCT_1:def 4;
then consider Y such that
A16: [x,y] in Y & Y in Z by TARSKI:def 4;
Y in PFuncs([:M,M:],M) by A2,A7,A16;
then consider g being Function such that
A17: Y = g & dom g c= [:M,M:] & rng g c= M by PARTFUN1:def 5;
x in dom g & g.x = y by A16,A17,FUNCT_1:8;
then y in rng g by FUNCT_1:def 5;
hence thesis by A17;
end;
then A18: f in PFuncs([:M,M:],M) by A12,PARTFUN1:def 5;
A19: f is one-to-one
proof let x1,x2 be set; assume x1 in dom f & x2 in dom f;
then A20: [x1,f.x1] in f & [x2,f.x2] in f by FUNCT_1:8;
then consider X1 such that
A21: [x1,f.x1] in X1 & X1 in Z by TARSKI:def 4;
consider X2 such that
A22: [x2,f.x2] in X2 & X2 in Z by A20,TARSKI:def 4;
consider f1 such that
A23: f1 = X1 & f1 is one-to-one & dom f1 = [:rng f1,rng f1:]
by A2,A7,A21;
consider f2 such that
A24: f2 = X2 & f2 is one-to-one & dom f2 = [:rng f2,rng f2:]
by A2,A7,A22;
X1, X2 are_c=-comparable by A8,A21,A22,ORDINAL1:def 9;
then X1 c= X2 or X2 c= X1 by XBOOLE_0:def 9;
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 A21,A22,A23,A24,FUNCT_1:8;
hence thesis by A23,A24,FUNCT_1:def 8;
end;
dom f = [:rng f,rng f:]
proof
thus dom f c= [:rng f,rng f:]
proof let x; assume x in dom f;
then [x,f.x] in f by FUNCT_1:def 4;
then consider Y such that
A25: [x,f.x] in Y & Y in Z by TARSKI:def 4;
consider g being Function such that
A26: g = Y & g is one-to-one & dom g = [:rng g,rng g:] by A2,A7,A25;
g <= f by A25,A26,ZFMISC_1:92;
then rng g c= rng f by RELAT_1:25;
then dom g c= [:rng f,rng f:] & x in dom g
by A25,A26,FUNCT_1:8,ZFMISC_1:119;
hence thesis;
end;
let x; assume x in [:rng f,rng f:];
then A27: x = [x`1,x`2] & x`1 in rng f & x`2 in
rng f by MCART_1:10,23;
then consider y1 such that
A28: y1 in dom f & x`1 = f.y1 by FUNCT_1:def 5;
consider y2 such that
A29: y2 in dom f & x`2 = f.y2 by A27,FUNCT_1:def 5;
A30: [y1,x`1] in f & [y2,x`2] in f by A28,A29,FUNCT_1:8;
then consider X1 such that
A31: [y1,x`1] in X1 & X1 in Z by TARSKI:def 4;
consider X2 such that
A32: [y2,x`2] in X2 & X2 in Z by A30,TARSKI:def 4;
consider f1 such that
A33: f1 = X1 & f1 is one-to-one & dom f1 = [:rng f1,rng f1:]
by A2,A7,A31;
consider f2 such that
A34: f2 = X2 & f2 is one-to-one & dom f2 = [:rng f2,rng f2:]
by A2,A7,A32;
X1, X2 are_c=-comparable by A8,A31,A32,ORDINAL1:def 9;
then X1 c= X2 or X2 c= X1 by XBOOLE_0:def 9;
then y1 in dom f1 & y2 in dom f1 & f1.y1 = x`1 & f1.y2 = x`2 or
y1 in dom f2 & y2 in dom f2 & f2.y1 = x`1 & f2.y2 = x`2
by A31,A32,A33,A34,FUNCT_1:8;
then x`1 in rng f1 & x`2 in rng f1 or x`1 in rng f2 & x`2 in rng f2
by FUNCT_1:def 5;
then A35: x in dom f1 or x in dom f2 by A27,A33,A34,ZFMISC_1:106;
f1 <= f & f2 <= f by A31,A32,A33,A34,ZFMISC_1:92;
then dom f1 c= dom f & dom f2 c= dom f by RELAT_1:25;
hence thesis by A35;
end;
hence thesis by A2,A18,A19;
end;
then consider Y such that
A36: Y in X & for Z st Z in X & Z <> Y holds not Y c= Z
by A6,ORDERS_2:79;
consider f such that
A37: f = Y & f is one-to-one & dom f = [:rng f,rng f:] by A2,A36;
Y in PFuncs([:M,M:],M) by A2,A36;
then A38: ex f st Y = f & dom f c= [:M,M:] & rng f c= M by PARTFUN1:def 5;
then A39: dom f c= [:M,M:] & rng f c= M & Card M = M by A37,CARD_1:def 5;
set A = rng f;
set N = Card A;
now assume
A40: A is finite;
then reconsider A as finite set;
A41: N <` alef 0 & alef 0 <=` alef 0 & N = Card card A
by A40,Th2,CARD_1:def 11;
then A42: alef 0 <=` alef 0 +` N & not alef 0 is finite &
alef 0 +` N <=` alef 0 +` alef 0 by Th11,Th41,Th72;
then alef 0 +` alef 0 = alef 0 by Th33;
then A43: alef 0 = alef 0 +` N & Card alef 0 = alef 0 &
alef 0 c= alef 0 \/ A by A42,CARD_1:def 5,XBOOLE_0:def 10,XBOOLE_1:7;
then A44: alef 0 = Card (alef 0 \ A) & Card (alef 0 \/ A) <=` alef 0 &
alef 0 <=` Card (alef 0 \/ A) by A41,Th76,CARD_1:27,CARD_2:47;
(alef 0 \ A) misses A & A misses (alef 0 \ A) by XBOOLE_1:79;
then A45: (alef 0 \ A) /\ A = {} & A /\ (alef 0 \ A) = {} by XBOOLE_0:def 7;
then [:(alef 0 \ A) /\ (alef 0 \ A),(alef 0 \ A) /\ A:] = {} &
[:(alef 0 \ A) /\ A,(alef 0 \ A) /\ (alef 0 \ A):] = {} &
[:(alef 0 \ A) /\ A,A /\ (alef 0 \ A):] = {} by ZFMISC_1:113;
then A46: [:alef 0 \ A,alef 0 \ A:] /\ [:alef 0 \ A,A:] = {} &
[:alef 0 \ A,alef 0 \ A:] /\ [:A,alef 0 \ A:] = {} &
[:alef 0 \ A,A:] /\ [:A,alef 0 \ A:] = {} by ZFMISC_1:123;
then A47: [:alef 0 \ A,alef 0 \ A:] misses [:alef 0 \ A,A:] &
[:alef 0 \ A,alef 0 \ A:] misses [:A,alef 0 \ A:] &
[:alef 0 \ A,A:] misses [:A,alef 0 \ A:] by XBOOLE_0:def 7;
([:alef 0 \ A,alef 0 \ A:] \/ [:alef 0 \ A,A:]) /\
[:A,alef 0 \ A:] = {} \/ {} by A46,XBOOLE_1:23 .= {};
then ([:alef 0 \ A,alef 0 \ A:] \/ [:alef 0 \ A,A:]) misses
[:A,alef 0 \ A:] by XBOOLE_0:def 7;
then A48: Card ([:alef 0 \ A,alef 0 \ A:] \/
[:alef 0 \ A,A:] \/ [:A,alef 0 \ A:]) =
Card ([:alef 0 \ A,alef 0 \ A:] \/
[:alef 0 \ A,A:]) +` Card [:A,alef 0 \ A:] by CARD_2:48 .=
Card [:alef 0 \ A,alef 0 \ A:] +`
Card [:alef 0 \ A,A:] +` Card [:A,alef 0 \ A:]
by A47,CARD_2:48 .=
Card [:alef 0 \ A,alef 0 \ A:] +`
Card [:alef 0,N:] +` Card [:A,alef 0 \ A:] by A44,CARD_2:14 .=
Card [:alef 0,alef 0:] +`
Card [:alef 0,N:] +` Card [:A,alef 0 \ A:] by A44,CARD_2:14 .=
Card [:alef 0,alef 0:] +`
Card [:alef 0,N:] +` Card [:N,alef 0:] by A44,CARD_2:14 .=
alef 0 +` Card [:alef 0,N:] +` Card [:N,alef 0:]
by Th54,CARD_2:def 2
.= alef 0 +` (alef 0)*`N +` Card [:N,alef 0:] by CARD_2:def 2
.= alef 0 +` (alef 0)*`N +` N*`(alef 0) by CARD_2:def 2;
(alef 0)*`N <=` alef 0 by A41,Th67;
then alef 0 +` (alef 0)*`N = alef 0 & N*`(alef 0) <=` alef 0
by A42,Th34;
then [:alef 0 \ A,alef 0 \ A:] \/ [:alef 0 \ A,A:] \/
[:A,alef 0 \ A:],alef 0 \ A are_equipotent by A44,A48,CARD_1:21;
then consider g being Function such that
A49: g is one-to-one & dom g = [:alef 0 \ A,alef 0 \ A:] \/
[:alef 0 \ A,A:] \/ [:A,alef 0 \ A:] & rng g = alef 0 \ A
by WELLORD2:def 4;
A50: [:(alef 0 \ A) /\ A,(alef 0 \ A) /\ A:] = {} &
[:(alef 0 \ A) /\ A,A /\ A:] = {} &
[:A /\ A,(alef 0 \ A) /\ A:] = {} by A45,ZFMISC_1:113;
then [:alef 0 \ A,alef 0 \ A:] /\ [:A,A:] = {} & {} \/ {} = {} &
[:alef 0 \ A,A:] /\ [:A,A:] = {} by ZFMISC_1:123;
then ([:alef 0 \ A,alef 0 \ A:] \/ [:alef 0 \ A,A:]) /\ [:A,A:] = {} &
[:A,alef 0 \ A:] /\ [:A,A:] = {} & {} \/ {} = {}
by A50,XBOOLE_1:23,ZFMISC_1:123;
then dom g /\ dom f = {} by A37,A49,XBOOLE_1:23;
then A51: dom g misses dom f by XBOOLE_0:def 7;
then A52: dom (g+*f) = dom g \/ dom f & g <= g+*f & rng f c= rng (g+*f) &
rng (g+*f) c= rng g \/ rng f by FUNCT_4:18,19,33,def 1;
then rng g c= rng (g+*f) by RELAT_1:25;
then rng g \/ rng f c= rng (g+*f) by A52,XBOOLE_1:8;
then A53: rng (g+*f) = rng g \/ rng f by A52,XBOOLE_0:def 10
.= alef 0 \/ A by A49,XBOOLE_1:39;
A54: dom (g+*f) =
[:alef 0 \ A,(alef 0 \ A) \/ A:] \/ [:A,alef 0 \ A:] \/
[:A,A:] by A37,A49,A52,ZFMISC_1:120
.= [:alef 0 \ A,(alef 0 \ A) \/ A:] \/ ([:A,alef 0 \ A:] \/
[:A,A:]) by XBOOLE_1:4
.= [:alef 0 \ A,(alef 0 \ A) \/ A:] \/ [:A,(alef 0 \ A) \/ A:]
by ZFMISC_1:120
.= [:(alef 0 \ A) \/ A,(alef 0 \ A) \/ A:] by ZFMISC_1:120
.= [:alef 0 \/ A,(alef 0 \ A) \/ A:] by XBOOLE_1:39
.= [:alef 0 \/ A,alef 0 \/ A:] by XBOOLE_1:39;
A55: alef 0 \/ A c= M by A5,A37,A38,XBOOLE_1:8;
then [:alef 0 \/ A,alef 0 \/ A:] c= [:M,M:] by ZFMISC_1:119;
then A56: g+*f in PFuncs([:M,M:],M) by A53,A54,A55,PARTFUN1:def 5;
g+*f is one-to-one
proof
rng f misses rng g by A49,XBOOLE_1:79;
then A57: rng f /\ rng g = {} by XBOOLE_0:def 7;
let x,y; assume x in dom (g+*f) & y in dom (g+*f);
then (x in dom f or x in dom g) & (y in dom g or y in dom f)
by A52,XBOOLE_0:def 2;
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 A37,A49,A51,FUNCT_1:def 5,def 8,FUNCT_4:14,17;
hence thesis by A57,XBOOLE_0:def 3;
end;
then g+*f in X & f c= (g+*f) & f = Y & (g+*f) = g+*f
by A2,A37,A53,A54,A56,FUNCT_4:26;
then A58: g+*f = f by A36;
A59: alef 0 \ A <> {} by A41,A43,CARD_2:4;
consider x being Element of alef 0 \ A;
x in alef 0 & not x in A by A59,XBOOLE_0:def 4;
hence contradiction by A53,A58,XBOOLE_0:def 2;
end;
then A60: not N is finite & N <=` M by A39,Th1,CARD_1:27;
A61: now assume N <> M;
then N <` M & M+`N = M by A1,A60,Th34,CARD_1:13;
then Card (M \ A) = M by A39,Th76;
then consider h being Function such that
A62: h is one-to-one & dom h = A & rng h c= M \ A by A60,CARD_1:26;
set B = rng h;
A,B are_equipotent by A62,WELLORD2:def 4;
then A63: N = Card B by CARD_1:21;
N*`N = Card [:N,N:] by CARD_2:def 2;
then [:A,A:],A are_equipotent &
N*`N = Card [:A,A:] by A37,CARD_2:14,WELLORD2:def 4;
then A64: N*`N = N & N+`N = N by A60,Th33,CARD_1:21;
A65: A misses (M \ A) by XBOOLE_1:79;
A /\ B c= A /\ (M \ A) by A62,XBOOLE_1:26;
then A /\ B c= {} by A65,XBOOLE_0:def 7;
then A /\ B = {} & A /\ B = B /\ A by XBOOLE_1:3;
then A66: A misses B & A /\ B = B /\ A by XBOOLE_0:def 7;
then Card (A \/ B) = N by A63,A64,CARD_2:48;
then A67: Card [:A \/ B,A \/ B:] = Card [:N,N:] by CARD_2:14 .= N
by A64,CARD_2:def 2;
(A \/ B) \ A = B \ A by XBOOLE_1:40
.= B by A66,XBOOLE_1:83;
then A68: B c= A \/ B & A c= A \/ B & B c= (A \/ B) \ A by XBOOLE_1:7;
then [:(A \/ B) \ A,A \/ B:] c= [:(A \/ B) \ A,A \/ B:] \/ [:A \/ B,(A
\/
B) \ A:] &
[:B,B:] c= [:(A \/ B) \ A,A \/ B:] & [:A \/ B,A \/ B:] \ [:A,A:] =
[:(A \/ B) \ A,A \/ B:] \/ [:A \/ B,(A \/ B) \ A:] & N = Card [:N,N:]
by A64,CARD_2:def 2,XBOOLE_1:7,ZFMISC_1:119,126;
then [:B,B:] c= [:A \/ B,A \/ B:] \ [:A,A:] & N = Card [:B,B:] &
[:A \/ B,A \/ B:] \ [:A,A:] c= [:A \/ B,A \/ B:]
by A63,CARD_2:14,XBOOLE_1:1,36;
then N <=` Card ([:A \/ B,A \/ B:] \ [:A,A:]) &
Card ([:A \/ B,A \/ B:] \ [:A,A:]) <=` N by A67,CARD_1:27;
then Card ([:A \/ B,A \/ B:] \ [:A,A:]) = N by XBOOLE_0:def 10;
then [:A \/ B,A \/ B:] \ [:A,A:],B are_equipotent by A63,CARD_1:21;
then consider g such that
A69: g is one-to-one & dom g = [:A \/ B,A \/ B:] \ [:A,A:] & rng g = B
by WELLORD2:def 4;
A70: ([:A \/ B,A \/ B:] \ [:A,A:]) misses [:rng f,rng f:] by XBOOLE_1:79
;
then g <= g+*f by A37,A69,FUNCT_4:33;
then rng f c= rng (g+*f) & rng g c= rng (g+*f) by FUNCT_4:19,RELAT_1:25;
then rng g \/ rng f c= rng(g+*f) & rng(g+*f) c= rng g \/ rng f
by FUNCT_4:18,XBOOLE_1:8;
then A71: rng (g+*f) = rng g \/ rng f by XBOOLE_0:def 10;
A72: dom (g+*f) = dom g \/ dom f by FUNCT_4:def 1;
then dom (g+*f) = [:A \/ B,A \/ B:] \/ [:A,A:] & [:A,A:] c= [:A \/ B,A
\/ B:]
by A37,A68,A69,XBOOLE_1:39,ZFMISC_1:119;
then A73: dom (g+*f) = [:A \/ B,A \/ B:] by XBOOLE_1:12;
M \ A c= M by XBOOLE_1:36;
then B c= M by A62,XBOOLE_1:1;
then A74: A \/ B c= M by A37,A38,XBOOLE_1:8;
then [:A \/ B,A \/ B:] c= [:M,M:] by ZFMISC_1:119;
then A75: g+*f in PFuncs([:M,M:],M) by A69,A71,A73,A74,PARTFUN1:def 5;
g+*f is one-to-one
proof
A76: A misses (M \ A) by XBOOLE_1:79;
A /\ B c= A /\ (M \ A) by A62,XBOOLE_1:26;
then rng f /\ rng g c= {} by A69,A76,XBOOLE_0:def 7;
then A77: rng f /\ rng g = {} by XBOOLE_1:3;
let x,y; assume x in dom (g+*f) & y in dom (g+*f);
then (x in dom f or x in dom g) & (y in dom g or y in dom f)
by A72,XBOOLE_0:def 2;
then A78: (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 A37,A69,A70,FUNCT_1:def 5,def 8,FUNCT_4:14,17;
assume (g+*f).x = (g+*f).y;
hence thesis by A77,A78,XBOOLE_0:def 3;
end;
then A79: g+*f in X & f c= (g+*f) & f = Y & (g+*f) = g+*f
by A2,A37,A69,A71,A73,A75,FUNCT_4:26;
A80: B <> {} by A60,A63,Th1;
consider x being Element of B;
x in M \ A by A62,A80,TARSKI:def 3;
then not x in rng f & x in rng (g+*f) by A69,A71,A80,XBOOLE_0:def 2,def 4
;
hence contradiction by A36,A79;
end;
then A81: M*`M = Card [:N,N:] by CARD_2:def 2 .= Card [:A,A:] by CARD_2:14;
[:A,A:],A are_equipotent by A37,WELLORD2:def 4;
hence thesis by A61,A81,CARD_1:21;
end;
theorem
Th78: not M is finite & 0 <` N & (N <=` M or N <` M)
implies M*`N = M & N*`M = M
proof assume not M is finite;
then A1: M*`M = M by Th77;
assume
A2: 0 <` N;
assume N <=` M or N <` M;
then N <=` M & 1 <=` N & M <=` M by A2,Th24,CARD_1:13;
then 1*`M <=` N*`M & N*`M <=` M*`M & 1*`M = M & N*`M = M*`N
by Th68,CARD_2:33;
hence thesis by A1,XBOOLE_0:def 10;
end;
theorem
Th79: not M is finite & (N <=` M or N <` M) implies M*`N <=` M & N*`M <=` M
proof assume not M is finite & (N <=` M or N <` M);
then M*`N = M or not 0 <` N by Th78;
then M*`N <=` M or N = 0 & M*`0 = 0 & 0 <=` M
by Th19,CARD_2:32,ORDINAL3:10;
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 not Card X is finite by Th1;
then (Card X)*`(Card X) = Card X by Th77;
then Card [:Card X,Card X:] = Card X by CARD_2:def 2;
then Card [:X,X:] = Card X by CARD_2:14;
hence thesis by CARD_1:21;
end;
theorem
not X is finite & Y is finite & Y <> {} implies
[:X,Y:],X are_equipotent & Card [:X,Y:] = Card X
proof assume not X is finite & Y is finite & Y <> {};
then A1: not Card X is finite & Card Y is finite & Card Y <> 0 by Th1,CARD_2:
59;
then Card Y <=` Card X & 0 <` Card Y by Th13,ORDINAL3:10;
then (Card X)*`(Card Y) = Card X by A1,Th78;
then Card [:Card X,Card Y:] = Card X by CARD_2:def 2;
then Card [:X,Y:] = Card X by CARD_2:14;
hence thesis by CARD_1:21;
end;
theorem
K <` L & M <` N implies K*`M <` L*`N & M*`K <` L*`N
proof
A1: for K,L,M,N st K <` L & M <` N & L <=` N holds K*`M <` L*`N
proof let K,L,M,N; assume
A2: K <` L & M <` N & L <=` N;
then A3: 0 <` L by ORDINAL3:10;
A4: now assume
A5: N is finite;
then reconsider N as finite Cardinal;
reconsider L,M,K as finite Cardinal by A2,A5,Th26;
Card K = Card card K & Card K = K & Card L = L & Card M = M &
Card N = N by CARD_1:def 5;
then A6: K*`M = Card (card K * card M) & L*`N = Card (card L * card N) &
card K < card L & card M < card N & 0 <= card K & 0 <= card M
by A2,CARD_1:73,CARD_2:52,NAT_1:18;
then card K * card M <= card K * card N &
card K * card N < card L * card N by AXIOMS:25,REAL_1:70;
then card K * card M < card L * card N by AXIOMS:22;
hence thesis by A6,CARD_1:73;
end;
now assume not N is finite;
then A7: L*`N = N & omega c= N by A2,A3,Th11,Th78,CARD_1:83;
K,M are_c=-comparable by ORDINAL1:25;
then K <=` M & (M is finite or not M is finite) or
M <=` K & (K is finite or not K is finite) by XBOOLE_0:def 9;
then A8: K is finite & M is finite or K*`M <=` M or K*`M <=` K & K <` N
by A2,Th26,Th79;
now assume K is finite & M is finite;
then reconsider K,M as finite Cardinal;
Card K = Card card K & Card M = Card card M &
Card K = K & Card M = M by CARD_1:def 5;
then K*`M = Card (card K * card M) by CARD_2:52
.= (card K * card M) by CARD_1:def 5;
hence thesis by A7,TARSKI:def 3;
end;
hence thesis by A2,A7,A8,ORDINAL1:22;
end;
hence K*`M <` L*`N by A4;
end;
L,N are_c=-comparable by ORDINAL1:25;
then K*`M = M*`K & L*`N = N*`L & (L <=` N or N <=` L)
by XBOOLE_0:def 9;
hence thesis by A1;
end;
theorem
K*`M <` K*`N implies M <` N
proof assume
A1: K*`M <` K*`N & not M <` N;
then N <=` M & K <=` K by CARD_1:14;
then K*`N <=` K*`M by Th68;
hence thesis by A1,CARD_1:14;
end;
theorem
Th84: not X is finite implies Card X = (alef 0)*`Card X
proof assume not X is finite;
then A1: not Card X is finite by Th1;
then 0 <` alef 0 & alef 0 <=` Card X
by Th11,CARD_1:83;
hence thesis by A1,Th78;
end;
theorem
X <> {} & X is finite & not Y is finite implies Card Y *` Card X = Card Y
proof assume X <> {} & X is finite & not Y is finite;
then A1: Card X <> 0 & Card X is finite & not Card Y is finite by Th1,CARD_2:
59;
then Card X <` Card Y & 0 <` Card X by Th13,ORDINAL3:10;
hence thesis by A1,Th78;
end;
theorem
Th86: not D is finite & n <> 0 implies n-tuples_on D,D are_equipotent &
Card (n-tuples_on D) = Card D
proof assume
A1: not D is finite & n <> 0;
then A2: not Card D is finite by Th1;
defpred P[Nat] means $1 <> 0 implies Card ($1-tuples_on D) = Card D;
A3: P[0];
A4: P[k] implies P[k+1]
proof assume that
A5: P[k];
A6: Card ((k+1)-tuples_on D)
= Card [:(k-tuples_on D),1-tuples_on D:] by Th57
.= Card [:Card (k-tuples_on D),Card (1-tuples_on D):] by CARD_2:14
.= Card [:Card (k-tuples_on D),Card D:] by Th56
.= Card (k-tuples_on D) *` Card D by CARD_2:def 2;
A7: 0-tuples_on D = { <*>D } by FINSEQ_2:112;
then A8: Card (0-tuples_on D) <> 0 & 0-tuples_on D is finite by CARD_2:59;
Card (0-tuples_on D) is finite by A7,Th1;
then 0 <` Card (0-tuples_on D) & Card (0-tuples_on D) <=` Card D
by A2,A8,Th13,ORDINAL3:10;
hence thesis by A2,A5,A6,Th78;
end;
P[k] from Ind(A3,A4);
then Card (n-tuples_on D) = Card D by A1;
hence thesis by CARD_1:21;
end;
theorem
not D is finite implies Card D = Card (D*)
proof assume
A1: not D is finite;
deffunc f(Nat) = $1-tuples_on D;
defpred P[set] means not contradiction;
{f(k): P[k]} is countable from FraenCoun1;
then A2: Card {k-tuples_on D: not contradiction} <=` alef 0 by Def1;
for X st X in {k-tuples_on D: not contradiction} holds Card X <=` Card D
proof let X; assume X in {k-tuples_on D: not contradiction};
then consider k such that
A3: X = k-tuples_on D;
0-tuples_on D = { <*>D } by FINSEQ_2:112;
then Card (0-tuples_on D) is finite & not Card D is finite by A1,Th1;
then Card (0-tuples_on D) <=` Card D & k = 0 or k <> 0 by Th13;
hence Card X <=` Card D by A1,A3,Th86;
end;
then A4: Card union {k-tuples_on D: not contradiction} <=` alef 0 *` Card D
by A2,Th60;
A5: D* = union {k-tuples_on D: not contradiction} by FINSEQ_2:128;
then A6: Card (D*) <=` Card D by A1,A4,Th84;
1-tuples_on D in {k-tuples_on D: not contradiction};
then 1-tuples_on D c= D* by A5,ZFMISC_1:92;
then Card (1-tuples_on D) <=` Card (D*) by CARD_1:27;
then Card D <=` Card (D*) by Th56;
hence thesis by A6,XBOOLE_0:def 10;
end;