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