Metamath Proof Explorer

Theorem hasheni

Description: Equinumerous sets have the same number of elements (even if they are not finite). (Contributed by Mario Carneiro, 15-Apr-2015)

Ref Expression
Assertion hasheni 
|- ( A ~~ B -> ( # ` A ) = ( # ` B ) )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( A ~~ B /\ B e. Fin ) -> A ~~ B )
2 enfii 
 |-  ( ( B e. Fin /\ A ~~ B ) -> A e. Fin )
3 2 ancoms 
 |-  ( ( A ~~ B /\ B e. Fin ) -> A e. Fin )
4 hashen 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( ( # ` A ) = ( # ` B ) <-> A ~~ B ) )
5 3 4 sylancom 
 |-  ( ( A ~~ B /\ B e. Fin ) -> ( ( # ` A ) = ( # ` B ) <-> A ~~ B ) )
6 1 5 mpbird 
 |-  ( ( A ~~ B /\ B e. Fin ) -> ( # ` A ) = ( # ` B ) )
7 relen 
 |-  Rel ~~
8 7 brrelex1i 
 |-  ( A ~~ B -> A e. _V )
9 enfi 
 |-  ( A ~~ B -> ( A e. Fin <-> B e. Fin ) )
10 9 notbid 
 |-  ( A ~~ B -> ( -. A e. Fin <-> -. B e. Fin ) )
11 10 biimpar 
 |-  ( ( A ~~ B /\ -. B e. Fin ) -> -. A e. Fin )
12 hashinf 
 |-  ( ( A e. _V /\ -. A e. Fin ) -> ( # ` A ) = +oo )
13 8 11 12 syl2an2r 
 |-  ( ( A ~~ B /\ -. B e. Fin ) -> ( # ` A ) = +oo )
14 7 brrelex2i 
 |-  ( A ~~ B -> B e. _V )
15 hashinf 
 |-  ( ( B e. _V /\ -. B e. Fin ) -> ( # ` B ) = +oo )
16 14 15 sylan 
 |-  ( ( A ~~ B /\ -. B e. Fin ) -> ( # ` B ) = +oo )
17 13 16 eqtr4d 
 |-  ( ( A ~~ B /\ -. B e. Fin ) -> ( # ` A ) = ( # ` B ) )
18 6 17 pm2.61dan 
 |-  ( A ~~ B -> ( # ` A ) = ( # ` B ) )