Metamath Proof Explorer

Theorem ssnnfiOLD

Description: Obsolete version of ssnnfi as of 23-Sep-2024. (Contributed by NM, 24-Jun-1998) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	ssnnfiOLD	$⊢ (A \in ω \land B \subseteq A) \to B \in Fin$

Proof

Step	Hyp	Ref	Expression
1		sspss	$⊢ B \subseteq A \leftrightarrow (B \subset A \lor B = A)$
2		pssnn	$⊢ (A \in ω \land B \subset A) \to \exists x \in A B \approx x$
3		elnn	$⊢ (x \in A \land A \in ω) \to x \in ω$
4	3	expcom	$⊢ A \in ω \to (x \in A \to x \in ω)$
5	4	anim1d	$⊢ A \in ω \to ((x \in A \land B \approx x) \to (x \in ω \land B \approx x))$
6	5	reximdv2	$⊢ A \in ω \to (\exists x \in A B \approx x \to \exists x \in ω B \approx x)$
7	6	adantr	$⊢ (A \in ω \land B \subset A) \to (\exists x \in A B \approx x \to \exists x \in ω B \approx x)$
8	2 7	mpd	$⊢ (A \in ω \land B \subset A) \to \exists x \in ω B \approx x$
9		eleq1	$⊢ B = A \to (B \in ω \leftrightarrow A \in ω)$
10	9	biimparc	$⊢ (A \in ω \land B = A) \to B \in ω$
11		enrefnn	$⊢ B \in ω \to B \approx B$
12		breq2	$⊢ x = B \to (B \approx x \leftrightarrow B \approx B)$
13	12	rspcev	$⊢ (B \in ω \land B \approx B) \to \exists x \in ω B \approx x$
14	10 11 13	syl2anc2	$⊢ (A \in ω \land B = A) \to \exists x \in ω B \approx x$
15	8 14	jaodan	$⊢ (A \in ω \land (B \subset A \lor B = A)) \to \exists x \in ω B \approx x$
16	1 15	sylan2b	$⊢ (A \in ω \land B \subseteq A) \to \exists x \in ω B \approx x$
17		isfi	$⊢ B \in Fin \leftrightarrow \exists x \in ω B \approx x$
18	16 17	sylibr	$⊢ (A \in ω \land B \subseteq A) \to B \in Fin$