Metamath Proof Explorer

Definition df-hash

Description: Define the set size function # , which gives the cardinality of a finite set as a member of NN0 , and assigns all infinite sets the value +oo . For example, ( #{ 0 , 1 , 2 } ) = 3 ( ex-hash ). (Contributed by Paul Chapman, 22-Jun-2011)

Ref Expression
Assertion df-hash ⊢ . = rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω ∘ card ∪ V ∖ Fin × +∞

Detailed syntax breakdown

Step Hyp Ref Expression
0 chash class .
1 vx setvar x
2 cvv class V
3 1 cv setvar x
4 caddc class +
5 c1 class 1
6 3 5 4 co class x + 1
7 1 2 6 cmpt class x ∈ V ⟼ x + 1
8 cc0 class 0
9 7 8 crdg class rec ⁡ x ∈ V ⟼ x + 1 0
10 com class ω
11 9 10 cres class rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω
12 ccrd class card
13 11 12 ccom class rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω ∘ card
14 cfn class Fin
15 2 14 cdif class V ∖ Fin
16 cpnf class +∞
17 16 csn class +∞
18 15 17 cxp class V ∖ Fin × +∞
19 13 18 cun class rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω ∘ card ∪ V ∖ Fin × +∞
20 0 19 wceq wff . = rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω ∘ card ∪ V ∖ Fin × +∞