# 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 ${⊢}\left|.\right|=\left(\left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}+1\right),0\right)↾}_{\mathrm{\omega }}\right)\circ \mathrm{card}\right)\cup \left(\left(\mathrm{V}\setminus \mathrm{Fin}\right)×\left\{\mathrm{+\infty }\right\}\right)$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 chash ${class}\left|.\right|$
1 vx ${setvar}{x}$
2 cvv ${class}\mathrm{V}$
3 1 cv ${setvar}{x}$
4 caddc ${class}+$
5 c1 ${class}1$
6 3 5 4 co ${class}\left({x}+1\right)$
7 1 2 6 cmpt ${class}\left({x}\in \mathrm{V}⟼{x}+1\right)$
8 cc0 ${class}0$
9 7 8 crdg ${class}\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}+1\right),0\right)$
10 com ${class}\mathrm{\omega }$
11 9 10 cres ${class}\left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}+1\right),0\right)↾}_{\mathrm{\omega }}\right)$
12 ccrd ${class}\mathrm{card}$
13 11 12 ccom ${class}\left(\left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}+1\right),0\right)↾}_{\mathrm{\omega }}\right)\circ \mathrm{card}\right)$
14 cfn ${class}\mathrm{Fin}$
15 2 14 cdif ${class}\left(\mathrm{V}\setminus \mathrm{Fin}\right)$
16 cpnf ${class}\mathrm{+\infty }$
17 16 csn ${class}\left\{\mathrm{+\infty }\right\}$
18 15 17 cxp ${class}\left(\left(\mathrm{V}\setminus \mathrm{Fin}\right)×\left\{\mathrm{+\infty }\right\}\right)$
19 13 18 cun ${class}\left(\left(\left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}+1\right),0\right)↾}_{\mathrm{\omega }}\right)\circ \mathrm{card}\right)\cup \left(\left(\mathrm{V}\setminus \mathrm{Fin}\right)×\left\{\mathrm{+\infty }\right\}\right)\right)$
20 0 19 wceq ${wff}\left|.\right|=\left(\left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}+1\right),0\right)↾}_{\mathrm{\omega }}\right)\circ \mathrm{card}\right)\cup \left(\left(\mathrm{V}\setminus \mathrm{Fin}\right)×\left\{\mathrm{+\infty }\right\}\right)$