Metamath Proof Explorer

Theorem snfi

Description: A singleton is finite. (Contributed by NM, 4-Nov-2002)

Ref Expression
Assertion snfi ⊢ A ∈ Fin

Proof

Step Hyp Ref Expression
1 1onn ⊢ 1 𝑜 ∈ ω
2 ensn1g ⊢ A ∈ V → A ≈ 1 𝑜
3 breq2 ⊢ x = 1 𝑜 → A ≈ x ↔ A ≈ 1 𝑜
4 3 rspcev ⊢ 1 𝑜 ∈ ω ∧ A ≈ 1 𝑜 → ∃ x ∈ ω A ≈ x
5 1 2 4 sylancr ⊢ A ∈ V → ∃ x ∈ ω A ≈ x
6 snprc ⊢ ¬ A ∈ V ↔ A = ∅
7 en0 ⊢ A ≈ ∅ ↔ A = ∅
8 peano1 ⊢ ∅ ∈ ω
9 breq2 ⊢ x = ∅ → A ≈ x ↔ A ≈ ∅
10 9 rspcev ⊢ ∅ ∈ ω ∧ A ≈ ∅ → ∃ x ∈ ω A ≈ x
11 8 10 mpan ⊢ A ≈ ∅ → ∃ x ∈ ω A ≈ x
12 7 11 sylbir ⊢ A = ∅ → ∃ x ∈ ω A ≈ x
13 6 12 sylbi ⊢ ¬ A ∈ V → ∃ x ∈ ω A ≈ x
14 5 13 pm2.61i ⊢ ∃ x ∈ ω A ≈ x
15 isfi ⊢ A ∈ Fin ↔ ∃ x ∈ ω A ≈ x
16 14 15 mpbir ⊢ A ∈ Fin