This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝑥 ∈ 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 ) × { +∞ } ) )