Theorem snfi

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

	Ref	Expression
Assertion	snfi	|- { A } e. Fin

Proof

Step	Hyp	Ref	Expression
1		1onn	|- 1o e. _om
2		ensn1g	|- ( A e. _V -> { A } ~~ 1o )
3		breq2	|- ( x = 1o -> ( { A } ~~ x <-> { A } ~~ 1o ) )
4	3	rspcev	|- ( ( 1o e. _om /\ { A } ~~ 1o ) -> E. x e. _om { A } ~~ x )
5	1 2 4	sylancr	|- ( A e. _V -> E. x e. _om { A } ~~ x )
6		snprc	|- ( -. A e. _V <-> { A } = (/) )
7		en0	|- ( { A } ~~ (/) <-> { A } = (/) )
8		peano1	|- (/) e. _om
9		breq2	|- ( x = (/) -> ( { A } ~~ x <-> { A } ~~ (/) ) )
10	9	rspcev	|- ( ( (/) e. _om /\ { A } ~~ (/) ) -> E. x e. _om { A } ~~ x )
11	8 10	mpan	|- ( { A } ~~ (/) -> E. x e. _om { A } ~~ x )
12	7 11	sylbir	|- ( { A } = (/) -> E. x e. _om { A } ~~ x )
13	6 12	sylbi	|- ( -. A e. _V -> E. x e. _om { A } ~~ x )
14	5 13	pm2.61i	|- E. x e. _om { A } ~~ x
15		isfi	|- ( { A } e. Fin <-> E. x e. _om { A } ~~ x )
16	14 15	mpbir	|- { A } e. Fin