Metamath Proof Explorer


Theorem hashsdom

Description: Strict dominance relation for the size function. (Contributed by Mario Carneiro, 18-Aug-2014)

Ref Expression
Assertion hashsdom
|- ( ( A e. Fin /\ B e. Fin ) -> ( ( # ` A ) < ( # ` B ) <-> A ~< B ) )

Proof

Step Hyp Ref Expression
1 hashcl
 |-  ( A e. Fin -> ( # ` A ) e. NN0 )
2 hashcl
 |-  ( B e. Fin -> ( # ` B ) e. NN0 )
3 nn0re
 |-  ( ( # ` A ) e. NN0 -> ( # ` A ) e. RR )
4 nn0re
 |-  ( ( # ` B ) e. NN0 -> ( # ` B ) e. RR )
5 ltlen
 |-  ( ( ( # ` A ) e. RR /\ ( # ` B ) e. RR ) -> ( ( # ` A ) < ( # ` B ) <-> ( ( # ` A ) <_ ( # ` B ) /\ ( # ` B ) =/= ( # ` A ) ) ) )
6 3 4 5 syl2an
 |-  ( ( ( # ` A ) e. NN0 /\ ( # ` B ) e. NN0 ) -> ( ( # ` A ) < ( # ` B ) <-> ( ( # ` A ) <_ ( # ` B ) /\ ( # ` B ) =/= ( # ` A ) ) ) )
7 1 2 6 syl2an
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( ( # ` A ) < ( # ` B ) <-> ( ( # ` A ) <_ ( # ` B ) /\ ( # ` B ) =/= ( # ` A ) ) ) )
8 hashdom
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( ( # ` A ) <_ ( # ` B ) <-> A ~<_ B ) )
9 eqcom
 |-  ( ( # ` B ) = ( # ` A ) <-> ( # ` A ) = ( # ` B ) )
10 hashen
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( ( # ` A ) = ( # ` B ) <-> A ~~ B ) )
11 9 10 syl5bb
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( ( # ` B ) = ( # ` A ) <-> A ~~ B ) )
12 11 necon3abid
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( ( # ` B ) =/= ( # ` A ) <-> -. A ~~ B ) )
13 8 12 anbi12d
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( ( ( # ` A ) <_ ( # ` B ) /\ ( # ` B ) =/= ( # ` A ) ) <-> ( A ~<_ B /\ -. A ~~ B ) ) )
14 7 13 bitrd
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( ( # ` A ) < ( # ` B ) <-> ( A ~<_ B /\ -. A ~~ B ) ) )
15 brsdom
 |-  ( A ~< B <-> ( A ~<_ B /\ -. A ~~ B ) )
16 14 15 bitr4di
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( ( # ` A ) < ( # ` B ) <-> A ~< B ) )