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 \in V ⟼ x + 1), 0) ↾}_{ω}) \circ card) \cup ((V ∖ Fin) \times \{+∞\})$

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 \in V ⟼ x + 1)$
8		cc0	$class 0$
9	7 8	crdg	$class rec ((x \in V ⟼ x + 1), 0)$
10		com	$class ω$
11	9 10	cres	$class ({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω})$
12		ccrd	$class card$
13	11 12	ccom	$class (({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}) \circ 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) \times \{+∞\})$
19	13 18	cun	$class ((({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}) \circ card) \cup ((V ∖ Fin) \times \{+∞\}))$
20	0 19	wceq	$wff \|.\| = (({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}) \circ card) \cup ((V ∖ Fin) \times \{+∞\})$

Metamath Proof Explorer

Definition df-hash

Detailed syntax breakdown