snfi

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

		Ref	Expression
	Assertion	snfi	$⊢ \{A\} \in Fin$

Step	Hyp	Ref	Expression
1		1onn	$⊢ 1_{𝑜} \in ω$
2		ensn1g	$⊢ A \in V \to \{A\} \approx 1_{𝑜}$
3		breq2	$⊢ x = 1_{𝑜} \to (\{A\} \approx x \leftrightarrow \{A\} \approx 1_{𝑜})$
4	3	rspcev	$⊢ (1_{𝑜} \in ω \land \{A\} \approx 1_{𝑜}) \to \exists x \in ω \{A\} \approx x$
5	1 2 4	sylancr	$⊢ A \in V \to \exists x \in ω \{A\} \approx x$
6		isfi	$⊢ \{A\} \in Fin \leftrightarrow \exists x \in ω \{A\} \approx x$
7	5 6	sylibr	$⊢ A \in V \to \{A\} \in Fin$
8		snprc	$⊢ \neg A \in V \leftrightarrow \{A\} = \emptyset$
9		0fi	$⊢ \emptyset \in Fin$
10		eleq1	$⊢ \{A\} = \emptyset \to (\{A\} \in Fin \leftrightarrow \emptyset \in Fin)$
11	9 10	mpbiri	$⊢ \{A\} = \emptyset \to \{A\} \in Fin$
12	8 11	sylbi	$⊢ \neg A \in V \to \{A\} \in Fin$
13	7 12	pm2.61i	$⊢ \{A\} \in Fin$

Metamath Proof Explorer