ssnnfi

Description: A subset of a natural number is finite. (Contributed by NM, 24-Jun-1998) (Proof shortened by BTernaryTau, 23-Sep-2024)

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

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		isfi	$⊢ B \in Fin \leftrightarrow \exists x \in ω B \approx x$
10	8 9	sylibr	$⊢ (A \in ω \land B \subset A) \to B \in Fin$
11		eleq1	$⊢ B = A \to (B \in ω \leftrightarrow A \in ω)$
12	11	biimparc	$⊢ (A \in ω \land B = A) \to B \in ω$
13		nnfi	$⊢ B \in ω \to B \in Fin$
14	12 13	syl	$⊢ (A \in ω \land B = A) \to B \in Fin$
15	10 14	jaodan	$⊢ (A \in ω \land (B \subset A \lor B = A)) \to B \in Fin$
16	1 15	sylan2b	$⊢ (A \in ω \land B \subseteq A) \to B \in Fin$

Metamath Proof Explorer