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 ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) ∪ ( ( V ∖ Fin ) × { +∞ } ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		chash	⊢ ♯
1		vx	⊢ 𝑥
2		cvv	⊢ V
3	1	cv	⊢ 𝑥
4		caddc	⊢ +
5		c1	⊢ 1
6	3 5 4	co	⊢ ( 𝑥 + 1 )
7	1 2 6	cmpt	⊢ ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) )
8		cc0	⊢ 0
9	7 8	crdg	⊢ rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 )
10		com	⊢ ω
11	9 10	cres	⊢ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω )
12		ccrd	⊢ card
13	11 12	ccom	⊢ ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card )
14		cfn	⊢ Fin
15	2 14	cdif	⊢ ( V ∖ Fin )
16		cpnf	⊢ +∞
17	16	csn	⊢ { +∞ }
18	15 17	cxp	⊢ ( ( V ∖ Fin ) × { +∞ } )
19	13 18	cun	⊢ ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) ∪ ( ( V ∖ Fin ) × { +∞ } ) )
20	0 19	wceq	⊢ ♯ = ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) ∪ ( ( V ∖ Fin ) × { +∞ } ) )