The abstract of the Mizar article:

Countable Sets and Hessenberg's Theorem

by

Grzegorz Bancerek

Received September 5, 1990

MML identifier: CARD_4

[ Mizar article, 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;


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;

theorem :: CARD_4:1
  X is finite iff Card X is finite;

theorem :: CARD_4:2
  X is finite iff Card X <` alef 0;

theorem :: CARD_4:3
    X is finite implies Card X in alef 0 & Card X in omega;

theorem :: CARD_4:4
    X is finite iff ex n st Card X = Card n;

theorem :: CARD_4:5
  succ A \ {A} = A;

theorem :: CARD_4:6
  A,n are_equipotent implies A = n;

theorem :: CARD_4:7
  A is finite iff A in omega;

theorem :: CARD_4:8
   not A is finite iff omega c= A;

theorem :: CARD_4:9
    M is finite iff M in alef 0;

canceled;

theorem :: CARD_4:11
  not M is finite iff alef 0 c= M;

canceled;

theorem :: CARD_4:13
  N is finite & not M is finite implies N <` M & N <=` M;

theorem :: CARD_4:14
   not X is finite iff ex Y st Y c= X & Card Y = alef 0;

theorem :: CARD_4:15
  not omega is finite & not NAT is finite;

theorem :: CARD_4:16
    not alef 0 is finite;

theorem :: CARD_4:17
    X = {} iff Card X = 0;

canceled;

theorem :: CARD_4:19
  0 <=` M;

theorem :: CARD_4:20
  Card X = Card Y iff nextcard X = nextcard Y;

theorem :: CARD_4:21
   M = N iff nextcard N = nextcard M;

theorem :: CARD_4:22
  N <` M iff nextcard N <=` M;

theorem :: CARD_4:23
   N <` nextcard M iff N <=` M;

theorem :: CARD_4:24
  0 <` M iff 1 <=` M;

theorem :: CARD_4:25
   1 <` M iff 2 <=` M;

theorem :: CARD_4:26
  M is finite & (N <=` M or N <` M) implies N is finite;

theorem :: CARD_4:27
  A is_limit_ordinal iff for B,n st B in A holds B+^ n in A;

theorem :: CARD_4:28
  A+^succ n = succ A +^ n & A +^ (n+1) = succ A +^ n;

theorem :: CARD_4:29
  ex n st A*^succ one = A +^ n;

theorem :: CARD_4:30
  A is_limit_ordinal implies A *^ succ one = A;

theorem :: CARD_4:31
  omega c= A implies one+^A = A;

theorem :: CARD_4:32
  M is infinite implies M is_limit_ordinal;

theorem :: CARD_4:33
  not M is finite implies M+`M = M;

theorem :: CARD_4:34
  not M is finite & (N <=` M or N <` M) implies M+`N = M & N+`M = M;

theorem :: CARD_4:35
   not X is finite & (X,Y are_equipotent or Y,X are_equipotent) implies
 X \/ Y,X are_equipotent & Card (X \/ Y) = Card X;

theorem :: CARD_4:36
   not X is finite & Y is finite implies
  X \/ Y,X are_equipotent & Card (X \/ Y) = Card X;

theorem :: CARD_4:37
   not X is finite & (Card Y <` Card X or Card Y <=` Card X) implies
   X \/ Y,X are_equipotent & Card (X \/ Y) = Card X;

theorem :: CARD_4:38
   for M,N being finite Cardinal holds M+`N is finite;

theorem :: CARD_4:39
   not M is finite implies not M+`N is finite & not N+`M is finite;

theorem :: CARD_4:40
   for M,N being finite Cardinal holds M*`N is finite;

theorem :: CARD_4:41
 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;

theorem :: CARD_4:42
   M <` N or M <=` N implies K+`M <=` K+`N & K+`M <=` N+`K &
 M+`K <=` K+`N & M+`K <=` N+`K;

 definition let X;
  attr X is countable means
:: CARD_4:def 1
   Card X <=` alef 0;
 end;

theorem :: CARD_4:43
  X is finite implies X is countable;

theorem :: CARD_4:44
  omega is countable & NAT is countable;

theorem :: CARD_4:45
  X is countable iff ex f st dom f = NAT & X c= rng f;

theorem :: CARD_4:46
  Y c= X & X is countable implies Y is countable;

theorem :: CARD_4:47
  X is countable & Y is countable implies X \/ Y is countable;

theorem :: CARD_4:48
   X is countable implies X /\ Y is countable & Y /\ X is countable;

theorem :: CARD_4:49
  X is countable implies X \ Y is countable;

theorem :: CARD_4:50
   X is countable & Y is countable implies X \+\ Y is countable;

 reserve r for Real;

theorem :: CARD_4:51
  r <> 0 or n = 0 iff r|^n <> 0;

 definition let m,n be Nat;
  redefine func m|^n -> Nat;
 end;

theorem :: CARD_4:52
  (2|^n1)*(2*m1+1) = (2|^n2)*(2*m2+1) implies n1 = n2 & m1 = m2;

theorem :: CARD_4:53
  [:NAT,NAT:],NAT are_equipotent & Card NAT = Card [:NAT,NAT:];

theorem :: CARD_4:54
  (alef 0)*`(alef 0) = alef 0;

theorem :: CARD_4:55
  X is countable & Y is countable implies [:X,Y:] is countable;

theorem :: CARD_4:56
  1-tuples_on D,D are_equipotent & Card (1-tuples_on D) = Card D;

 reserve p,q for FinSequence;

theorem :: CARD_4:57
  [: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);

theorem :: CARD_4:58
  D is countable implies n-tuples_on D is countable;

theorem :: CARD_4:59
  (Card dom f <=` M & for x st x in dom f holds Card (f.x) <=` N) implies
   Card Union f <=` M*`N;

theorem :: CARD_4:60
 (Card X <=` M & for Y st Y in X holds Card Y <=` N) implies Card union X <=`
 M*`N;

theorem :: CARD_4:61
  for f st dom f is countable &
   for x st x in dom f holds f.x is countable holds Union f is countable;

theorem :: CARD_4:62
   (X is countable & for Y st Y in X holds Y is countable) implies
   union X is countable;

theorem :: CARD_4:63
    for f st dom f is finite &
   for x st x in dom f holds f.x is finite holds Union f is finite;

canceled;

theorem :: CARD_4:65
   D is countable implies D* is countable;

theorem :: CARD_4:66
   alef 0 <=` Card (D*);

scheme FraenCoun1 { f(set)->set, P[Nat] } :
 { f(n) : P[n] } is countable;

scheme FraenCoun2 { f(set,set)->set, P[set,set] } :
 { f(n1,n2) : P[n1,n2] } is countable;

scheme FraenCoun3 { f(set,set,set)->set, P[Nat,Nat,Nat] } :
 { f(n1,n2,n3) : P[n1,n2,n3] } is countable;

theorem :: CARD_4:67
  (alef 0)*`(Card n) <=` alef 0 & (Card n)*`(alef 0) <=` alef 0;

theorem :: CARD_4:68
 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;

theorem :: CARD_4:69
   M <` N or M <=` N implies
  K*`M <=` K*`N & K*`M <=` N*`K & M*`K <=` K*`N & M*`K <=` N*`K;

theorem :: CARD_4:70
 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);

theorem :: CARD_4:71
   M <` N or M <=` N implies K = 0 or
 exp(K,M) <=` exp(K,N) & exp(M,K) <=` exp(N,K);

theorem :: CARD_4:72
  M <=` M+`N & N <=` M+`N;

theorem :: CARD_4:73
    N <> 0 implies M <=` M*`N & M <=` N*`M;

theorem :: CARD_4:74
  K <` L & M <` N implies K+`M <` L+`N & M+`K <` L+`N;

theorem :: CARD_4:75
   K+`M <` K+`N implies M <` N;

theorem :: CARD_4:76
 Card X +` Card Y = Card X & Card Y <` Card X implies Card (X \ Y) = Card X;

 reserve f,f1,f2 for Function, X1,X2 for set;

:: Hessenberg's theorem

theorem :: CARD_4:77
  not M is finite implies M*`M = M;

theorem :: CARD_4:78
  not M is finite & 0 <` N & (N <=` M or N <` M)
  implies M*`N = M & N*`M = M;

theorem :: CARD_4:79
  not M is finite & (N <=` M or N <` M) implies M*`N <=` M & N*`M <=` M;

theorem :: CARD_4:80
   not X is finite implies [:X,X:],X are_equipotent & Card [:X,X:] = Card X;

theorem :: CARD_4:81
   not X is finite & Y is finite & Y <> {} implies
   [:X,Y:],X are_equipotent & Card [:X,Y:] = Card X;

theorem :: CARD_4:82
   K <` L & M <` N implies K*`M <` L*`N & M*`K <` L*`N;

theorem :: CARD_4:83
   K*`M <` K*`N implies M <` N;

theorem :: CARD_4:84
  not X is finite implies Card X = (alef 0)*`Card X;

theorem :: CARD_4:85
   X <> {} & X is finite & not Y is finite implies Card Y *` Card X = Card Y;

theorem :: CARD_4:86
  not D is finite & n <> 0 implies n-tuples_on D,D are_equipotent &
   Card (n-tuples_on D) = Card D;

theorem :: CARD_4:87
   not D is finite implies Card D = Card (D*);