Theorem hashnnlt

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

	Ref	Expression
Assertion	hashnnlt	|- ( ( A e. _om /\ B e. A ) -> ( # ` B ) < ( # ` A ) )

Proof

Step	Hyp	Ref	Expression
1		nnfi	|- ( A e. _om -> A e. Fin )
2		nnord	|- ( A e. _om -> Ord A )
3		ordpss	|- ( Ord A -> ( B e. A -> B C. A ) )
4	2 3	syl	|- ( A e. _om -> ( B e. A -> B C. A ) )
5	4	imp	|- ( ( A e. _om /\ B e. A ) -> B C. A )
6		hashpss	|- ( ( A e. Fin /\ B C. A ) -> ( # ` B ) < ( # ` A ) )
7	1 5 6	syl2an2r	|- ( ( A e. _om /\ B e. A ) -> ( # ` B ) < ( # ` A ) )