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