Metamath Proof Explorer

Theorem hashdom

Description: Dominance relation for the size function. (Contributed by Mario Carneiro, 22-Sep-2013) (Revised by Mario Carneiro, 22-Apr-2015)

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

Proof

Step Hyp Ref Expression
1 fzfi 
 |-  ( 1 ... ( ( # ` B ) - ( # ` A ) ) ) e. Fin
2 ficardom 
 |-  ( ( 1 ... ( ( # ` B ) - ( # ` A ) ) ) e. Fin -> ( card ` ( 1 ... ( ( # ` B ) - ( # ` A ) ) ) ) e. _om )
3 1 2 ax-mp 
 |-  ( card ` ( 1 ... ( ( # ` B ) - ( # ` A ) ) ) ) e. _om
4 eqid 
 |-  ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) = ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om )
5 4 hashgval 
 |-  ( A e. Fin -> ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( card ` A ) ) = ( # ` A ) )
6 5 ad2antrr 
 |-  ( ( ( A e. Fin /\ B e. Fin ) /\ ( # ` A ) <_ ( # ` B ) ) -> ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( card ` A ) ) = ( # ` A ) )
7 4 hashgval 
 |-  ( ( 1 ... ( ( # ` B ) - ( # ` A ) ) ) e. Fin -> ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( card ` ( 1 ... ( ( # ` B ) - ( # ` A ) ) ) ) ) = ( # ` ( 1 ... ( ( # ` B ) - ( # ` A ) ) ) ) )
8 1 7 ax-mp 
 |-  ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( card ` ( 1 ... ( ( # ` B ) - ( # ` A ) ) ) ) ) = ( # ` ( 1 ... ( ( # ` B ) - ( # ` A ) ) ) )
9 hashcl 
 |-  ( A e. Fin -> ( # ` A ) e. NN0 )
10 9 ad2antrr 
 |-  ( ( ( A e. Fin /\ B e. Fin ) /\ ( # ` A ) <_ ( # ` B ) ) -> ( # ` A ) e. NN0 )
11 hashcl 
 |-  ( B e. Fin -> ( # ` B ) e. NN0 )
12 11 ad2antlr 
 |-  ( ( ( A e. Fin /\ B e. Fin ) /\ ( # ` A ) <_ ( # ` B ) ) -> ( # ` B ) e. NN0 )
13 simpr 
 |-  ( ( ( A e. Fin /\ B e. Fin ) /\ ( # ` A ) <_ ( # ` B ) ) -> ( # ` A ) <_ ( # ` B ) )
14 nn0sub2 
 |-  ( ( ( # ` A ) e. NN0 /\ ( # ` B ) e. NN0 /\ ( # ` A ) <_ ( # ` B ) ) -> ( ( # ` B ) - ( # ` A ) ) e. NN0 )
15 10 12 13 14 syl3anc 
 |-  ( ( ( A e. Fin /\ B e. Fin ) /\ ( # ` A ) <_ ( # ` B ) ) -> ( ( # ` B ) - ( # ` A ) ) e. NN0 )
16 hashfz1 
 |-  ( ( ( # ` B ) - ( # ` A ) ) e. NN0 -> ( # ` ( 1 ... ( ( # ` B ) - ( # ` A ) ) ) ) = ( ( # ` B ) - ( # ` A ) ) )
17 15 16 syl 
 |-  ( ( ( A e. Fin /\ B e. Fin ) /\ ( # ` A ) <_ ( # ` B ) ) -> ( # ` ( 1 ... ( ( # ` B ) - ( # ` A ) ) ) ) = ( ( # ` B ) - ( # ` A ) ) )
18 8 17 syl5eq 
 |-  ( ( ( A e. Fin /\ B e. Fin ) /\ ( # ` A ) <_ ( # ` B ) ) -> ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( card ` ( 1 ... ( ( # ` B ) - ( # ` A ) ) ) ) ) = ( ( # ` B ) - ( # ` A ) ) )
19 6 18 oveq12d 
 |-  ( ( ( A e. Fin /\ B e. Fin ) /\ ( # ` A ) <_ ( # ` B ) ) -> ( ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( card ` A ) ) + ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( card ` ( 1 ... ( ( # ` B ) - ( # ` A ) ) ) ) ) ) = ( ( # ` A ) + ( ( # ` B ) - ( # ` A ) ) ) )
20 9 nn0cnd 
 |-  ( A e. Fin -> ( # ` A ) e. CC )
21 11 nn0cnd 
 |-  ( B e. Fin -> ( # ` B ) e. CC )
22 pncan3 
 |-  ( ( ( # ` A ) e. CC /\ ( # ` B ) e. CC ) -> ( ( # ` A ) + ( ( # ` B ) - ( # ` A ) ) ) = ( # ` B ) )
23 20 21 22 syl2an 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( ( # ` A ) + ( ( # ` B ) - ( # ` A ) ) ) = ( # ` B ) )
24 23 adantr 
 |-  ( ( ( A e. Fin /\ B e. Fin ) /\ ( # ` A ) <_ ( # ` B ) ) -> ( ( # ` A ) + ( ( # ` B ) - ( # ` A ) ) ) = ( # ` B ) )
25 19 24 eqtrd 
 |-  ( ( ( A e. Fin /\ B e. Fin ) /\ ( # ` A ) <_ ( # ` B ) ) -> ( ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( card ` A ) ) + ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( card ` ( 1 ... ( ( # ` B ) - ( # ` A ) ) ) ) ) ) = ( # ` B ) )
26 ficardom 
 |-  ( A e. Fin -> ( card ` A ) e. _om )
27 26 ad2antrr 
 |-  ( ( ( A e. Fin /\ B e. Fin ) /\ ( # ` A ) <_ ( # ` B ) ) -> ( card ` A ) e. _om )
28 4 hashgadd 
 |-  ( ( ( card ` A ) e. _om /\ ( card ` ( 1 ... ( ( # ` B ) - ( # ` A ) ) ) ) e. _om ) -> ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( ( card ` A ) +o ( card ` ( 1 ... ( ( # ` B ) - ( # ` A ) ) ) ) ) ) = ( ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( card ` A ) ) + ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( card ` ( 1 ... ( ( # ` B ) - ( # ` A ) ) ) ) ) ) )
29 27 3 28 sylancl 
 |-  ( ( ( A e. Fin /\ B e. Fin ) /\ ( # ` A ) <_ ( # ` B ) ) -> ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( ( card ` A ) +o ( card ` ( 1 ... ( ( # ` B ) - ( # ` A ) ) ) ) ) ) = ( ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( card ` A ) ) + ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( card ` ( 1 ... ( ( # ` B ) - ( # ` A ) ) ) ) ) ) )
30 4 hashgval 
 |-  ( B e. Fin -> ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( card ` B ) ) = ( # ` B ) )
31 30 ad2antlr 
 |-  ( ( ( A e. Fin /\ B e. Fin ) /\ ( # ` A ) <_ ( # ` B ) ) -> ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( card ` B ) ) = ( # ` B ) )
32 25 29 31 3eqtr4d 
 |-  ( ( ( A e. Fin /\ B e. Fin ) /\ ( # ` A ) <_ ( # ` B ) ) -> ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( ( card ` A ) +o ( card ` ( 1 ... ( ( # ` B ) - ( # ` A ) ) ) ) ) ) = ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( card ` B ) ) )
33 32 fveq2d 
 |-  ( ( ( A e. Fin /\ B e. Fin ) /\ ( # ` A ) <_ ( # ` B ) ) -> ( `' ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( ( card ` A ) +o ( card ` ( 1 ... ( ( # ` B ) - ( # ` A ) ) ) ) ) ) ) = ( `' ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( card ` B ) ) ) )
34 4 hashgf1o 
 |-  ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) : _om -1-1-onto-> NN0
35 nnacl 
 |-  ( ( ( card ` A ) e. _om /\ ( card ` ( 1 ... ( ( # ` B ) - ( # ` A ) ) ) ) e. _om ) -> ( ( card ` A ) +o ( card ` ( 1 ... ( ( # ` B ) - ( # ` A ) ) ) ) ) e. _om )
36 27 3 35 sylancl 
 |-  ( ( ( A e. Fin /\ B e. Fin ) /\ ( # ` A ) <_ ( # ` B ) ) -> ( ( card ` A ) +o ( card ` ( 1 ... ( ( # ` B ) - ( # ` A ) ) ) ) ) e. _om )
37 f1ocnvfv1 
 |-  ( ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) : _om -1-1-onto-> NN0 /\ ( ( card ` A ) +o ( card ` ( 1 ... ( ( # ` B ) - ( # ` A ) ) ) ) ) e. _om ) -> ( `' ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( ( card ` A ) +o ( card ` ( 1 ... ( ( # ` B ) - ( # ` A ) ) ) ) ) ) ) = ( ( card ` A ) +o ( card ` ( 1 ... ( ( # ` B ) - ( # ` A ) ) ) ) ) )
38 34 36 37 sylancr 
 |-  ( ( ( A e. Fin /\ B e. Fin ) /\ ( # ` A ) <_ ( # ` B ) ) -> ( `' ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( ( card ` A ) +o ( card ` ( 1 ... ( ( # ` B ) - ( # ` A ) ) ) ) ) ) ) = ( ( card ` A ) +o ( card ` ( 1 ... ( ( # ` B ) - ( # ` A ) ) ) ) ) )
39 ficardom 
 |-  ( B e. Fin -> ( card ` B ) e. _om )
40 39 ad2antlr 
 |-  ( ( ( A e. Fin /\ B e. Fin ) /\ ( # ` A ) <_ ( # ` B ) ) -> ( card ` B ) e. _om )
41 f1ocnvfv1 
 |-  ( ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) : _om -1-1-onto-> NN0 /\ ( card ` B ) e. _om ) -> ( `' ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( card ` B ) ) ) = ( card ` B ) )
42 34 40 41 sylancr 
 |-  ( ( ( A e. Fin /\ B e. Fin ) /\ ( # ` A ) <_ ( # ` B ) ) -> ( `' ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( card ` B ) ) ) = ( card ` B ) )
43 33 38 42 3eqtr3d 
 |-  ( ( ( A e. Fin /\ B e. Fin ) /\ ( # ` A ) <_ ( # ` B ) ) -> ( ( card ` A ) +o ( card ` ( 1 ... ( ( # ` B ) - ( # ` A ) ) ) ) ) = ( card ` B ) )
44 oveq2 
 |-  ( y = ( card ` ( 1 ... ( ( # ` B ) - ( # ` A ) ) ) ) -> ( ( card ` A ) +o y ) = ( ( card ` A ) +o ( card ` ( 1 ... ( ( # ` B ) - ( # ` A ) ) ) ) ) )
45 44 eqeq1d 
 |-  ( y = ( card ` ( 1 ... ( ( # ` B ) - ( # ` A ) ) ) ) -> ( ( ( card ` A ) +o y ) = ( card ` B ) <-> ( ( card ` A ) +o ( card ` ( 1 ... ( ( # ` B ) - ( # ` A ) ) ) ) ) = ( card ` B ) ) )
46 45 rspcev 
 |-  ( ( ( card ` ( 1 ... ( ( # ` B ) - ( # ` A ) ) ) ) e. _om /\ ( ( card ` A ) +o ( card ` ( 1 ... ( ( # ` B ) - ( # ` A ) ) ) ) ) = ( card ` B ) ) -> E. y e. _om ( ( card ` A ) +o y ) = ( card ` B ) )
47 3 43 46 sylancr 
 |-  ( ( ( A e. Fin /\ B e. Fin ) /\ ( # ` A ) <_ ( # ` B ) ) -> E. y e. _om ( ( card ` A ) +o y ) = ( card ` B ) )
48 47 ex 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( ( # ` A ) <_ ( # ` B ) -> E. y e. _om ( ( card ` A ) +o y ) = ( card ` B ) ) )
49 cardnn 
 |-  ( y e. _om -> ( card ` y ) = y )
50 49 adantl 
 |-  ( ( ( A e. Fin /\ B e. Fin ) /\ y e. _om ) -> ( card ` y ) = y )
51 50 oveq2d 
 |-  ( ( ( A e. Fin /\ B e. Fin ) /\ y e. _om ) -> ( ( card ` A ) +o ( card ` y ) ) = ( ( card ` A ) +o y ) )
52 51 eqeq1d 
 |-  ( ( ( A e. Fin /\ B e. Fin ) /\ y e. _om ) -> ( ( ( card ` A ) +o ( card ` y ) ) = ( card ` B ) <-> ( ( card ` A ) +o y ) = ( card ` B ) ) )
53 fveq2 
 |-  ( ( ( card ` A ) +o ( card ` y ) ) = ( card ` B ) -> ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( ( card ` A ) +o ( card ` y ) ) ) = ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( card ` B ) ) )
54 nnfi 
 |-  ( y e. _om -> y e. Fin )
55 ficardom 
 |-  ( y e. Fin -> ( card ` y ) e. _om )
56 4 hashgadd 
 |-  ( ( ( card ` A ) e. _om /\ ( card ` y ) e. _om ) -> ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( ( card ` A ) +o ( card ` y ) ) ) = ( ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( card ` A ) ) + ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( card ` y ) ) ) )
57 26 55 56 syl2an 
 |-  ( ( A e. Fin /\ y e. Fin ) -> ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( ( card ` A ) +o ( card ` y ) ) ) = ( ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( card ` A ) ) + ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( card ` y ) ) ) )
58 4 hashgval 
 |-  ( y e. Fin -> ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( card ` y ) ) = ( # ` y ) )
59 5 58 oveqan12d 
 |-  ( ( A e. Fin /\ y e. Fin ) -> ( ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( card ` A ) ) + ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( card ` y ) ) ) = ( ( # ` A ) + ( # ` y ) ) )
60 57 59 eqtrd 
 |-  ( ( A e. Fin /\ y e. Fin ) -> ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( ( card ` A ) +o ( card ` y ) ) ) = ( ( # ` A ) + ( # ` y ) ) )
61 60 adantlr 
 |-  ( ( ( A e. Fin /\ B e. Fin ) /\ y e. Fin ) -> ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( ( card ` A ) +o ( card ` y ) ) ) = ( ( # ` A ) + ( # ` y ) ) )
62 30 ad2antlr 
 |-  ( ( ( A e. Fin /\ B e. Fin ) /\ y e. Fin ) -> ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( card ` B ) ) = ( # ` B ) )
63 61 62 eqeq12d 
 |-  ( ( ( A e. Fin /\ B e. Fin ) /\ y e. Fin ) -> ( ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( ( card ` A ) +o ( card ` y ) ) ) = ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( card ` B ) ) <-> ( ( # ` A ) + ( # ` y ) ) = ( # ` B ) ) )
64 hashcl 
 |-  ( y e. Fin -> ( # ` y ) e. NN0 )
65 64 nn0ge0d 
 |-  ( y e. Fin -> 0 <_ ( # ` y ) )
66 65 adantl 
 |-  ( ( A e. Fin /\ y e. Fin ) -> 0 <_ ( # ` y ) )
67 9 nn0red 
 |-  ( A e. Fin -> ( # ` A ) e. RR )
68 64 nn0red 
 |-  ( y e. Fin -> ( # ` y ) e. RR )
69 addge01 
 |-  ( ( ( # ` A ) e. RR /\ ( # ` y ) e. RR ) -> ( 0 <_ ( # ` y ) <-> ( # ` A ) <_ ( ( # ` A ) + ( # ` y ) ) ) )
70 67 68 69 syl2an 
 |-  ( ( A e. Fin /\ y e. Fin ) -> ( 0 <_ ( # ` y ) <-> ( # ` A ) <_ ( ( # ` A ) + ( # ` y ) ) ) )
71 66 70 mpbid 
 |-  ( ( A e. Fin /\ y e. Fin ) -> ( # ` A ) <_ ( ( # ` A ) + ( # ` y ) ) )
72 71 adantlr 
 |-  ( ( ( A e. Fin /\ B e. Fin ) /\ y e. Fin ) -> ( # ` A ) <_ ( ( # ` A ) + ( # ` y ) ) )
73 breq2 
 |-  ( ( ( # ` A ) + ( # ` y ) ) = ( # ` B ) -> ( ( # ` A ) <_ ( ( # ` A ) + ( # ` y ) ) <-> ( # ` A ) <_ ( # ` B ) ) )
74 72 73 syl5ibcom 
 |-  ( ( ( A e. Fin /\ B e. Fin ) /\ y e. Fin ) -> ( ( ( # ` A ) + ( # ` y ) ) = ( # ` B ) -> ( # ` A ) <_ ( # ` B ) ) )
75 63 74 sylbid 
 |-  ( ( ( A e. Fin /\ B e. Fin ) /\ y e. Fin ) -> ( ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( ( card ` A ) +o ( card ` y ) ) ) = ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( card ` B ) ) -> ( # ` A ) <_ ( # ` B ) ) )
76 54 75 sylan2 
 |-  ( ( ( A e. Fin /\ B e. Fin ) /\ y e. _om ) -> ( ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( ( card ` A ) +o ( card ` y ) ) ) = ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( card ` B ) ) -> ( # ` A ) <_ ( # ` B ) ) )
77 53 76 syl5 
 |-  ( ( ( A e. Fin /\ B e. Fin ) /\ y e. _om ) -> ( ( ( card ` A ) +o ( card ` y ) ) = ( card ` B ) -> ( # ` A ) <_ ( # ` B ) ) )
78 52 77 sylbird 
 |-  ( ( ( A e. Fin /\ B e. Fin ) /\ y e. _om ) -> ( ( ( card ` A ) +o y ) = ( card ` B ) -> ( # ` A ) <_ ( # ` B ) ) )
79 78 rexlimdva 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( E. y e. _om ( ( card ` A ) +o y ) = ( card ` B ) -> ( # ` A ) <_ ( # ` B ) ) )
80 48 79 impbid 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( ( # ` A ) <_ ( # ` B ) <-> E. y e. _om ( ( card ` A ) +o y ) = ( card ` B ) ) )
81 nnawordex 
 |-  ( ( ( card ` A ) e. _om /\ ( card ` B ) e. _om ) -> ( ( card ` A ) C_ ( card ` B ) <-> E. y e. _om ( ( card ` A ) +o y ) = ( card ` B ) ) )
82 26 39 81 syl2an 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( ( card ` A ) C_ ( card ` B ) <-> E. y e. _om ( ( card ` A ) +o y ) = ( card ` B ) ) )
83 finnum 
 |-  ( A e. Fin -> A e. dom card )
84 finnum 
 |-  ( B e. Fin -> B e. dom card )
85 carddom2 
 |-  ( ( A e. dom card /\ B e. dom card ) -> ( ( card ` A ) C_ ( card ` B ) <-> A ~<_ B ) )
86 83 84 85 syl2an 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( ( card ` A ) C_ ( card ` B ) <-> A ~<_ B ) )
87 80 82 86 3bitr2d 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( ( # ` A ) <_ ( # ` B ) <-> A ~<_ B ) )
88 87 adantlr 
 |-  ( ( ( A e. Fin /\ B e. V ) /\ B e. Fin ) -> ( ( # ` A ) <_ ( # ` B ) <-> A ~<_ B ) )
89 hashxrcl 
 |-  ( A e. Fin -> ( # ` A ) e. RR* )
90 89 ad2antrr 
 |-  ( ( ( A e. Fin /\ B e. V ) /\ -. B e. Fin ) -> ( # ` A ) e. RR* )
91 pnfge 
 |-  ( ( # ` A ) e. RR* -> ( # ` A ) <_ +oo )
92 90 91 syl 
 |-  ( ( ( A e. Fin /\ B e. V ) /\ -. B e. Fin ) -> ( # ` A ) <_ +oo )
93 hashinf 
 |-  ( ( B e. V /\ -. B e. Fin ) -> ( # ` B ) = +oo )
94 93 adantll 
 |-  ( ( ( A e. Fin /\ B e. V ) /\ -. B e. Fin ) -> ( # ` B ) = +oo )
95 92 94 breqtrrd 
 |-  ( ( ( A e. Fin /\ B e. V ) /\ -. B e. Fin ) -> ( # ` A ) <_ ( # ` B ) )
96 isinffi 
 |-  ( ( -. B e. Fin /\ A e. Fin ) -> E. f f : A -1-1-> B )
97 96 ancoms 
 |-  ( ( A e. Fin /\ -. B e. Fin ) -> E. f f : A -1-1-> B )
98 97 adantlr 
 |-  ( ( ( A e. Fin /\ B e. V ) /\ -. B e. Fin ) -> E. f f : A -1-1-> B )
99 brdomg 
 |-  ( B e. V -> ( A ~<_ B <-> E. f f : A -1-1-> B ) )
100 99 ad2antlr 
 |-  ( ( ( A e. Fin /\ B e. V ) /\ -. B e. Fin ) -> ( A ~<_ B <-> E. f f : A -1-1-> B ) )
101 98 100 mpbird 
 |-  ( ( ( A e. Fin /\ B e. V ) /\ -. B e. Fin ) -> A ~<_ B )
102 95 101 2thd 
 |-  ( ( ( A e. Fin /\ B e. V ) /\ -. B e. Fin ) -> ( ( # ` A ) <_ ( # ` B ) <-> A ~<_ B ) )
103 88 102 pm2.61dan 
 |-  ( ( A e. Fin /\ B e. V ) -> ( ( # ` A ) <_ ( # ` B ) <-> A ~<_ B ) )