Theorem snfi

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

	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		snprc	⊢ ( ¬ 𝐴 ∈ V ↔ { 𝐴 } = ∅ )
7		en0	⊢ ( { 𝐴 } ≈ ∅ ↔ { 𝐴 } = ∅ )
8		peano1	⊢ ∅ ∈ ω
9		breq2	⊢ ( 𝑥 = ∅ → ( { 𝐴 } ≈ 𝑥 ↔ { 𝐴 } ≈ ∅ ) )
10	9	rspcev	⊢ ( ( ∅ ∈ ω ∧ { 𝐴 } ≈ ∅ ) → ∃ 𝑥 ∈ ω { 𝐴 } ≈ 𝑥 )
11	8 10	mpan	⊢ ( { 𝐴 } ≈ ∅ → ∃ 𝑥 ∈ ω { 𝐴 } ≈ 𝑥 )
12	7 11	sylbir	⊢ ( { 𝐴 } = ∅ → ∃ 𝑥 ∈ ω { 𝐴 } ≈ 𝑥 )
13	6 12	sylbi	⊢ ( ¬ 𝐴 ∈ V → ∃ 𝑥 ∈ ω { 𝐴 } ≈ 𝑥 )
14	5 13	pm2.61i	⊢ ∃ 𝑥 ∈ ω { 𝐴 } ≈ 𝑥
15		isfi	⊢ ( { 𝐴 } ∈ Fin ↔ ∃ 𝑥 ∈ ω { 𝐴 } ≈ 𝑥 )
16	14 15	mpbir	⊢ { 𝐴 } ∈ Fin