Theorem snfi

Description: A singleton is finite. (Contributed by NM, 4-Nov-2002) (Proof shortened by BTernaryTau, 13-Jan-2025)

	Ref	Expression
Assertion	snfi	⊢ { 𝐴 } ∈ Fin

Proof

Step	Hyp	Ref	Expression
1		1onn	⊢ 1o ∈ ω
2		ensn1g	⊢ ( 𝐴 ∈ V → { 𝐴 } ≈ 1o )
3		breq2	⊢ ( 𝑥 = 1o → ( { 𝐴 } ≈ 𝑥 ↔ { 𝐴 } ≈ 1o ) )
4	3	rspcev	⊢ ( ( 1o ∈ ω ∧ { 𝐴 } ≈ 1o ) → ∃ 𝑥 ∈ ω { 𝐴 } ≈ 𝑥 )
5	1 2 4	sylancr	⊢ ( 𝐴 ∈ V → ∃ 𝑥 ∈ ω { 𝐴 } ≈ 𝑥 )
6		isfi	⊢ ( { 𝐴 } ∈ Fin ↔ ∃ 𝑥 ∈ ω { 𝐴 } ≈ 𝑥 )
7	5 6	sylibr	⊢ ( 𝐴 ∈ V → { 𝐴 } ∈ Fin )
8		snprc	⊢ ( ¬ 𝐴 ∈ V ↔ { 𝐴 } = ∅ )
9		0fi	⊢ ∅ ∈ Fin
10		eleq1	⊢ ( { 𝐴 } = ∅ → ( { 𝐴 } ∈ Fin ↔ ∅ ∈ Fin ) )
11	9 10	mpbiri	⊢ ( { 𝐴 } = ∅ → { 𝐴 } ∈ Fin )
12	8 11	sylbi	⊢ ( ¬ 𝐴 ∈ V → { 𝐴 } ∈ Fin )
13	7 12	pm2.61i	⊢ { 𝐴 } ∈ Fin