| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | hasheqf1o 14388 | . . . 4
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
((♯‘𝐴) =
(♯‘𝐵) ↔
∃𝑓 𝑓:𝐴–1-1-onto→𝐵)) | 
| 2 | 1 | biimprd 248 | . . 3
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
(∃𝑓 𝑓:𝐴–1-1-onto→𝐵 → (♯‘𝐴) = (♯‘𝐵))) | 
| 3 | 2 | a1d 25 | . 2
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 ∈ 𝑉 → (∃𝑓 𝑓:𝐴–1-1-onto→𝐵 → (♯‘𝐴) = (♯‘𝐵)))) | 
| 4 |  | fiinfnf1o 14389 | . . . 4
⊢ ((𝐴 ∈ Fin ∧ ¬ 𝐵 ∈ Fin) → ¬
∃𝑓 𝑓:𝐴–1-1-onto→𝐵) | 
| 5 | 4 | pm2.21d 121 | . . 3
⊢ ((𝐴 ∈ Fin ∧ ¬ 𝐵 ∈ Fin) →
(∃𝑓 𝑓:𝐴–1-1-onto→𝐵 → (♯‘𝐴) = (♯‘𝐵))) | 
| 6 | 5 | a1d 25 | . 2
⊢ ((𝐴 ∈ Fin ∧ ¬ 𝐵 ∈ Fin) → (𝐴 ∈ 𝑉 → (∃𝑓 𝑓:𝐴–1-1-onto→𝐵 → (♯‘𝐴) = (♯‘𝐵)))) | 
| 7 |  | fiinfnf1o 14389 | . . . 4
⊢ ((𝐵 ∈ Fin ∧ ¬ 𝐴 ∈ Fin) → ¬
∃𝑔 𝑔:𝐵–1-1-onto→𝐴) | 
| 8 |  | 19.41v 1949 | . . . . . . 7
⊢
(∃𝑓(𝑓:𝐴–1-1-onto→𝐵 ∧ 𝐴 ∈ 𝑉) ↔ (∃𝑓 𝑓:𝐴–1-1-onto→𝐵 ∧ 𝐴 ∈ 𝑉)) | 
| 9 |  | f1orel 6851 | . . . . . . . . . . . . 13
⊢ (𝑓:𝐴–1-1-onto→𝐵 → Rel 𝑓) | 
| 10 | 9 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝐴 ∈ 𝑉) → Rel 𝑓) | 
| 11 |  | f1ocnvb 6861 | . . . . . . . . . . . 12
⊢ (Rel
𝑓 → (𝑓:𝐴–1-1-onto→𝐵 ↔ ◡𝑓:𝐵–1-1-onto→𝐴)) | 
| 12 | 10, 11 | syl 17 | . . . . . . . . . . 11
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝐴 ∈ 𝑉) → (𝑓:𝐴–1-1-onto→𝐵 ↔ ◡𝑓:𝐵–1-1-onto→𝐴)) | 
| 13 |  | f1of 6848 | . . . . . . . . . . . . . 14
⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝑓:𝐴⟶𝐵) | 
| 14 |  | fex 7246 | . . . . . . . . . . . . . 14
⊢ ((𝑓:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉) → 𝑓 ∈ V) | 
| 15 | 13, 14 | sylan 580 | . . . . . . . . . . . . 13
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝐴 ∈ 𝑉) → 𝑓 ∈ V) | 
| 16 |  | cnvexg 7946 | . . . . . . . . . . . . 13
⊢ (𝑓 ∈ V → ◡𝑓 ∈ V) | 
| 17 |  | f1oeq1 6836 | . . . . . . . . . . . . . 14
⊢ (𝑔 = ◡𝑓 → (𝑔:𝐵–1-1-onto→𝐴 ↔ ◡𝑓:𝐵–1-1-onto→𝐴)) | 
| 18 | 17 | spcegv 3597 | . . . . . . . . . . . . 13
⊢ (◡𝑓 ∈ V → (◡𝑓:𝐵–1-1-onto→𝐴 → ∃𝑔 𝑔:𝐵–1-1-onto→𝐴)) | 
| 19 | 15, 16, 18 | 3syl 18 | . . . . . . . . . . . 12
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝐴 ∈ 𝑉) → (◡𝑓:𝐵–1-1-onto→𝐴 → ∃𝑔 𝑔:𝐵–1-1-onto→𝐴)) | 
| 20 |  | pm2.24 124 | . . . . . . . . . . . 12
⊢
(∃𝑔 𝑔:𝐵–1-1-onto→𝐴 → (¬ ∃𝑔 𝑔:𝐵–1-1-onto→𝐴 → (♯‘𝐴) = (♯‘𝐵))) | 
| 21 | 19, 20 | syl6 35 | . . . . . . . . . . 11
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝐴 ∈ 𝑉) → (◡𝑓:𝐵–1-1-onto→𝐴 → (¬ ∃𝑔 𝑔:𝐵–1-1-onto→𝐴 → (♯‘𝐴) = (♯‘𝐵)))) | 
| 22 | 12, 21 | sylbid 240 | . . . . . . . . . 10
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝐴 ∈ 𝑉) → (𝑓:𝐴–1-1-onto→𝐵 → (¬ ∃𝑔 𝑔:𝐵–1-1-onto→𝐴 → (♯‘𝐴) = (♯‘𝐵)))) | 
| 23 | 22 | com12 32 | . . . . . . . . 9
⊢ (𝑓:𝐴–1-1-onto→𝐵 → ((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝐴 ∈ 𝑉) → (¬ ∃𝑔 𝑔:𝐵–1-1-onto→𝐴 → (♯‘𝐴) = (♯‘𝐵)))) | 
| 24 | 23 | anabsi5 669 | . . . . . . . 8
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝐴 ∈ 𝑉) → (¬ ∃𝑔 𝑔:𝐵–1-1-onto→𝐴 → (♯‘𝐴) = (♯‘𝐵))) | 
| 25 | 24 | exlimiv 1930 | . . . . . . 7
⊢
(∃𝑓(𝑓:𝐴–1-1-onto→𝐵 ∧ 𝐴 ∈ 𝑉) → (¬ ∃𝑔 𝑔:𝐵–1-1-onto→𝐴 → (♯‘𝐴) = (♯‘𝐵))) | 
| 26 | 8, 25 | sylbir 235 | . . . . . 6
⊢
((∃𝑓 𝑓:𝐴–1-1-onto→𝐵 ∧ 𝐴 ∈ 𝑉) → (¬ ∃𝑔 𝑔:𝐵–1-1-onto→𝐴 → (♯‘𝐴) = (♯‘𝐵))) | 
| 27 | 26 | ex 412 | . . . . 5
⊢
(∃𝑓 𝑓:𝐴–1-1-onto→𝐵 → (𝐴 ∈ 𝑉 → (¬ ∃𝑔 𝑔:𝐵–1-1-onto→𝐴 → (♯‘𝐴) = (♯‘𝐵)))) | 
| 28 | 27 | com13 88 | . . . 4
⊢ (¬
∃𝑔 𝑔:𝐵–1-1-onto→𝐴 → (𝐴 ∈ 𝑉 → (∃𝑓 𝑓:𝐴–1-1-onto→𝐵 → (♯‘𝐴) = (♯‘𝐵)))) | 
| 29 | 7, 28 | syl 17 | . . 3
⊢ ((𝐵 ∈ Fin ∧ ¬ 𝐴 ∈ Fin) → (𝐴 ∈ 𝑉 → (∃𝑓 𝑓:𝐴–1-1-onto→𝐵 → (♯‘𝐴) = (♯‘𝐵)))) | 
| 30 | 29 | ancoms 458 | . 2
⊢ ((¬
𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 ∈ 𝑉 → (∃𝑓 𝑓:𝐴–1-1-onto→𝐵 → (♯‘𝐴) = (♯‘𝐵)))) | 
| 31 |  | hashinf 14374 | . . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → (♯‘𝐴) = +∞) | 
| 32 | 31 | expcom 413 | . . . . . . . . 9
⊢ (¬
𝐴 ∈ Fin → (𝐴 ∈ 𝑉 → (♯‘𝐴) = +∞)) | 
| 33 | 32 | adantr 480 | . . . . . . . 8
⊢ ((¬
𝐴 ∈ Fin ∧ ¬
𝐵 ∈ Fin) → (𝐴 ∈ 𝑉 → (♯‘𝐴) = +∞)) | 
| 34 | 33 | imp 406 | . . . . . . 7
⊢ (((¬
𝐴 ∈ Fin ∧ ¬
𝐵 ∈ Fin) ∧ 𝐴 ∈ 𝑉) → (♯‘𝐴) = +∞) | 
| 35 | 34 | adantr 480 | . . . . . 6
⊢ ((((¬
𝐴 ∈ Fin ∧ ¬
𝐵 ∈ Fin) ∧ 𝐴 ∈ 𝑉) ∧ 𝑓:𝐴–1-1-onto→𝐵) → (♯‘𝐴) = +∞) | 
| 36 |  | simpr 484 | . . . . . . . 8
⊢ (((¬
𝐴 ∈ Fin ∧ ¬
𝐵 ∈ Fin) ∧ 𝐴 ∈ 𝑉) → 𝐴 ∈ 𝑉) | 
| 37 |  | f1ofo 6855 | . . . . . . . 8
⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝑓:𝐴–onto→𝐵) | 
| 38 |  | focdmex 7980 | . . . . . . . . 9
⊢ (𝐴 ∈ 𝑉 → (𝑓:𝐴–onto→𝐵 → 𝐵 ∈ V)) | 
| 39 | 38 | imp 406 | . . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑓:𝐴–onto→𝐵) → 𝐵 ∈ V) | 
| 40 | 36, 37, 39 | syl2an 596 | . . . . . . 7
⊢ ((((¬
𝐴 ∈ Fin ∧ ¬
𝐵 ∈ Fin) ∧ 𝐴 ∈ 𝑉) ∧ 𝑓:𝐴–1-1-onto→𝐵) → 𝐵 ∈ V) | 
| 41 |  | hashinf 14374 | . . . . . . . . 9
⊢ ((𝐵 ∈ V ∧ ¬ 𝐵 ∈ Fin) →
(♯‘𝐵) =
+∞) | 
| 42 | 41 | expcom 413 | . . . . . . . 8
⊢ (¬
𝐵 ∈ Fin → (𝐵 ∈ V →
(♯‘𝐵) =
+∞)) | 
| 43 | 42 | ad3antlr 731 | . . . . . . 7
⊢ ((((¬
𝐴 ∈ Fin ∧ ¬
𝐵 ∈ Fin) ∧ 𝐴 ∈ 𝑉) ∧ 𝑓:𝐴–1-1-onto→𝐵) → (𝐵 ∈ V → (♯‘𝐵) = +∞)) | 
| 44 | 40, 43 | mpd 15 | . . . . . 6
⊢ ((((¬
𝐴 ∈ Fin ∧ ¬
𝐵 ∈ Fin) ∧ 𝐴 ∈ 𝑉) ∧ 𝑓:𝐴–1-1-onto→𝐵) → (♯‘𝐵) = +∞) | 
| 45 | 35, 44 | eqtr4d 2780 | . . . . 5
⊢ ((((¬
𝐴 ∈ Fin ∧ ¬
𝐵 ∈ Fin) ∧ 𝐴 ∈ 𝑉) ∧ 𝑓:𝐴–1-1-onto→𝐵) → (♯‘𝐴) = (♯‘𝐵)) | 
| 46 | 45 | ex 412 | . . . 4
⊢ (((¬
𝐴 ∈ Fin ∧ ¬
𝐵 ∈ Fin) ∧ 𝐴 ∈ 𝑉) → (𝑓:𝐴–1-1-onto→𝐵 → (♯‘𝐴) = (♯‘𝐵))) | 
| 47 | 46 | exlimdv 1933 | . . 3
⊢ (((¬
𝐴 ∈ Fin ∧ ¬
𝐵 ∈ Fin) ∧ 𝐴 ∈ 𝑉) → (∃𝑓 𝑓:𝐴–1-1-onto→𝐵 → (♯‘𝐴) = (♯‘𝐵))) | 
| 48 | 47 | ex 412 | . 2
⊢ ((¬
𝐴 ∈ Fin ∧ ¬
𝐵 ∈ Fin) → (𝐴 ∈ 𝑉 → (∃𝑓 𝑓:𝐴–1-1-onto→𝐵 → (♯‘𝐴) = (♯‘𝐵)))) | 
| 49 | 3, 6, 30, 48 | 4cases 1041 | 1
⊢ (𝐴 ∈ 𝑉 → (∃𝑓 𝑓:𝐴–1-1-onto→𝐵 → (♯‘𝐴) = (♯‘𝐵))) |