Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-ihash Unicode version

Definition df-ihash 10555
 Description: Define the set size function ♯, which gives the cardinality of a finite set as a member of , and assigns all infinite sets the value . For example, ♯ . Note that we use the sharp sign (♯) for this function and we use the different character octothorpe (#) for the apartness relation (see df-ap 8369). We adopt the former notation from Corollary 8.2.4 of [AczelRathjen], p. 80 (although that work only defines it for finite sets). This definition (in terms of and ) is not taken directly from the literature, but for finite sets should be equivalent to the conventional definition that the size of a finite set is the unique natural number which is equinumerous to the given set. (Contributed by Jim Kingdon, 19-Feb-2022.)
Assertion
Ref Expression
df-ihash frec
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-ihash
StepHypRef Expression
1 chash 10554 . 2
2 vx . . . . . 6
3 cz 9079 . . . . . 6
42cv 1331 . . . . . . 7
5 c1 7646 . . . . . . 7
6 caddc 7648 . . . . . . 7
74, 5, 6co 5782 . . . . . 6
82, 3, 7cmpt 3997 . . . . 5
9 cc0 7645 . . . . 5
108, 9cfrec 6295 . . . 4 frec
11 com 4512 . . . . . 6
12 cpnf 7822 . . . . . 6
1311, 12cop 3535 . . . . 5
1413csn 3532 . . . 4
1510, 14cun 3074 . . 3 frec
16 cvv 2689 . . . 4
17 vy . . . . . . . 8
1817cv 1331 . . . . . . 7
19 cdom 6641 . . . . . . 7
2018, 4, 19wbr 3937 . . . . . 6
2111csn 3532 . . . . . . 7
2211, 21cun 3074 . . . . . 6
2320, 17, 22crab 2421 . . . . 5
2423cuni 3744 . . . 4
252, 16, 24cmpt 3997 . . 3
2615, 25ccom 4551 . 2 frec
271, 26wceq 1332 1 frec
 Colors of variables: wff set class This definition is referenced by:  hashinfom  10557  hashennn  10559
 Copyright terms: Public domain W3C validator