Theorem hashnnltb

Description: The # function on _om preserves the ordering. (Contributed by Eric Schmidt, 7-Jul-2026)

	Ref	Expression
Assertion	hashnnltb	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴 ∈ 𝐵 ↔ ( ♯ ‘ 𝐴 ) < ( ♯ ‘ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		hashnnlt	⊢ ( ( 𝐵 ∈ ω ∧ 𝐴 ∈ 𝐵 ) → ( ♯ ‘ 𝐴 ) < ( ♯ ‘ 𝐵 ) )
2	1	ex	⊢ ( 𝐵 ∈ ω → ( 𝐴 ∈ 𝐵 → ( ♯ ‘ 𝐴 ) < ( ♯ ‘ 𝐵 ) ) )
3	2	adantl	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴 ∈ 𝐵 → ( ♯ ‘ 𝐴 ) < ( ♯ ‘ 𝐵 ) ) )
4		hashss	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ⊆ 𝐴 ) → ( ♯ ‘ 𝐵 ) ≤ ( ♯ ‘ 𝐴 ) )
5	4	ex	⊢ ( 𝐴 ∈ ω → ( 𝐵 ⊆ 𝐴 → ( ♯ ‘ 𝐵 ) ≤ ( ♯ ‘ 𝐴 ) ) )
6	5	adantr	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐵 ⊆ 𝐴 → ( ♯ ‘ 𝐵 ) ≤ ( ♯ ‘ 𝐴 ) ) )
7		nnon	⊢ ( 𝐵 ∈ ω → 𝐵 ∈ On )
8		nnon	⊢ ( 𝐴 ∈ ω → 𝐴 ∈ On )
9		ontri1	⊢ ( ( 𝐵 ∈ On ∧ 𝐴 ∈ On ) → ( 𝐵 ⊆ 𝐴 ↔ ¬ 𝐴 ∈ 𝐵 ) )
10	7 8 9	syl2anr	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐵 ⊆ 𝐴 ↔ ¬ 𝐴 ∈ 𝐵 ) )
11		hashxrcl	⊢ ( 𝐵 ∈ ω → ( ♯ ‘ 𝐵 ) ∈ ℝ* )
12		hashxrcl	⊢ ( 𝐴 ∈ ω → ( ♯ ‘ 𝐴 ) ∈ ℝ* )
13		xrlenlt	⊢ ( ( ( ♯ ‘ 𝐵 ) ∈ ℝ* ∧ ( ♯ ‘ 𝐴 ) ∈ ℝ* ) → ( ( ♯ ‘ 𝐵 ) ≤ ( ♯ ‘ 𝐴 ) ↔ ¬ ( ♯ ‘ 𝐴 ) < ( ♯ ‘ 𝐵 ) ) )
14	11 12 13	syl2anr	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( ( ♯ ‘ 𝐵 ) ≤ ( ♯ ‘ 𝐴 ) ↔ ¬ ( ♯ ‘ 𝐴 ) < ( ♯ ‘ 𝐵 ) ) )
15	6 10 14	3imtr3d	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( ¬ 𝐴 ∈ 𝐵 → ¬ ( ♯ ‘ 𝐴 ) < ( ♯ ‘ 𝐵 ) ) )
16	3 15	impcon4bid	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴 ∈ 𝐵 ↔ ( ♯ ‘ 𝐴 ) < ( ♯ ‘ 𝐵 ) ) )