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

Definition df-hash 12980
Description: Define the set size function #, which gives the cardinality of a finite set as a member of 0, and assigns all infinite sets the value +∞. For example, (#‘{0, 1, 2}) = 3 (ex-hash 26702). (Contributed by Paul Chapman, 22-Jun-2011.)
Assertion
Ref Expression
df-hash # = (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω) ∘ card) ∪ ((V ∖ Fin) × {+∞}))

Detailed syntax breakdown of Definition df-hash
StepHypRef Expression
1 chash 12979 . 2 class #
2 vx . . . . . . 7 setvar 𝑥
3 cvv 3173 . . . . . . 7 class V
42cv 1474 . . . . . . . 8 class 𝑥
5 c1 9816 . . . . . . . 8 class 1
6 caddc 9818 . . . . . . . 8 class +
74, 5, 6co 6549 . . . . . . 7 class (𝑥 + 1)
82, 3, 7cmpt 4643 . . . . . 6 class (𝑥 ∈ V ↦ (𝑥 + 1))
9 cc0 9815 . . . . . 6 class 0
108, 9crdg 7392 . . . . 5 class rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0)
11 com 6957 . . . . 5 class ω
1210, 11cres 5040 . . . 4 class (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)
13 ccrd 8644 . . . 4 class card
1412, 13ccom 5042 . . 3 class ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω) ∘ card)
15 cfn 7841 . . . . 5 class Fin
163, 15cdif 3537 . . . 4 class (V ∖ Fin)
17 cpnf 9950 . . . . 5 class +∞
1817csn 4125 . . . 4 class {+∞}
1916, 18cxp 5036 . . 3 class ((V ∖ Fin) × {+∞})
2014, 19cun 3538 . 2 class (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω) ∘ card) ∪ ((V ∖ Fin) × {+∞}))
211, 20wceq 1475 1 wff # = (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω) ∘ card) ∪ ((V ∖ Fin) × {+∞}))
Colors of variables: wff setvar class
This definition is referenced by:  hashgval  12982  hashinf  12984  hashfxnn0  12986  hashfOLD  12988
  Copyright terms: Public domain W3C validator