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