Theorem hashnnltb

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

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

Proof

Step	Hyp	Ref	Expression
1		hashnnlt	|- ( ( B e. _om /\ A e. B ) -> ( # ` A ) < ( # ` B ) )
2	1	ex	|- ( B e. _om -> ( A e. B -> ( # ` A ) < ( # ` B ) ) )
3	2	adantl	|- ( ( A e. _om /\ B e. _om ) -> ( A e. B -> ( # ` A ) < ( # ` B ) ) )
4		hashss	|- ( ( A e. _om /\ B C_ A ) -> ( # ` B ) <_ ( # ` A ) )
5	4	ex	|- ( A e. _om -> ( B C_ A -> ( # ` B ) <_ ( # ` A ) ) )
6	5	adantr	|- ( ( A e. _om /\ B e. _om ) -> ( B C_ A -> ( # ` B ) <_ ( # ` A ) ) )
7		nnon	|- ( B e. _om -> B e. On )
8		nnon	|- ( A e. _om -> A e. On )
9		ontri1	|- ( ( B e. On /\ A e. On ) -> ( B C_ A <-> -. A e. B ) )
10	7 8 9	syl2anr	|- ( ( A e. _om /\ B e. _om ) -> ( B C_ A <-> -. A e. B ) )
11		hashxrcl	|- ( B e. _om -> ( # ` B ) e. RR* )
12		hashxrcl	|- ( A e. _om -> ( # ` A ) e. RR* )
13		xrlenlt	|- ( ( ( # ` B ) e. RR* /\ ( # ` A ) e. RR* ) -> ( ( # ` B ) <_ ( # ` A ) <-> -. ( # ` A ) < ( # ` B ) ) )
14	11 12 13	syl2anr	|- ( ( A e. _om /\ B e. _om ) -> ( ( # ` B ) <_ ( # ` A ) <-> -. ( # ` A ) < ( # ` B ) ) )
15	6 10 14	3imtr3d	|- ( ( A e. _om /\ B e. _om ) -> ( -. A e. B -> -. ( # ` A ) < ( # ` B ) ) )
16	3 15	impcon4bid	|- ( ( A e. _om /\ B e. _om ) -> ( A e. B <-> ( # ` A ) < ( # ` B ) ) )