Step | Hyp | Ref
| Expression |
1 | | hasheqf1o 12999 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
((#‘𝐴) =
(#‘𝐵) ↔
∃𝑓 𝑓:𝐴–1-1-onto→𝐵)) |
2 | 1 | biimprd 237 |
. . 3
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
(∃𝑓 𝑓:𝐴–1-1-onto→𝐵 → (#‘𝐴) = (#‘𝐵))) |
3 | 2 | a1d 25 |
. 2
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∃𝑓 𝑓:𝐴–1-1-onto→𝐵 → (#‘𝐴) = (#‘𝐵)))) |
4 | | fiinfnf1o 13000 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ ¬ 𝐵 ∈ Fin) → ¬
∃𝑓 𝑓:𝐴–1-1-onto→𝐵) |
5 | 4 | pm2.21d 117 |
. . 3
⊢ ((𝐴 ∈ Fin ∧ ¬ 𝐵 ∈ Fin) →
(∃𝑓 𝑓:𝐴–1-1-onto→𝐵 → (#‘𝐴) = (#‘𝐵))) |
6 | 5 | a1d 25 |
. 2
⊢ ((𝐴 ∈ Fin ∧ ¬ 𝐵 ∈ Fin) → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∃𝑓 𝑓:𝐴–1-1-onto→𝐵 → (#‘𝐴) = (#‘𝐵)))) |
7 | | fiinfnf1o 13000 |
. . . 4
⊢ ((𝐵 ∈ Fin ∧ ¬ 𝐴 ∈ Fin) → ¬
∃𝑔 𝑔:𝐵–1-1-onto→𝐴) |
8 | | 19.41v 1901 |
. . . . . . 7
⊢
(∃𝑓(𝑓:𝐴–1-1-onto→𝐵 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) ↔ (∃𝑓 𝑓:𝐴–1-1-onto→𝐵 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊))) |
9 | | f1orel 6053 |
. . . . . . . . . . . . 13
⊢ (𝑓:𝐴–1-1-onto→𝐵 → Rel 𝑓) |
10 | 9 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → Rel 𝑓) |
11 | | f1ocnvb 6063 |
. . . . . . . . . . . 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 6050 |
. . . . . . . . . . . . . . 15
⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝑓:𝐴⟶𝐵) |
14 | 13 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → 𝑓:𝐴⟶𝐵) |
15 | | simprl 790 |
. . . . . . . . . . . . . 14
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → 𝐴 ∈ 𝑉) |
16 | | simprr 792 |
. . . . . . . . . . . . . 14
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → 𝐵 ∈ 𝑊) |
17 | | fex2 7014 |
. . . . . . . . . . . . . 14
⊢ ((𝑓:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝑓 ∈ V) |
18 | 14, 15, 16, 17 | syl3anc 1318 |
. . . . . . . . . . . . 13
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → 𝑓 ∈ V) |
19 | | cnvexg 7005 |
. . . . . . . . . . . . 13
⊢ (𝑓 ∈ V → ◡𝑓 ∈ V) |
20 | | f1oeq1 6040 |
. . . . . . . . . . . . . 14
⊢ (𝑔 = ◡𝑓 → (𝑔:𝐵–1-1-onto→𝐴 ↔ ◡𝑓:𝐵–1-1-onto→𝐴)) |
21 | 20 | spcegv 3267 |
. . . . . . . . . . . . 13
⊢ (◡𝑓 ∈ V → (◡𝑓:𝐵–1-1-onto→𝐴 → ∃𝑔 𝑔:𝐵–1-1-onto→𝐴)) |
22 | 18, 19, 21 | 3syl 18 |
. . . . . . . . . . . 12
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → (◡𝑓:𝐵–1-1-onto→𝐴 → ∃𝑔 𝑔:𝐵–1-1-onto→𝐴)) |
23 | | pm2.24 120 |
. . . . . . . . . . . 12
⊢
(∃𝑔 𝑔:𝐵–1-1-onto→𝐴 → (¬ ∃𝑔 𝑔:𝐵–1-1-onto→𝐴 → (#‘𝐴) = (#‘𝐵))) |
24 | 22, 23 | syl6 34 |
. . . . . . . . . . 11
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → (◡𝑓:𝐵–1-1-onto→𝐴 → (¬ ∃𝑔 𝑔:𝐵–1-1-onto→𝐴 → (#‘𝐴) = (#‘𝐵)))) |
25 | 12, 24 | sylbid 229 |
. . . . . . . . . 10
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → (𝑓:𝐴–1-1-onto→𝐵 → (¬ ∃𝑔 𝑔:𝐵–1-1-onto→𝐴 → (#‘𝐴) = (#‘𝐵)))) |
26 | 25 | com12 32 |
. . . . . . . . 9
⊢ (𝑓:𝐴–1-1-onto→𝐵 → ((𝑓:𝐴–1-1-onto→𝐵 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → (¬ ∃𝑔 𝑔:𝐵–1-1-onto→𝐴 → (#‘𝐴) = (#‘𝐵)))) |
27 | 26 | anabsi5 854 |
. . . . . . . 8
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → (¬ ∃𝑔 𝑔:𝐵–1-1-onto→𝐴 → (#‘𝐴) = (#‘𝐵))) |
28 | 27 | exlimiv 1845 |
. . . . . . 7
⊢
(∃𝑓(𝑓:𝐴–1-1-onto→𝐵 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → (¬ ∃𝑔 𝑔:𝐵–1-1-onto→𝐴 → (#‘𝐴) = (#‘𝐵))) |
29 | 8, 28 | sylbir 224 |
. . . . . 6
⊢
((∃𝑓 𝑓:𝐴–1-1-onto→𝐵 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → (¬ ∃𝑔 𝑔:𝐵–1-1-onto→𝐴 → (#‘𝐴) = (#‘𝐵))) |
30 | 29 | ex 449 |
. . . . 5
⊢
(∃𝑓 𝑓:𝐴–1-1-onto→𝐵 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (¬ ∃𝑔 𝑔:𝐵–1-1-onto→𝐴 → (#‘𝐴) = (#‘𝐵)))) |
31 | 30 | com13 86 |
. . . 4
⊢ (¬
∃𝑔 𝑔:𝐵–1-1-onto→𝐴 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∃𝑓 𝑓:𝐴–1-1-onto→𝐵 → (#‘𝐴) = (#‘𝐵)))) |
32 | 7, 31 | syl 17 |
. . 3
⊢ ((𝐵 ∈ Fin ∧ ¬ 𝐴 ∈ Fin) → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∃𝑓 𝑓:𝐴–1-1-onto→𝐵 → (#‘𝐴) = (#‘𝐵)))) |
33 | 32 | ancoms 468 |
. 2
⊢ ((¬
𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∃𝑓 𝑓:𝐴–1-1-onto→𝐵 → (#‘𝐴) = (#‘𝐵)))) |
34 | | hashinf 12984 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → (#‘𝐴) = +∞) |
35 | 34 | expcom 450 |
. . . . . . . . 9
⊢ (¬
𝐴 ∈ Fin → (𝐴 ∈ 𝑉 → (#‘𝐴) = +∞)) |
36 | 35 | adantr 480 |
. . . . . . . 8
⊢ ((¬
𝐴 ∈ Fin ∧ ¬
𝐵 ∈ Fin) → (𝐴 ∈ 𝑉 → (#‘𝐴) = +∞)) |
37 | 36 | com12 32 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑉 → ((¬ 𝐴 ∈ Fin ∧ ¬ 𝐵 ∈ Fin) → (#‘𝐴) = +∞)) |
38 | 37 | adantr 480 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((¬ 𝐴 ∈ Fin ∧ ¬ 𝐵 ∈ Fin) → (#‘𝐴) = +∞)) |
39 | 38 | impcom 445 |
. . . . 5
⊢ (((¬
𝐴 ∈ Fin ∧ ¬
𝐵 ∈ Fin) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → (#‘𝐴) = +∞) |
40 | | hashinf 12984 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ 𝑊 ∧ ¬ 𝐵 ∈ Fin) → (#‘𝐵) = +∞) |
41 | 40 | expcom 450 |
. . . . . . . . 9
⊢ (¬
𝐵 ∈ Fin → (𝐵 ∈ 𝑊 → (#‘𝐵) = +∞)) |
42 | 41 | adantl 481 |
. . . . . . . 8
⊢ ((¬
𝐴 ∈ Fin ∧ ¬
𝐵 ∈ Fin) → (𝐵 ∈ 𝑊 → (#‘𝐵) = +∞)) |
43 | 42 | com12 32 |
. . . . . . 7
⊢ (𝐵 ∈ 𝑊 → ((¬ 𝐴 ∈ Fin ∧ ¬ 𝐵 ∈ Fin) → (#‘𝐵) = +∞)) |
44 | 43 | adantl 481 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((¬ 𝐴 ∈ Fin ∧ ¬ 𝐵 ∈ Fin) → (#‘𝐵) = +∞)) |
45 | 44 | impcom 445 |
. . . . 5
⊢ (((¬
𝐴 ∈ Fin ∧ ¬
𝐵 ∈ Fin) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → (#‘𝐵) = +∞) |
46 | 39, 45 | eqtr4d 2647 |
. . . 4
⊢ (((¬
𝐴 ∈ Fin ∧ ¬
𝐵 ∈ Fin) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → (#‘𝐴) = (#‘𝐵)) |
47 | 46 | a1d 25 |
. . 3
⊢ (((¬
𝐴 ∈ Fin ∧ ¬
𝐵 ∈ Fin) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → (∃𝑓 𝑓:𝐴–1-1-onto→𝐵 → (#‘𝐴) = (#‘𝐵))) |
48 | 47 | ex 449 |
. 2
⊢ ((¬
𝐴 ∈ Fin ∧ ¬
𝐵 ∈ Fin) →
((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∃𝑓 𝑓:𝐴–1-1-onto→𝐵 → (#‘𝐴) = (#‘𝐵)))) |
49 | 3, 6, 33, 48 | 4cases 987 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∃𝑓 𝑓:𝐴–1-1-onto→𝐵 → (#‘𝐴) = (#‘𝐵))) |