Theorem hashnnlt

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

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

Proof

Step	Hyp	Ref	Expression
1		nnfi	⊢ ( 𝐴 ∈ ω → 𝐴 ∈ Fin )
2		nnord	⊢ ( 𝐴 ∈ ω → Ord 𝐴 )
3		ordpss	⊢ ( Ord 𝐴 → ( 𝐵 ∈ 𝐴 → 𝐵 ⊊ 𝐴 ) )
4	2 3	syl	⊢ ( 𝐴 ∈ ω → ( 𝐵 ∈ 𝐴 → 𝐵 ⊊ 𝐴 ) )
5	4	imp	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴 ) → 𝐵 ⊊ 𝐴 )
6		hashpss	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ⊊ 𝐴 ) → ( ♯ ‘ 𝐵 ) < ( ♯ ‘ 𝐴 ) )
7	1 5 6	syl2an2r	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴 ) → ( ♯ ‘ 𝐵 ) < ( ♯ ‘ 𝐴 ) )