The abstract of the Mizar article:

Finite Sets

by

Agata Darmochwal

Received April 6, 1989

MML identifier: FINSET_1

[ Mizar article, MML identifier index ]

environ

 vocabulary FUNCT_1, RELAT_1, ORDINAL2, BOOLE, ORDINAL1, ORDINAL3, SETFAM_1,
      TARSKI, MCART_1, FINSET_1;
 notation TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1,
      MCART_1, SETFAM_1, ORDINAL1, ORDINAL2, ORDINAL3;
 constructors ENUMSET1, MCART_1, ORDINAL3, SETFAM_1, XBOOLE_0;
 clusters FUNCT_1, ORDINAL2, RELAT_1, ARYTM_3, ORDINAL1, SUBSET_1, ZFMISC_1,
      XBOOLE_0;
 requirements SUBSET, BOOLE;


begin

 definition let IT be set;
  attr IT is finite means
:: FINSET_1:def 1
    ex p being Function st rng p = IT & dom p in omega;
  antonym IT is infinite;
 end;

 reserve A, B, C, D, X, Y, Z, x, y for set;
 reserve f for Function;

definition
 cluster non empty finite set;
end;

definition
 cluster empty -> finite set;
end;

definition let X be set;
 cluster empty finite Subset of X;
end;

scheme OLambdaC{A()->set,C[set],F(set)->set,G(set)->set}:
 ex f being Function st dom f = A() &
  for x being Ordinal st x in A() holds
   (C[x] implies f.x = F(x)) & (not C[x] implies f.x = G(x));

definition let x be set;
 cluster {x} -> finite;
end;

definition let X be non empty set;
 cluster non empty finite Subset of X;
end;

definition
  let x,y be set;
  cluster {x,y} -> finite;
end;

definition
  let x,y,z be set;
  cluster {x,y,z} -> finite;
end;

definition
  let x1,x2,x3,x4 be set;
  cluster {x1,x2,x3,x4} -> finite;
end;

definition
  let x1,x2,x3,x4,x5 be set;
  cluster {x1,x2,x3,x4,x5} -> finite;
end;

definition
  let x1,x2,x3,x4,x5,x6 be set;
  cluster {x1,x2,x3,x4,x5,x6} -> finite;
end;

definition
  let x1,x2,x3,x4,x5,x6,x7 be set;
  cluster {x1,x2,x3,x4,x5,x6,x7} -> finite;
end;

definition
  let x1,x2,x3,x4,x5,x6,x7,x8 be set;
  cluster {x1,x2,x3,x4,x5,x6,x7,x8} -> finite;
end;

definition let B be finite set;
 cluster -> finite Subset of B;
end;

definition let X,Y be finite set;
 cluster X \/ Y -> finite;
end;

canceled 12;

theorem :: FINSET_1:13
 A c= B & B is finite implies A is finite;

theorem :: FINSET_1:14
   A is finite & B is finite implies A \/ B is finite;

definition let A be set, B be finite set;
 cluster A /\ B -> finite;
end;

definition let A be finite set, B be set;
 cluster A /\ B -> finite;
 cluster A \ B -> finite;
end;

theorem :: FINSET_1:15
 A is finite implies A /\ B is finite;

theorem :: FINSET_1:16
   A is finite implies A \ B is finite;

theorem :: FINSET_1:17
 A is finite implies f.:A is finite;

definition let f be Function, A be finite set;
 cluster f.:A -> finite;
end;

reserve O for Ordinal;

theorem :: FINSET_1:18
 A is finite implies for X being Subset-Family of A st X <> {}
  ex x being set st
   x in X & for B being set st B in X holds x c= B implies B = x;

scheme Finite{A()->set,P[set]} : P[A()]
  provided
  A() is finite and
  P[{}] and
  for x,B being set st x in A() & B c= A() & P[B] holds P[B \/ {x}];

theorem :: FINSET_1:19
 A is finite & B is finite implies [:A,B:] is finite;

definition let A,B be finite set;
 cluster [:A,B:] -> finite;
end;

theorem :: FINSET_1:20
 A is finite & B is finite & C is finite
  implies [:A,B,C:] is finite;

definition let A,B,C be finite set;
 cluster [:A,B,C:] -> finite;
end;

theorem :: FINSET_1:21
 A is finite & B is finite & C is finite & D is finite
  implies [:A,B,C,D:] is finite;

definition let A,B,C,D be finite set;
 cluster [:A,B,C,D:] -> finite;
end;

theorem :: FINSET_1:22
   B <> {} & [:A,B:] is finite implies A is finite;

theorem :: FINSET_1:23
   A <> {} & [:A,B:] is finite implies B is finite;

theorem :: FINSET_1:24
 A is finite iff bool A is finite;

theorem :: FINSET_1:25
   A is finite & (for X st X in A holds X is finite) iff union A is finite;

theorem :: FINSET_1:26
   dom f is finite implies rng f is finite;

theorem :: FINSET_1:27
   Y c= rng f & f"Y is finite implies Y is finite;