Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-hash Structured version   Unicode version

Definition df-hash 11650
 Description: Define the function, which gives the cardinality of a finite set as a member of , and assigns all infinite sets the value . (Contributed by Paul Chapman, 22-Jun-2011.)
Assertion
Ref Expression
df-hash

Detailed syntax breakdown of Definition df-hash
StepHypRef Expression
1 chash 11649 . 2
2 vx . . . . . . 7
3 cvv 2962 . . . . . . 7
42cv 1652 . . . . . . . 8
5 c1 9022 . . . . . . . 8
6 caddc 9024 . . . . . . . 8
74, 5, 6co 6110 . . . . . . 7
82, 3, 7cmpt 4291 . . . . . 6
9 cc0 9021 . . . . . 6
108, 9crdg 6696 . . . . 5
11 com 4874 . . . . 5
1210, 11cres 4909 . . . 4
13 ccrd 7853 . . . 4
1412, 13ccom 4911 . . 3
15 cfn 7138 . . . . 5
163, 15cdif 3303 . . . 4
17 cpnf 9148 . . . . 5
1817csn 3838 . . . 4
1916, 18cxp 4905 . . 3
2014, 19cun 3304 . 2
211, 20wceq 1653 1
 Colors of variables: wff set class This definition is referenced by:  hashgval  11652  hashinf  11654  hashf  11656
 Copyright terms: Public domain W3C validator