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*