This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 bitrid 
 |-  ( ( 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 ) )