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 ⁡ x ∈ V ⟼ x + 1 0 ↾ ω = rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω
2 eqid ⊢ rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω ∘ card = rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω ∘ card
3 1 2 hashkf ⊢ rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω ∘ card : Fin ⟶ ℕ 0
4 pnfex ⊢ +∞ ∈ V
5 4 fconst ⊢ V ∖ Fin × +∞ : V ∖ Fin ⟶ +∞
6 3 5 pm3.2i ⊢ rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω ∘ card : Fin ⟶ ℕ 0 ∧ V ∖ Fin × +∞ : V ∖ Fin ⟶ +∞
7 disjdif ⊢ Fin ∩ V ∖ Fin = ∅
8 fun ⊢ rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω ∘ card : Fin ⟶ ℕ 0 ∧ V ∖ Fin × +∞ : V ∖ Fin ⟶ +∞ ∧ Fin ∩ V ∖ Fin = ∅ → rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω ∘ card ∪ V ∖ Fin × +∞ : Fin ∪ V ∖ Fin ⟶ ℕ 0 ∪ +∞
9 6 7 8 mp2an ⊢ rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω ∘ card ∪ V ∖ Fin × +∞ : Fin ∪ V ∖ Fin ⟶ ℕ 0 ∪ +∞
10 df-hash ⊢ . = rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω ∘ card ∪ V ∖ Fin × +∞
11 eqid ⊢ V = V
12 df-xnn0 ⊢ ℕ 0 * = ℕ 0 ∪ +∞
13 feq123 ⊢ . = rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω ∘ card ∪ V ∖ Fin × +∞ ∧ V = V ∧ ℕ 0 * = ℕ 0 ∪ +∞ → . : V ⟶ ℕ 0 * ↔ rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω ∘ card ∪ V ∖ Fin × +∞ : V ⟶ ℕ 0 ∪ +∞
14 10 11 12 13 mp3an ⊢ . : V ⟶ ℕ 0 * ↔ rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω ∘ card ∪ V ∖ Fin × +∞ : V ⟶ ℕ 0 ∪ +∞
15 unvdif ⊢ Fin ∪ V ∖ Fin = V
16 15 feq2i ⊢ rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω ∘ card ∪ V ∖ Fin × +∞ : Fin ∪ V ∖ Fin ⟶ ℕ 0 ∪ +∞ ↔ rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω ∘ card ∪ V ∖ Fin × +∞ : V ⟶ ℕ 0 ∪ +∞
17 14 16 bitr4i ⊢ . : V ⟶ ℕ 0 * ↔ rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω ∘ card ∪ V ∖ Fin × +∞ : Fin ∪ V ∖ Fin ⟶ ℕ 0 ∪ +∞
18 9 17 mpbir ⊢ . : V ⟶ ℕ 0 *