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 ( 𝐴 ∈ 𝑉 → ( ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ 𝐵 → ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 hasheqf1o ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) ↔ ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) )
2 1 biimprd ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ 𝐵 → ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) ) )
3 2 a1d ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( 𝐴 ∈ 𝑉 → ( ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ 𝐵 → ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) ) ) )
4 fiinfnf1o ⊢ ( ( 𝐴 ∈ Fin ∧ ¬ 𝐵 ∈ Fin ) → ¬ ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ 𝐵 )
5 4 pm2.21d ⊢ ( ( 𝐴 ∈ Fin ∧ ¬ 𝐵 ∈ Fin ) → ( ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ 𝐵 → ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) ) )
6 5 a1d ⊢ ( ( 𝐴 ∈ Fin ∧ ¬ 𝐵 ∈ Fin ) → ( 𝐴 ∈ 𝑉 → ( ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ 𝐵 → ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) ) ) )
7 fiinfnf1o ⊢ ( ( 𝐵 ∈ Fin ∧ ¬ 𝐴 ∈ Fin ) → ¬ ∃ 𝑔 𝑔 : 𝐵 –1-1-onto→ 𝐴 )
8 19.41v ⊢ ( ∃ 𝑓 ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐴 ∈ 𝑉 ) ↔ ( ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐴 ∈ 𝑉 ) )
9 f1orel ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → Rel 𝑓 )
10 9 adantr ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐴 ∈ 𝑉 ) → Rel 𝑓 )
11 f1ocnvb ⊢ ( Rel 𝑓 → ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ↔ ◡ 𝑓 : 𝐵 –1-1-onto→ 𝐴 ) )
12 10 11 syl ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐴 ∈ 𝑉 ) → ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ↔ ◡ 𝑓 : 𝐵 –1-1-onto→ 𝐴 ) )
13 f1of ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → 𝑓 : 𝐴 ⟶ 𝐵 )
14 fex ⊢ ( ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑉 ) → 𝑓 ∈ V )
15 13 14 sylan ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐴 ∈ 𝑉 ) → 𝑓 ∈ V )
16 cnvexg ⊢ ( 𝑓 ∈ V → ◡ 𝑓 ∈ V )
17 f1oeq1 ⊢ ( 𝑔 = ◡ 𝑓 → ( 𝑔 : 𝐵 –1-1-onto→ 𝐴 ↔ ◡ 𝑓 : 𝐵 –1-1-onto→ 𝐴 ) )
18 17 spcegv ⊢ ( ◡ 𝑓 ∈ V → ( ◡ 𝑓 : 𝐵 –1-1-onto→ 𝐴 → ∃ 𝑔 𝑔 : 𝐵 –1-1-onto→ 𝐴 ) )
19 15 16 18 3syl ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐴 ∈ 𝑉 ) → ( ◡ 𝑓 : 𝐵 –1-1-onto→ 𝐴 → ∃ 𝑔 𝑔 : 𝐵 –1-1-onto→ 𝐴 ) )
20 pm2.24 ⊢ ( ∃ 𝑔 𝑔 : 𝐵 –1-1-onto→ 𝐴 → ( ¬ ∃ 𝑔 𝑔 : 𝐵 –1-1-onto→ 𝐴 → ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) ) )
21 19 20 syl6 ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐴 ∈ 𝑉 ) → ( ◡ 𝑓 : 𝐵 –1-1-onto→ 𝐴 → ( ¬ ∃ 𝑔 𝑔 : 𝐵 –1-1-onto→ 𝐴 → ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) ) ) )
22 12 21 sylbid ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐴 ∈ 𝑉 ) → ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → ( ¬ ∃ 𝑔 𝑔 : 𝐵 –1-1-onto→ 𝐴 → ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) ) ) )
23 22 com12 ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐴 ∈ 𝑉 ) → ( ¬ ∃ 𝑔 𝑔 : 𝐵 –1-1-onto→ 𝐴 → ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) ) ) )
24 23 anabsi5 ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐴 ∈ 𝑉 ) → ( ¬ ∃ 𝑔 𝑔 : 𝐵 –1-1-onto→ 𝐴 → ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) ) )
25 24 exlimiv ⊢ ( ∃ 𝑓 ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐴 ∈ 𝑉 ) → ( ¬ ∃ 𝑔 𝑔 : 𝐵 –1-1-onto→ 𝐴 → ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) ) )
26 8 25 sylbir ⊢ ( ( ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐴 ∈ 𝑉 ) → ( ¬ ∃ 𝑔 𝑔 : 𝐵 –1-1-onto→ 𝐴 → ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) ) )
27 26 ex ⊢ ( ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ 𝐵 → ( 𝐴 ∈ 𝑉 → ( ¬ ∃ 𝑔 𝑔 : 𝐵 –1-1-onto→ 𝐴 → ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) ) ) )
28 27 com13 ⊢ ( ¬ ∃ 𝑔 𝑔 : 𝐵 –1-1-onto→ 𝐴 → ( 𝐴 ∈ 𝑉 → ( ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ 𝐵 → ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) ) ) )
29 7 28 syl ⊢ ( ( 𝐵 ∈ Fin ∧ ¬ 𝐴 ∈ Fin ) → ( 𝐴 ∈ 𝑉 → ( ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ 𝐵 → ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) ) ) )
30 29 ancoms ⊢ ( ( ¬ 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( 𝐴 ∈ 𝑉 → ( ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ 𝐵 → ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) ) ) )
31 hashinf ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin ) → ( ♯ ‘ 𝐴 ) = +∞ )
32 31 expcom ⊢ ( ¬ 𝐴 ∈ Fin → ( 𝐴 ∈ 𝑉 → ( ♯ ‘ 𝐴 ) = +∞ ) )
33 32 adantr ⊢ ( ( ¬ 𝐴 ∈ Fin ∧ ¬ 𝐵 ∈ Fin ) → ( 𝐴 ∈ 𝑉 → ( ♯ ‘ 𝐴 ) = +∞ ) )
34 33 imp ⊢ ( ( ( ¬ 𝐴 ∈ Fin ∧ ¬ 𝐵 ∈ Fin ) ∧ 𝐴 ∈ 𝑉 ) → ( ♯ ‘ 𝐴 ) = +∞ )
35 34 adantr ⊢ ( ( ( ( ¬ 𝐴 ∈ Fin ∧ ¬ 𝐵 ∈ Fin ) ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) → ( ♯ ‘ 𝐴 ) = +∞ )
36 simpr ⊢ ( ( ( ¬ 𝐴 ∈ Fin ∧ ¬ 𝐵 ∈ Fin ) ∧ 𝐴 ∈ 𝑉 ) → 𝐴 ∈ 𝑉 )
37 f1ofo ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → 𝑓 : 𝐴 –onto→ 𝐵 )
38 focdmex ⊢ ( 𝐴 ∈ 𝑉 → ( 𝑓 : 𝐴 –onto→ 𝐵 → 𝐵 ∈ V ) )
39 38 imp ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑓 : 𝐴 –onto→ 𝐵 ) → 𝐵 ∈ V )
40 36 37 39 syl2an ⊢ ( ( ( ( ¬ 𝐴 ∈ Fin ∧ ¬ 𝐵 ∈ Fin ) ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) → 𝐵 ∈ V )
41 hashinf ⊢ ( ( 𝐵 ∈ V ∧ ¬ 𝐵 ∈ Fin ) → ( ♯ ‘ 𝐵 ) = +∞ )
42 41 expcom ⊢ ( ¬ 𝐵 ∈ Fin → ( 𝐵 ∈ V → ( ♯ ‘ 𝐵 ) = +∞ ) )
43 42 ad3antlr ⊢ ( ( ( ( ¬ 𝐴 ∈ Fin ∧ ¬ 𝐵 ∈ Fin ) ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) → ( 𝐵 ∈ V → ( ♯ ‘ 𝐵 ) = +∞ ) )
44 40 43 mpd ⊢ ( ( ( ( ¬ 𝐴 ∈ Fin ∧ ¬ 𝐵 ∈ Fin ) ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) → ( ♯ ‘ 𝐵 ) = +∞ )
45 35 44 eqtr4d ⊢ ( ( ( ( ¬ 𝐴 ∈ Fin ∧ ¬ 𝐵 ∈ Fin ) ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) → ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) )
46 45 ex ⊢ ( ( ( ¬ 𝐴 ∈ Fin ∧ ¬ 𝐵 ∈ Fin ) ∧ 𝐴 ∈ 𝑉 ) → ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) ) )
47 46 exlimdv ⊢ ( ( ( ¬ 𝐴 ∈ Fin ∧ ¬ 𝐵 ∈ Fin ) ∧ 𝐴 ∈ 𝑉 ) → ( ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ 𝐵 → ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) ) )
48 47 ex ⊢ ( ( ¬ 𝐴 ∈ Fin ∧ ¬ 𝐵 ∈ Fin ) → ( 𝐴 ∈ 𝑉 → ( ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ 𝐵 → ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) ) ) )
49 3 6 30 48 4cases ⊢ ( 𝐴 ∈ 𝑉 → ( ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ 𝐵 → ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) ) )