Step | Hyp | Ref
| Expression |
1 | | ficardom 8787 |
. . 3
⊢ (𝐵 ∈ Fin →
(card‘𝐵) ∈
ω) |
2 | | isinf 8173 |
. . 3
⊢ (¬
𝐴 ∈ Fin →
∀𝑎 ∈ ω
∃𝑐(𝑐 ⊆ 𝐴 ∧ 𝑐 ≈ 𝑎)) |
3 | | breq2 4657 |
. . . . . 6
⊢ (𝑎 = (card‘𝐵) → (𝑐 ≈ 𝑎 ↔ 𝑐 ≈ (card‘𝐵))) |
4 | 3 | anbi2d 740 |
. . . . 5
⊢ (𝑎 = (card‘𝐵) → ((𝑐 ⊆ 𝐴 ∧ 𝑐 ≈ 𝑎) ↔ (𝑐 ⊆ 𝐴 ∧ 𝑐 ≈ (card‘𝐵)))) |
5 | 4 | exbidv 1850 |
. . . 4
⊢ (𝑎 = (card‘𝐵) → (∃𝑐(𝑐 ⊆ 𝐴 ∧ 𝑐 ≈ 𝑎) ↔ ∃𝑐(𝑐 ⊆ 𝐴 ∧ 𝑐 ≈ (card‘𝐵)))) |
6 | 5 | rspcva 3307 |
. . 3
⊢
(((card‘𝐵)
∈ ω ∧ ∀𝑎 ∈ ω ∃𝑐(𝑐 ⊆ 𝐴 ∧ 𝑐 ≈ 𝑎)) → ∃𝑐(𝑐 ⊆ 𝐴 ∧ 𝑐 ≈ (card‘𝐵))) |
7 | 1, 2, 6 | syl2anr 495 |
. 2
⊢ ((¬
𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ∃𝑐(𝑐 ⊆ 𝐴 ∧ 𝑐 ≈ (card‘𝐵))) |
8 | | simprr 796 |
. . . . . 6
⊢ (((¬
𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (𝑐 ⊆ 𝐴 ∧ 𝑐 ≈ (card‘𝐵))) → 𝑐 ≈ (card‘𝐵)) |
9 | | ficardid 8788 |
. . . . . . 7
⊢ (𝐵 ∈ Fin →
(card‘𝐵) ≈
𝐵) |
10 | 9 | ad2antlr 763 |
. . . . . 6
⊢ (((¬
𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (𝑐 ⊆ 𝐴 ∧ 𝑐 ≈ (card‘𝐵))) → (card‘𝐵) ≈ 𝐵) |
11 | | entr 8008 |
. . . . . 6
⊢ ((𝑐 ≈ (card‘𝐵) ∧ (card‘𝐵) ≈ 𝐵) → 𝑐 ≈ 𝐵) |
12 | 8, 10, 11 | syl2anc 693 |
. . . . 5
⊢ (((¬
𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (𝑐 ⊆ 𝐴 ∧ 𝑐 ≈ (card‘𝐵))) → 𝑐 ≈ 𝐵) |
13 | 12 | ensymd 8007 |
. . . 4
⊢ (((¬
𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (𝑐 ⊆ 𝐴 ∧ 𝑐 ≈ (card‘𝐵))) → 𝐵 ≈ 𝑐) |
14 | | bren 7964 |
. . . 4
⊢ (𝐵 ≈ 𝑐 ↔ ∃𝑓 𝑓:𝐵–1-1-onto→𝑐) |
15 | 13, 14 | sylib 208 |
. . 3
⊢ (((¬
𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (𝑐 ⊆ 𝐴 ∧ 𝑐 ≈ (card‘𝐵))) → ∃𝑓 𝑓:𝐵–1-1-onto→𝑐) |
16 | | f1of1 6136 |
. . . . . . 7
⊢ (𝑓:𝐵–1-1-onto→𝑐 → 𝑓:𝐵–1-1→𝑐) |
17 | 16 | adantl 482 |
. . . . . 6
⊢ ((((¬
𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (𝑐 ⊆ 𝐴 ∧ 𝑐 ≈ (card‘𝐵))) ∧ 𝑓:𝐵–1-1-onto→𝑐) → 𝑓:𝐵–1-1→𝑐) |
18 | | simplrl 800 |
. . . . . 6
⊢ ((((¬
𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (𝑐 ⊆ 𝐴 ∧ 𝑐 ≈ (card‘𝐵))) ∧ 𝑓:𝐵–1-1-onto→𝑐) → 𝑐 ⊆ 𝐴) |
19 | | f1ss 6106 |
. . . . . 6
⊢ ((𝑓:𝐵–1-1→𝑐 ∧ 𝑐 ⊆ 𝐴) → 𝑓:𝐵–1-1→𝐴) |
20 | 17, 18, 19 | syl2anc 693 |
. . . . 5
⊢ ((((¬
𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (𝑐 ⊆ 𝐴 ∧ 𝑐 ≈ (card‘𝐵))) ∧ 𝑓:𝐵–1-1-onto→𝑐) → 𝑓:𝐵–1-1→𝐴) |
21 | 20 | ex 450 |
. . . 4
⊢ (((¬
𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (𝑐 ⊆ 𝐴 ∧ 𝑐 ≈ (card‘𝐵))) → (𝑓:𝐵–1-1-onto→𝑐 → 𝑓:𝐵–1-1→𝐴)) |
22 | 21 | eximdv 1846 |
. . 3
⊢ (((¬
𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (𝑐 ⊆ 𝐴 ∧ 𝑐 ≈ (card‘𝐵))) → (∃𝑓 𝑓:𝐵–1-1-onto→𝑐 → ∃𝑓 𝑓:𝐵–1-1→𝐴)) |
23 | 15, 22 | mpd 15 |
. 2
⊢ (((¬
𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (𝑐 ⊆ 𝐴 ∧ 𝑐 ≈ (card‘𝐵))) → ∃𝑓 𝑓:𝐵–1-1→𝐴) |
24 | 7, 23 | exlimddv 1863 |
1
⊢ ((¬
𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ∃𝑓 𝑓:𝐵–1-1→𝐴) |