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

Metamath Proof Explorer

Theorem hashen

Description: Two finite sets have the same number of elements iff they are equinumerous. (Contributed by Paul Chapman, 22-Jun-2011) (Revised by Mario Carneiro, 15-Sep-2013)

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

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( ( # ` A ) = ( # ` B ) -> ( `' ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( # ` A ) ) = ( `' ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( # ` B ) ) )
2 eqid 
 |-  ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) = ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om )
3 2 hashginv 
 |-  ( A e. Fin -> ( `' ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( # ` A ) ) = ( card ` A ) )
4 2 hashginv 
 |-  ( B e. Fin -> ( `' ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( # ` B ) ) = ( card ` B ) )
5 3 4 eqeqan12d 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( ( `' ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( # ` A ) ) = ( `' ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( # ` B ) ) <-> ( card ` A ) = ( card ` B ) ) )
6 1 5 imbitrid 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( ( # ` A ) = ( # ` B ) -> ( card ` A ) = ( card ` B ) ) )
7 fveq2 
 |-  ( ( card ` A ) = ( card ` B ) -> ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( card ` A ) ) = ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( card ` B ) ) )
8 2 hashgval 
 |-  ( A e. Fin -> ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( card ` A ) ) = ( # ` A ) )
9 2 hashgval 
 |-  ( B e. Fin -> ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( card ` B ) ) = ( # ` B ) )
10 8 9 eqeqan12d 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( card ` A ) ) = ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( card ` B ) ) <-> ( # ` A ) = ( # ` B ) ) )
11 7 10 imbitrid 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( ( card ` A ) = ( card ` B ) -> ( # ` A ) = ( # ` B ) ) )
12 6 11 impbid 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( ( # ` A ) = ( # ` B ) <-> ( card ` A ) = ( card ` B ) ) )
13 finnum 
 |-  ( A e. Fin -> A e. dom card )
14 finnum 
 |-  ( B e. Fin -> B e. dom card )
15 carden2 
 |-  ( ( A e. dom card /\ B e. dom card ) -> ( ( card ` A ) = ( card ` B ) <-> A ~~ B ) )
16 13 14 15 syl2an 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( ( card ` A ) = ( card ` B ) <-> A ~~ B ) )
17 12 16 bitrd 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( ( # ` A ) = ( # ` B ) <-> A ~~ B ) )