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

Metamath Proof Explorer

Theorem hashfxnn0

Description: The size function is a function into the extended nonnegative integers. (Contributed by Mario Carneiro, 13-Sep-2013) (Revised by AV, 10-Dec-2020)

Ref Expression
Assertion hashfxnn0 ♯ : V ⟶ ℕ0*

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω )
2 eqid ⊢ ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) = ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card )
3 1 2 hashkf ⊢ ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) : Fin ⟶ ℕ0
4 pnfex ⊢ +∞ ∈ V
5 4 fconst ⊢ ( ( V ∖ Fin ) × { +∞ } ) : ( V ∖ Fin ) ⟶ { +∞ }
6 3 5 pm3.2i ⊢ ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) : Fin ⟶ ℕ0 ∧ ( ( V ∖ Fin ) × { +∞ } ) : ( V ∖ Fin ) ⟶ { +∞ } )
7 disjdif ⊢ ( Fin ∩ ( V ∖ Fin ) ) = ∅
8 fun ⊢ ( ( ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) : Fin ⟶ ℕ0 ∧ ( ( V ∖ Fin ) × { +∞ } ) : ( V ∖ Fin ) ⟶ { +∞ } ) ∧ ( Fin ∩ ( V ∖ Fin ) ) = ∅ ) → ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) ∪ ( ( V ∖ Fin ) × { +∞ } ) ) : ( Fin ∪ ( V ∖ Fin ) ) ⟶ ( ℕ0 ∪ { +∞ } ) )
9 6 7 8 mp2an ⊢ ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) ∪ ( ( V ∖ Fin ) × { +∞ } ) ) : ( Fin ∪ ( V ∖ Fin ) ) ⟶ ( ℕ0 ∪ { +∞ } )
10 df-hash ⊢ ♯ = ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) ∪ ( ( V ∖ Fin ) × { +∞ } ) )
11 eqid ⊢ V = V
12 df-xnn0 ⊢ ℕ0* = ( ℕ0 ∪ { +∞ } )
13 feq123 ⊢ ( ( ♯ = ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) ∪ ( ( V ∖ Fin ) × { +∞ } ) ) ∧ V = V ∧ ℕ0* = ( ℕ0 ∪ { +∞ } ) ) → ( ♯ : V ⟶ ℕ0* ↔ ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) ∪ ( ( V ∖ Fin ) × { +∞ } ) ) : V ⟶ ( ℕ0 ∪ { +∞ } ) ) )
14 10 11 12 13 mp3an ⊢ ( ♯ : V ⟶ ℕ0* ↔ ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) ∪ ( ( V ∖ Fin ) × { +∞ } ) ) : V ⟶ ( ℕ0 ∪ { +∞ } ) )
15 unvdif ⊢ ( Fin ∪ ( V ∖ Fin ) ) = V
16 15 feq2i ⊢ ( ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) ∪ ( ( V ∖ Fin ) × { +∞ } ) ) : ( Fin ∪ ( V ∖ Fin ) ) ⟶ ( ℕ0 ∪ { +∞ } ) ↔ ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) ∪ ( ( V ∖ Fin ) × { +∞ } ) ) : V ⟶ ( ℕ0 ∪ { +∞ } ) )
17 14 16 bitr4i ⊢ ( ♯ : V ⟶ ℕ0* ↔ ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) ∪ ( ( V ∖ Fin ) × { +∞ } ) ) : ( Fin ∪ ( V ∖ Fin ) ) ⟶ ( ℕ0 ∪ { +∞ } ) )
18 9 17 mpbir ⊢ ♯ : V ⟶ ℕ0*