### The Mizar article:

### Countable Sets and Hessenberg's Theorem

**by****Grzegorz Bancerek**

- Received September 5, 1990
Copyright (c) 1990 Association of Mizar Users

- MML identifier: CARD_4
- [ MML identifier index ]

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;

Back to top