Theorem hashomf1o

Description: The # function yields a bijection from _om to NN0 . (Contributed by Eric Schmidt, 7-Jul-2026)

	Ref	Expression
Assertion	hashomf1o	⊢ ( ♯ ↾ ω ) : ω –1-1-onto→ ℕ0

Proof

Step	Hyp	Ref	Expression
1		hashgval2	⊢ ( ♯ ↾ ω ) = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω )
2	1	hashgf1o	⊢ ( ♯ ↾ ω ) : ω –1-1-onto→ ℕ0