Metamath Proof Explorer

Theorem snfiOLD

Description: Obsolete version of snfi as of 13-Jan-2025. (Contributed by NM, 4-Nov-2002) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

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		snprc	$⊢ \neg A \in V \leftrightarrow \{A\} = \emptyset$
7		en0	$⊢ \{A\} \approx \emptyset \leftrightarrow \{A\} = \emptyset$
8		peano1	$⊢ \emptyset \in ω$
9		breq2	$⊢ x = \emptyset \to (\{A\} \approx x \leftrightarrow \{A\} \approx \emptyset)$
10	9	rspcev	$⊢ (\emptyset \in ω \land \{A\} \approx \emptyset) \to \exists x \in ω \{A\} \approx x$
11	8 10	mpan	$⊢ \{A\} \approx \emptyset \to \exists x \in ω \{A\} \approx x$
12	7 11	sylbir	$⊢ \{A\} = \emptyset \to \exists x \in ω \{A\} \approx x$
13	6 12	sylbi	$⊢ \neg A \in V \to \exists x \in ω \{A\} \approx x$
14	5 13	pm2.61i	$⊢ \exists x \in ω \{A\} \approx x$
15		isfi	$⊢ \{A\} \in Fin \leftrightarrow \exists x \in ω \{A\} \approx x$
16	14 15	mpbir	$⊢ \{A\} \in Fin$