Metamath Proof Explorer

Theorem hasheqf1oi

Description: The size of two sets is equal if there is a bijection mapping one of the sets onto the other. (Contributed by Alexander van der Vekens, 25-Dec-2017) (Revised by AV, 4-May-2021)

Ref Expression
Assertion hasheqf1oi 
|- ( A e. V -> ( E. f f : A -1-1-onto-> B -> ( # ` A ) = ( # ` B ) ) )

Proof

Step Hyp Ref Expression
1 hasheqf1o 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( ( # ` A ) = ( # ` B ) <-> E. f f : A -1-1-onto-> B ) )
2 1 biimprd 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( E. f f : A -1-1-onto-> B -> ( # ` A ) = ( # ` B ) ) )
3 2 a1d 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( A e. V -> ( E. f f : A -1-1-onto-> B -> ( # ` A ) = ( # ` B ) ) ) )
4 fiinfnf1o 
 |-  ( ( A e. Fin /\ -. B e. Fin ) -> -. E. f f : A -1-1-onto-> B )
5 4 pm2.21d 
 |-  ( ( A e. Fin /\ -. B e. Fin ) -> ( E. f f : A -1-1-onto-> B -> ( # ` A ) = ( # ` B ) ) )
6 5 a1d 
 |-  ( ( A e. Fin /\ -. B e. Fin ) -> ( A e. V -> ( E. f f : A -1-1-onto-> B -> ( # ` A ) = ( # ` B ) ) ) )
7 fiinfnf1o 
 |-  ( ( B e. Fin /\ -. A e. Fin ) -> -. E. g g : B -1-1-onto-> A )
8 19.41v 
 |-  ( E. f ( f : A -1-1-onto-> B /\ A e. V ) <-> ( E. f f : A -1-1-onto-> B /\ A e. V ) )
9 f1orel 
 |-  ( f : A -1-1-onto-> B -> Rel f )
10 9 adantr 
 |-  ( ( f : A -1-1-onto-> B /\ A e. V ) -> Rel f )
11 f1ocnvb 
 |-  ( Rel f -> ( f : A -1-1-onto-> B <-> `' f : B -1-1-onto-> A ) )
12 10 11 syl 
 |-  ( ( f : A -1-1-onto-> B /\ A e. V ) -> ( f : A -1-1-onto-> B <-> `' f : B -1-1-onto-> A ) )
13 f1of 
 |-  ( f : A -1-1-onto-> B -> f : A --> B )
14 fex 
 |-  ( ( f : A --> B /\ A e. V ) -> f e. _V )
15 13 14 sylan 
 |-  ( ( f : A -1-1-onto-> B /\ A e. V ) -> f e. _V )
16 cnvexg 
 |-  ( f e. _V -> `' f e. _V )
17 f1oeq1 
 |-  ( g = `' f -> ( g : B -1-1-onto-> A <-> `' f : B -1-1-onto-> A ) )
18 17 spcegv 
 |-  ( `' f e. _V -> ( `' f : B -1-1-onto-> A -> E. g g : B -1-1-onto-> A ) )
19 15 16 18 3syl 
 |-  ( ( f : A -1-1-onto-> B /\ A e. V ) -> ( `' f : B -1-1-onto-> A -> E. g g : B -1-1-onto-> A ) )
20 pm2.24 
 |-  ( E. g g : B -1-1-onto-> A -> ( -. E. g g : B -1-1-onto-> A -> ( # ` A ) = ( # ` B ) ) )
21 19 20 syl6 
 |-  ( ( f : A -1-1-onto-> B /\ A e. V ) -> ( `' f : B -1-1-onto-> A -> ( -. E. g g : B -1-1-onto-> A -> ( # ` A ) = ( # ` B ) ) ) )
22 12 21 sylbid 
 |-  ( ( f : A -1-1-onto-> B /\ A e. V ) -> ( f : A -1-1-onto-> B -> ( -. E. g g : B -1-1-onto-> A -> ( # ` A ) = ( # ` B ) ) ) )
23 22 com12 
 |-  ( f : A -1-1-onto-> B -> ( ( f : A -1-1-onto-> B /\ A e. V ) -> ( -. E. g g : B -1-1-onto-> A -> ( # ` A ) = ( # ` B ) ) ) )
24 23 anabsi5 
 |-  ( ( f : A -1-1-onto-> B /\ A e. V ) -> ( -. E. g g : B -1-1-onto-> A -> ( # ` A ) = ( # ` B ) ) )
25 24 exlimiv 
 |-  ( E. f ( f : A -1-1-onto-> B /\ A e. V ) -> ( -. E. g g : B -1-1-onto-> A -> ( # ` A ) = ( # ` B ) ) )
26 8 25 sylbir 
 |-  ( ( E. f f : A -1-1-onto-> B /\ A e. V ) -> ( -. E. g g : B -1-1-onto-> A -> ( # ` A ) = ( # ` B ) ) )
27 26 ex 
 |-  ( E. f f : A -1-1-onto-> B -> ( A e. V -> ( -. E. g g : B -1-1-onto-> A -> ( # ` A ) = ( # ` B ) ) ) )
28 27 com13 
 |-  ( -. E. g g : B -1-1-onto-> A -> ( A e. V -> ( E. f f : A -1-1-onto-> B -> ( # ` A ) = ( # ` B ) ) ) )
29 7 28 syl 
 |-  ( ( B e. Fin /\ -. A e. Fin ) -> ( A e. V -> ( E. f f : A -1-1-onto-> B -> ( # ` A ) = ( # ` B ) ) ) )
30 29 ancoms 
 |-  ( ( -. A e. Fin /\ B e. Fin ) -> ( A e. V -> ( E. f f : A -1-1-onto-> B -> ( # ` A ) = ( # ` B ) ) ) )
31 hashinf 
 |-  ( ( A e. V /\ -. A e. Fin ) -> ( # ` A ) = +oo )
32 31 expcom 
 |-  ( -. A e. Fin -> ( A e. V -> ( # ` A ) = +oo ) )
33 32 adantr 
 |-  ( ( -. A e. Fin /\ -. B e. Fin ) -> ( A e. V -> ( # ` A ) = +oo ) )
34 33 imp 
 |-  ( ( ( -. A e. Fin /\ -. B e. Fin ) /\ A e. V ) -> ( # ` A ) = +oo )
35 34 adantr 
 |-  ( ( ( ( -. A e. Fin /\ -. B e. Fin ) /\ A e. V ) /\ f : A -1-1-onto-> B ) -> ( # ` A ) = +oo )
36 simpr 
 |-  ( ( ( -. A e. Fin /\ -. B e. Fin ) /\ A e. V ) -> A e. V )
37 f1ofo 
 |-  ( f : A -1-1-onto-> B -> f : A -onto-> B )
38 focdmex 
 |-  ( A e. V -> ( f : A -onto-> B -> B e. _V ) )
39 38 imp 
 |-  ( ( A e. V /\ f : A -onto-> B ) -> B e. _V )
40 36 37 39 syl2an 
 |-  ( ( ( ( -. A e. Fin /\ -. B e. Fin ) /\ A e. V ) /\ f : A -1-1-onto-> B ) -> B e. _V )
41 hashinf 
 |-  ( ( B e. _V /\ -. B e. Fin ) -> ( # ` B ) = +oo )
42 41 expcom 
 |-  ( -. B e. Fin -> ( B e. _V -> ( # ` B ) = +oo ) )
43 42 ad3antlr 
 |-  ( ( ( ( -. A e. Fin /\ -. B e. Fin ) /\ A e. V ) /\ f : A -1-1-onto-> B ) -> ( B e. _V -> ( # ` B ) = +oo ) )
44 40 43 mpd 
 |-  ( ( ( ( -. A e. Fin /\ -. B e. Fin ) /\ A e. V ) /\ f : A -1-1-onto-> B ) -> ( # ` B ) = +oo )
45 35 44 eqtr4d 
 |-  ( ( ( ( -. A e. Fin /\ -. B e. Fin ) /\ A e. V ) /\ f : A -1-1-onto-> B ) -> ( # ` A ) = ( # ` B ) )
46 45 ex 
 |-  ( ( ( -. A e. Fin /\ -. B e. Fin ) /\ A e. V ) -> ( f : A -1-1-onto-> B -> ( # ` A ) = ( # ` B ) ) )
47 46 exlimdv 
 |-  ( ( ( -. A e. Fin /\ -. B e. Fin ) /\ A e. V ) -> ( E. f f : A -1-1-onto-> B -> ( # ` A ) = ( # ` B ) ) )
48 47 ex 
 |-  ( ( -. A e. Fin /\ -. B e. Fin ) -> ( A e. V -> ( E. f f : A -1-1-onto-> B -> ( # ` A ) = ( # ` B ) ) ) )
49 3 6 30 48 4cases 
 |-  ( A e. V -> ( E. f f : A -1-1-onto-> B -> ( # ` A ) = ( # ` B ) ) )