Theorem hashomiso

Description: The # function yields an order isomorphism between _om and NN0 . (Contributed by Eric Schmidt, 7-Jul-2026)

	Ref	Expression
Assertion	hashomiso	⊢ ( ♯ ↾ ω ) Isom E , < ( ω , ℕ0 )

Proof

Step	Hyp	Ref	Expression
1		hashomf1o	⊢ ( ♯ ↾ ω ) : ω –1-1-onto→ ℕ0
2		epel	⊢ ( 𝑥 E 𝑦 ↔ 𝑥 ∈ 𝑦 )
3		hashnnltb	⊢ ( ( 𝑥 ∈ ω ∧ 𝑦 ∈ ω ) → ( 𝑥 ∈ 𝑦 ↔ ( ♯ ‘ 𝑥 ) < ( ♯ ‘ 𝑦 ) ) )
4	2 3	bitrid	⊢ ( ( 𝑥 ∈ ω ∧ 𝑦 ∈ ω ) → ( 𝑥 E 𝑦 ↔ ( ♯ ‘ 𝑥 ) < ( ♯ ‘ 𝑦 ) ) )
5		fvres	⊢ ( 𝑥 ∈ ω → ( ( ♯ ↾ ω ) ‘ 𝑥 ) = ( ♯ ‘ 𝑥 ) )
6		fvres	⊢ ( 𝑦 ∈ ω → ( ( ♯ ↾ ω ) ‘ 𝑦 ) = ( ♯ ‘ 𝑦 ) )
7	5 6	breqan12d	⊢ ( ( 𝑥 ∈ ω ∧ 𝑦 ∈ ω ) → ( ( ( ♯ ↾ ω ) ‘ 𝑥 ) < ( ( ♯ ↾ ω ) ‘ 𝑦 ) ↔ ( ♯ ‘ 𝑥 ) < ( ♯ ‘ 𝑦 ) ) )
8	4 7	bitr4d	⊢ ( ( 𝑥 ∈ ω ∧ 𝑦 ∈ ω ) → ( 𝑥 E 𝑦 ↔ ( ( ♯ ↾ ω ) ‘ 𝑥 ) < ( ( ♯ ↾ ω ) ‘ 𝑦 ) ) )
9	8	rgen2	⊢ ∀ 𝑥 ∈ ω ∀ 𝑦 ∈ ω ( 𝑥 E 𝑦 ↔ ( ( ♯ ↾ ω ) ‘ 𝑥 ) < ( ( ♯ ↾ ω ) ‘ 𝑦 ) )
10		df-isom	⊢ ( ( ♯ ↾ ω ) Isom E , < ( ω , ℕ0 ) ↔ ( ( ♯ ↾ ω ) : ω –1-1-onto→ ℕ0 ∧ ∀ 𝑥 ∈ ω ∀ 𝑦 ∈ ω ( 𝑥 E 𝑦 ↔ ( ( ♯ ↾ ω ) ‘ 𝑥 ) < ( ( ♯ ↾ ω ) ‘ 𝑦 ) ) ) )
11	1 9 10	mpbir2an	⊢ ( ♯ ↾ ω ) Isom E , < ( ω , ℕ0 )