:: Cardinal Numbers
::  by Grzegorz Bancerek
::
:: Received September 19, 1989
:: Copyright (c) 1990-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies ORDINAL1, RELAT_1, FUNCT_1, XBOOLE_0, TARSKI, WELLORD1, WELLORD2,
      ZFMISC_1, ORDINAL2, FUNCOP_1, FINSET_1, SUBSET_1, MCART_1, CARD_1,
      BSPACE, NAT_1, XCMPLX_0, FUNCT_4, QUANTAL1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, ENUMSET1, XTUPLE_0,
      MCART_1, FUNCT_1, FUNCOP_1, WELLORD1, ORDINAL1, ORDINAL2, WELLORD2,
      FINSET_1, FUNCT_4;
 constructors ENUMSET1, WELLORD1, WELLORD2, FUNCOP_1, ORDINAL2, FINSET_1,
      XTUPLE_0, FUNCT_4;
 registrations XBOOLE_0, SUBSET_1, FUNCT_1, ORDINAL1, FUNCOP_1, FINSET_1,
      ZFMISC_1, XTUPLE_0, FUNCT_4;
 requirements NUMERALS, SUBSET, BOOLE;


begin

reserve A,B,C for Ordinal,
  X,X1,Y,Y1,Z for set,a,b,b1,b2,x,y,z for object,
  R for Relation,
  f,g,h for Function,
  k,m,n for Nat;

definition
  let IT be object;
  attr IT is cardinal means
:: CARD_1:def 1

  ex B st IT = B & for A st A,B are_equipotent holds B c= A;
end;

registration
  cluster cardinal for set;
end;

definition
  mode Cardinal is cardinal set;
end;

registration
  cluster cardinal -> ordinal for set;
end;

reserve M,N for Cardinal;

::$CT

theorem :: CARD_1:2
  M,N are_equipotent implies M = N;

theorem :: CARD_1:3
  M in N iff M c= N & M <> N;

theorem :: CARD_1:4
  M in N iff not N c= M;

definition
  let X;
  func card X -> Cardinal means
:: CARD_1:def 2

    X, it are_equipotent;
  projectivity;
end;

registration let C be Cardinal;
 reduce card C to C;
end;

registration
  cluster empty -> cardinal for set;
end;

registration
  let X be empty set;
  cluster card X -> empty;
end;

registration
  let X be empty set;
  cluster card X -> zero;
end;

registration
  let X be non empty set;
  cluster card X -> non empty;
end;

registration
  let X be non empty set;
  cluster card X -> non zero;
end;

theorem :: CARD_1:5
  X,Y are_equipotent iff card X = card Y;

theorem :: CARD_1:6
  R is well-ordering implies field R,order_type_of R
  are_equipotent;

theorem :: CARD_1:7
  X c= M implies card X c= M;

theorem :: CARD_1:8
  card A c= A;

theorem :: CARD_1:9
  X in M implies card X in M;

::$N Cantor-Bernstein Theorem
theorem :: CARD_1:10
  card X c= card Y iff ex f st f is one-to-one & dom f = X & rng f c= Y;

theorem :: CARD_1:11
  X c= Y implies card X c= card Y;

theorem :: CARD_1:12
  card X c= card Y iff ex f st dom f = Y & X c= rng f;

theorem :: CARD_1:13
  not X,bool X are_equipotent;

::$N Cantor Theorem
theorem :: CARD_1:14
  card X in card bool X;

definition
  let X;
  func nextcard X -> Cardinal means
:: CARD_1:def 3

  card X in it & for M st card X in M holds it c= M;
end;

theorem :: CARD_1:15
  {} in nextcard X;

theorem :: CARD_1:16
  card X = card Y implies nextcard X = nextcard Y;

theorem :: CARD_1:17
  X,Y are_equipotent implies nextcard X = nextcard Y;

theorem :: CARD_1:18
  A in nextcard A;

reserve S for Sequence;

definition
  let M;
  attr M is limit_cardinal means
:: CARD_1:def 4

  not ex N st M = nextcard N;
end;

definition
  let A;
  func aleph A -> set means
:: CARD_1:def 5

  ex S st it = last S & dom S = succ A & S.0 = card omega &
  (for B st succ B in succ A holds S.succ B = nextcard(S.B)) &
  for B st B in succ A & B <> 0 & B is limit_ordinal holds S.B = card sup(S|B);
end;

registration
  let A;
  cluster aleph A -> cardinal;
end;

theorem :: CARD_1:19
  aleph succ A = nextcard aleph A;

theorem :: CARD_1:20
  A <> {} & A is limit_ordinal implies for S st dom S = A & for B st B
  in A holds S.B = aleph B holds aleph A = card sup S;

theorem :: CARD_1:21
  A in B iff aleph A in aleph B;

theorem :: CARD_1:22
  aleph A = aleph B implies A = B;

theorem :: CARD_1:23
  A c= B iff aleph A c= aleph B;

theorem :: CARD_1:24
  X c= Y & Y c= Z & X,Z are_equipotent implies X,Y are_equipotent & Y,Z
  are_equipotent;

theorem :: CARD_1:25
  bool Y c= X implies card Y in card X & not Y,X are_equipotent;

theorem :: CARD_1:26
  X,{} are_equipotent implies X = {};

theorem :: CARD_1:27
 card {} = 0;

theorem :: CARD_1:28
 for x being object  holds
  X,{x} are_equipotent iff ex x being object st X = { x };

theorem :: CARD_1:29
 for x being object holds
  card X = card { x } iff ex x being object st X = { x };

theorem :: CARD_1:30
 for x being object holds card { x } = 1;

theorem :: CARD_1:31
  X misses X1 & Y misses Y1 & X,Y are_equipotent & X1,Y1
  are_equipotent implies X \/ X1,Y \/ Y1 are_equipotent;

theorem :: CARD_1:32
  x in X & y in X implies X \ { x },X \ { y } are_equipotent;

theorem :: CARD_1:33
  X c= dom f & f is one-to-one implies X,f.:X are_equipotent;

theorem :: CARD_1:34
  X,Y are_equipotent & x in X & y in Y implies X \ { x },Y \ { y }
  are_equipotent;

theorem :: CARD_1:35
  succ X, succ Y are_equipotent implies X, Y are_equipotent;

theorem :: CARD_1:36
  n = {} or ex m st n = succ m;

theorem :: CARD_1:37
  x in omega implies x is cardinal;

registration
  cluster natural -> cardinal for number;
end;

theorem :: CARD_1:38
  X,Y are_equipotent & X is finite implies Y is finite;

theorem :: CARD_1:39
  n is finite & card n is finite;

theorem :: CARD_1:40
  card n = card m implies n = m;

theorem :: CARD_1:41
  card n c= card m iff n c= m;

theorem :: CARD_1:42
  card n in card m iff n in m;

::$CT

theorem :: CARD_1:44
  nextcard card n = card succ n;

:: definition
::   let n be Nat;
::   redefine func succ n -> Element of omega;
::   coherence by ORDINAL1:def 12;
:: end;

definition
  let X be finite set;
  redefine func card X -> Element of omega;
end;

theorem :: CARD_1:45
  X is finite implies nextcard X is finite;

scheme :: CARD_1:sch 1
  CardinalInd { Sigma[set] }: for M holds Sigma[M]
provided
 Sigma[{}] and
 for M st Sigma[M] holds Sigma[nextcard M] and
 for M st M <> {} & M is limit_cardinal & for N st N in M holds Sigma
[N] holds Sigma[M];

scheme :: CARD_1:sch 2
  CardinalCompInd { Sigma[set] }: for M holds Sigma[M]
provided
 for M st for N st N in M holds Sigma[N] holds Sigma[M];

theorem :: CARD_1:46
  aleph 0 = omega;

registration
  cluster omega -> cardinal for number;
end;

theorem :: CARD_1:47
  card omega = omega;

registration
  cluster omega -> limit_cardinal;
end;

registration
  cluster -> finite for Element of omega;
end;

registration
  cluster finite for Cardinal;
end;

theorem :: CARD_1:48
  for M being finite Cardinal ex n st M = card n;

registration
  let X be finite set;
  cluster card X -> finite;
end;

registration
  cluster omega -> infinite;
end;

registration
  cluster infinite for set;
end;

registration
  let X be infinite set;
  cluster card X -> infinite;
end;

begin :: The meaning of numerals, 2006.08.25

theorem :: CARD_1:49
  1 = { 0 };

theorem :: CARD_1:50
  2 = { 0,1 };

theorem :: CARD_1:51
  3 = { 0,1,2 };

theorem :: CARD_1:52
  4 = { 0,1,2,3 };

theorem :: CARD_1:53
  5 = { 0,1,2,3,4 };

theorem :: CARD_1:54
  6 = { 0,1,2,3,4,5 };

theorem :: CARD_1:55
  7 = { 0,1,2,3,4,5,6 };

theorem :: CARD_1:56
  8 = { 0,1,2,3,4,5,6,7 };

theorem :: CARD_1:57
  9 = { 0,1,2,3,4,5,6,7,8 };

theorem :: CARD_1:58
  10 = { 0,1,2,3,4,5,6,7,8,9 };

:: Moved from FRECHET2 by AK on 27.12.2006

theorem :: CARD_1:59
  for f being Function st dom f is infinite & f is one-to-one holds rng
  f is infinite;

:: from ALGSEQ_1, 2007.03.18, A.T.

reserve k,n,m for Nat;

registration
 cluster non zero natural for object;
 cluster non zero for Nat;
end;

registration let n be non zero natural Number;
 cluster Segm n -> non empty;
end;

reserve l for Element of omega;

definition
  let n be natural Number;
  redefine func Segm n -> Subset of omega;
end;

:: from CARD_4, 2007.08.16, A.T.

theorem :: CARD_1:60
  A,n are_equipotent implies A = n;

theorem :: CARD_1:61
  A is finite iff A in omega;

registration
  cluster natural -> finite for set;
end;

:: from CARD_4, CARD_5 etc. 2008.02.21, A.T.

registration
  let A be infinite set;
  cluster bool A -> infinite;
  let B be non empty set;
  cluster [:A,B:] ->infinite;
  cluster [:B,A:] ->infinite;
end;

registration
  let X be infinite set;
  cluster infinite for Subset of X;
end;

:: from NECKLA_2, 2008.06.28, A.T.

registration
  cluster finite ordinal -> natural for number;
end;

theorem :: CARD_1:62
  for f being Function holds card f = card dom f;

registration
  let X be finite set;
  cluster RelIncl X -> finite;
end;

:: from AMISTD_2, 2010.01.10, A.T

theorem :: CARD_1:63
  RelIncl X is finite implies X is finite;

theorem :: CARD_1:64
 card(k -->x) = k;

begin :: n-element set, 2010.11.17, A.T.

definition
::$CD
 let N be object, X be set;
 attr X is N-element means
:: CARD_1:def 7
 card X = N;
end;

registration let N be Cardinal;
 cluster N-element for set;
end;

registration
 cluster 0-element -> empty for set;
 cluster empty -> 0-element for set;
end;

registration let x be object;
 cluster {x} -> 1-element;
end;

registration let N be Cardinal;
 cluster N-element for Function;
end;

registration let N be Cardinal; let f be N-element Function;
 cluster dom f -> N-element;
end;

registration
 cluster 1-element -> trivial non empty for set;
 cluster trivial non empty -> 1-element for set;
end;

registration let X be non empty set;
 cluster 1-element for Subset of X;
end;

definition let X be non empty set;
 mode Singleton of X is 1-element Subset of X;
end;

theorem :: CARD_1:65
 for X being non empty set, A being Singleton of X
  ex x being Element of X st A = {x};

theorem :: CARD_1:66
  card X c= card Y iff ex f st X c= f.:Y;

theorem :: CARD_1:67
  card (f.:X) c= card X;

theorem :: CARD_1:68
  card X in card Y implies Y \ X <> {};

theorem :: CARD_1:69
 for x being object holds
  X,[:X,{x}:] are_equipotent & card X = card [:X,{x}:];

:: from POLYFORM, 2011.07.25, A.T.

theorem :: CARD_1:70
  for f being Function st f is one-to-one holds card dom f = card rng f;

registration
  let F be non trivial set;
  let A be Singleton of F;
  cluster F\A -> non empty;
end;

registration let k be non empty Cardinal;
 cluster k-element -> non empty for set;
end;

registration let k be natural Number;
 cluster Segm k -> finite;
end;

theorem :: CARD_1:71
 for f being Function, x,y being object
 holds card(f+~(x,y)) = card f;

registration let n be non zero natural Number;
 cluster Segm n -> with_zero;
end;

registration
  let c be Cardinal;
  cluster cardinal for Subset of c;
end;