| Step | Hyp | Ref
| Expression |
| 1 | | isfi 9016 |
. . 3
⊢ (𝐴 ∈ Fin ↔ ∃𝑥 ∈ ω 𝐴 ≈ 𝑥) |
| 2 | | bren 8995 |
. . . . 5
⊢ (𝐴 ≈ 𝑥 ↔ ∃𝑧 𝑧:𝐴–1-1-onto→𝑥) |
| 3 | | f1ofo 6855 |
. . . . . . . . . . 11
⊢ (𝑧:𝐴–1-1-onto→𝑥 → 𝑧:𝐴–onto→𝑥) |
| 4 | | imassrn 6089 |
. . . . . . . . . . . 12
⊢ (𝑧 “ 𝐵) ⊆ ran 𝑧 |
| 5 | | forn 6823 |
. . . . . . . . . . . 12
⊢ (𝑧:𝐴–onto→𝑥 → ran 𝑧 = 𝑥) |
| 6 | 4, 5 | sseqtrid 4026 |
. . . . . . . . . . 11
⊢ (𝑧:𝐴–onto→𝑥 → (𝑧 “ 𝐵) ⊆ 𝑥) |
| 7 | 3, 6 | syl 17 |
. . . . . . . . . 10
⊢ (𝑧:𝐴–1-1-onto→𝑥 → (𝑧 “ 𝐵) ⊆ 𝑥) |
| 8 | | ssnnfi 9209 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ω ∧ (𝑧 “ 𝐵) ⊆ 𝑥) → (𝑧 “ 𝐵) ∈ Fin) |
| 9 | | isfi 9016 |
. . . . . . . . . . 11
⊢ ((𝑧 “ 𝐵) ∈ Fin ↔ ∃𝑦 ∈ ω (𝑧 “ 𝐵) ≈ 𝑦) |
| 10 | 8, 9 | sylib 218 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ω ∧ (𝑧 “ 𝐵) ⊆ 𝑥) → ∃𝑦 ∈ ω (𝑧 “ 𝐵) ≈ 𝑦) |
| 11 | 7, 10 | sylan2 593 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ω ∧ 𝑧:𝐴–1-1-onto→𝑥) → ∃𝑦 ∈ ω (𝑧 “ 𝐵) ≈ 𝑦) |
| 12 | 11 | adantrr 717 |
. . . . . . . 8
⊢ ((𝑥 ∈ ω ∧ (𝑧:𝐴–1-1-onto→𝑥 ∧ 𝐵 ⊆ 𝐴)) → ∃𝑦 ∈ ω (𝑧 “ 𝐵) ≈ 𝑦) |
| 13 | | f1of1 6847 |
. . . . . . . . . . . . . 14
⊢ (𝑧:𝐴–1-1-onto→𝑥 → 𝑧:𝐴–1-1→𝑥) |
| 14 | | f1ores 6862 |
. . . . . . . . . . . . . 14
⊢ ((𝑧:𝐴–1-1→𝑥 ∧ 𝐵 ⊆ 𝐴) → (𝑧 ↾ 𝐵):𝐵–1-1-onto→(𝑧 “ 𝐵)) |
| 15 | 13, 14 | sylan 580 |
. . . . . . . . . . . . 13
⊢ ((𝑧:𝐴–1-1-onto→𝑥 ∧ 𝐵 ⊆ 𝐴) → (𝑧 ↾ 𝐵):𝐵–1-1-onto→(𝑧 “ 𝐵)) |
| 16 | | vex 3484 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑧 ∈ V |
| 17 | 16 | resex 6047 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ↾ 𝐵) ∈ V |
| 18 | | f1oeq1 6836 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = (𝑧 ↾ 𝐵) → (𝑥:𝐵–1-1-onto→(𝑧 “ 𝐵) ↔ (𝑧 ↾ 𝐵):𝐵–1-1-onto→(𝑧 “ 𝐵))) |
| 19 | 17, 18 | spcev 3606 |
. . . . . . . . . . . . . . 15
⊢ ((𝑧 ↾ 𝐵):𝐵–1-1-onto→(𝑧 “ 𝐵) → ∃𝑥 𝑥:𝐵–1-1-onto→(𝑧 “ 𝐵)) |
| 20 | | bren 8995 |
. . . . . . . . . . . . . . 15
⊢ (𝐵 ≈ (𝑧 “ 𝐵) ↔ ∃𝑥 𝑥:𝐵–1-1-onto→(𝑧 “ 𝐵)) |
| 21 | 19, 20 | sylibr 234 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ↾ 𝐵):𝐵–1-1-onto→(𝑧 “ 𝐵) → 𝐵 ≈ (𝑧 “ 𝐵)) |
| 22 | | entr 9046 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ≈ (𝑧 “ 𝐵) ∧ (𝑧 “ 𝐵) ≈ 𝑦) → 𝐵 ≈ 𝑦) |
| 23 | 21, 22 | sylan 580 |
. . . . . . . . . . . . 13
⊢ (((𝑧 ↾ 𝐵):𝐵–1-1-onto→(𝑧 “ 𝐵) ∧ (𝑧 “ 𝐵) ≈ 𝑦) → 𝐵 ≈ 𝑦) |
| 24 | 15, 23 | sylan 580 |
. . . . . . . . . . . 12
⊢ (((𝑧:𝐴–1-1-onto→𝑥 ∧ 𝐵 ⊆ 𝐴) ∧ (𝑧 “ 𝐵) ≈ 𝑦) → 𝐵 ≈ 𝑦) |
| 25 | 24 | ex 412 |
. . . . . . . . . . 11
⊢ ((𝑧:𝐴–1-1-onto→𝑥 ∧ 𝐵 ⊆ 𝐴) → ((𝑧 “ 𝐵) ≈ 𝑦 → 𝐵 ≈ 𝑦)) |
| 26 | 25 | reximdv 3170 |
. . . . . . . . . 10
⊢ ((𝑧:𝐴–1-1-onto→𝑥 ∧ 𝐵 ⊆ 𝐴) → (∃𝑦 ∈ ω (𝑧 “ 𝐵) ≈ 𝑦 → ∃𝑦 ∈ ω 𝐵 ≈ 𝑦)) |
| 27 | | isfi 9016 |
. . . . . . . . . 10
⊢ (𝐵 ∈ Fin ↔ ∃𝑦 ∈ ω 𝐵 ≈ 𝑦) |
| 28 | 26, 27 | imbitrrdi 252 |
. . . . . . . . 9
⊢ ((𝑧:𝐴–1-1-onto→𝑥 ∧ 𝐵 ⊆ 𝐴) → (∃𝑦 ∈ ω (𝑧 “ 𝐵) ≈ 𝑦 → 𝐵 ∈ Fin)) |
| 29 | 28 | adantl 481 |
. . . . . . . 8
⊢ ((𝑥 ∈ ω ∧ (𝑧:𝐴–1-1-onto→𝑥 ∧ 𝐵 ⊆ 𝐴)) → (∃𝑦 ∈ ω (𝑧 “ 𝐵) ≈ 𝑦 → 𝐵 ∈ Fin)) |
| 30 | 12, 29 | mpd 15 |
. . . . . . 7
⊢ ((𝑥 ∈ ω ∧ (𝑧:𝐴–1-1-onto→𝑥 ∧ 𝐵 ⊆ 𝐴)) → 𝐵 ∈ Fin) |
| 31 | 30 | exp32 420 |
. . . . . 6
⊢ (𝑥 ∈ ω → (𝑧:𝐴–1-1-onto→𝑥 → (𝐵 ⊆ 𝐴 → 𝐵 ∈ Fin))) |
| 32 | 31 | exlimdv 1933 |
. . . . 5
⊢ (𝑥 ∈ ω →
(∃𝑧 𝑧:𝐴–1-1-onto→𝑥 → (𝐵 ⊆ 𝐴 → 𝐵 ∈ Fin))) |
| 33 | 2, 32 | biimtrid 242 |
. . . 4
⊢ (𝑥 ∈ ω → (𝐴 ≈ 𝑥 → (𝐵 ⊆ 𝐴 → 𝐵 ∈ Fin))) |
| 34 | 33 | rexlimiv 3148 |
. . 3
⊢
(∃𝑥 ∈
ω 𝐴 ≈ 𝑥 → (𝐵 ⊆ 𝐴 → 𝐵 ∈ Fin)) |
| 35 | 1, 34 | sylbi 217 |
. 2
⊢ (𝐴 ∈ Fin → (𝐵 ⊆ 𝐴 → 𝐵 ∈ Fin)) |
| 36 | 35 | imp 406 |
1
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ Fin) |