Step | Hyp | Ref
| Expression |
1 | | 1onn 7606 |
. . . 4
⊢
1𝑜 ∈ ω |
2 | | ensn1g 7907 |
. . . 4
⊢ (𝐴 ∈ V → {𝐴} ≈
1𝑜) |
3 | | breq2 4587 |
. . . . 5
⊢ (𝑥 = 1𝑜 →
({𝐴} ≈ 𝑥 ↔ {𝐴} ≈
1𝑜)) |
4 | 3 | rspcev 3282 |
. . . 4
⊢
((1𝑜 ∈ ω ∧ {𝐴} ≈ 1𝑜) →
∃𝑥 ∈ ω
{𝐴} ≈ 𝑥) |
5 | 1, 2, 4 | sylancr 694 |
. . 3
⊢ (𝐴 ∈ V → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥) |
6 | | snprc 4197 |
. . . 4
⊢ (¬
𝐴 ∈ V ↔ {𝐴} = ∅) |
7 | | en0 7905 |
. . . . 5
⊢ ({𝐴} ≈ ∅ ↔ {𝐴} = ∅) |
8 | | peano1 6977 |
. . . . . 6
⊢ ∅
∈ ω |
9 | | breq2 4587 |
. . . . . . 7
⊢ (𝑥 = ∅ → ({𝐴} ≈ 𝑥 ↔ {𝐴} ≈ ∅)) |
10 | 9 | rspcev 3282 |
. . . . . 6
⊢ ((∅
∈ ω ∧ {𝐴}
≈ ∅) → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥) |
11 | 8, 10 | mpan 702 |
. . . . 5
⊢ ({𝐴} ≈ ∅ →
∃𝑥 ∈ ω
{𝐴} ≈ 𝑥) |
12 | 7, 11 | sylbir 224 |
. . . 4
⊢ ({𝐴} = ∅ → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥) |
13 | 6, 12 | sylbi 206 |
. . 3
⊢ (¬
𝐴 ∈ V →
∃𝑥 ∈ ω
{𝐴} ≈ 𝑥) |
14 | 5, 13 | pm2.61i 175 |
. 2
⊢
∃𝑥 ∈
ω {𝐴} ≈ 𝑥 |
15 | | isfi 7865 |
. 2
⊢ ({𝐴} ∈ Fin ↔ ∃𝑥 ∈ ω {𝐴} ≈ 𝑥) |
16 | 14, 15 | mpbir 220 |
1
⊢ {𝐴} ∈ Fin |