Step | Hyp | Ref
| Expression |
1 | | 1onn 8662 |
. . . 4
⊢
1o ∈ ω |
2 | | ensn1g 9047 |
. . . 4
⊢ (𝐴 ∈ V → {𝐴} ≈
1o) |
3 | | breq2 5149 |
. . . . 5
⊢ (𝑥 = 1o → ({𝐴} ≈ 𝑥 ↔ {𝐴} ≈ 1o)) |
4 | 3 | rspcev 3607 |
. . . 4
⊢
((1o ∈ ω ∧ {𝐴} ≈ 1o) → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥) |
5 | 1, 2, 4 | sylancr 585 |
. . 3
⊢ (𝐴 ∈ V → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥) |
6 | | isfi 8999 |
. . 3
⊢ ({𝐴} ∈ Fin ↔ ∃𝑥 ∈ ω {𝐴} ≈ 𝑥) |
7 | 5, 6 | sylibr 233 |
. 2
⊢ (𝐴 ∈ V → {𝐴} ∈ Fin) |
8 | | snprc 4716 |
. . 3
⊢ (¬
𝐴 ∈ V ↔ {𝐴} = ∅) |
9 | | 0fi 9072 |
. . . 4
⊢ ∅
∈ Fin |
10 | | eleq1 2814 |
. . . 4
⊢ ({𝐴} = ∅ → ({𝐴} ∈ Fin ↔ ∅
∈ Fin)) |
11 | 9, 10 | mpbiri 257 |
. . 3
⊢ ({𝐴} = ∅ → {𝐴} ∈ Fin) |
12 | 8, 11 | sylbi 216 |
. 2
⊢ (¬
𝐴 ∈ V → {𝐴} ∈ Fin) |
13 | 7, 12 | pm2.61i 182 |
1
⊢ {𝐴} ∈ Fin |