ssfi

Description: A subset of a finite set is finite. Corollary 6G of Enderton p. 138. (Contributed by NM, 24-Jun-1998)

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

Proof

Step	Hyp	Ref	Expression
1		isfi	$⊢ A \in Fin \leftrightarrow \exists x \in ω A \approx x$
2		bren	$⊢ A \approx x \leftrightarrow \exists z z : A \underset{1-1 onto}{⟶} x$
3		f1ofo	$⊢ z : A \underset{1-1 onto}{⟶} x \to z : A \underset{onto}{⟶} x$
4		imassrn	$⊢ z [B] \subseteq ran z$
5		forn	$⊢ z : A \underset{onto}{⟶} x \to ran z = x$
6	4 5	sseqtrid	$⊢ z : A \underset{onto}{⟶} x \to z [B] \subseteq x$
7	3 6	syl	$⊢ z : A \underset{1-1 onto}{⟶} x \to z [B] \subseteq x$
8		ssnnfi	$⊢ (x \in ω \land z [B] \subseteq x) \to z [B] \in Fin$
9		isfi	$⊢ z [B] \in Fin \leftrightarrow \exists y \in ω z [B] \approx y$
10	8 9	sylib	$⊢ (x \in ω \land z [B] \subseteq x) \to \exists y \in ω z [B] \approx y$
11	7 10	sylan2	$⊢ (x \in ω \land z : A \underset{1-1 onto}{⟶} x) \to \exists y \in ω z [B] \approx y$
12	11	adantrr	$⊢ (x \in ω \land (z : A \underset{1-1 onto}{⟶} x \land B \subseteq A)) \to \exists y \in ω z [B] \approx y$
13		f1of1	$⊢ z : A \underset{1-1 onto}{⟶} x \to z : A \underset{1-1}{⟶} x$
14		f1ores	$⊢ (z : A \underset{1-1}{⟶} x \land B \subseteq A) \to ({z ↾}_{B}) : B \underset{1-1 onto}{⟶} z [B]$
15	13 14	sylan	$⊢ (z : A \underset{1-1 onto}{⟶} x \land B \subseteq A) \to ({z ↾}_{B}) : B \underset{1-1 onto}{⟶} z [B]$
16		vex	$⊢ z \in V$
17	16	resex	$⊢ {z ↾}_{B} \in V$
18		f1oeq1	$⊢ x = {z ↾}_{B} \to (x : B \underset{1-1 onto}{⟶} z [B] \leftrightarrow ({z ↾}_{B}) : B \underset{1-1 onto}{⟶} z [B])$
19	17 18	spcev	$⊢ ({z ↾}_{B}) : B \underset{1-1 onto}{⟶} z [B] \to \exists x x : B \underset{1-1 onto}{⟶} z [B]$
20		bren	$⊢ B \approx z [B] \leftrightarrow \exists x x : B \underset{1-1 onto}{⟶} z [B]$
21	19 20	sylibr	$⊢ ({z ↾}_{B}) : B \underset{1-1 onto}{⟶} z [B] \to B \approx z [B]$
22		entr	$⊢ (B \approx z [B] \land z [B] \approx y) \to B \approx y$
23	21 22	sylan	$⊢ (({z ↾}_{B}) : B \underset{1-1 onto}{⟶} z [B] \land z [B] \approx y) \to B \approx y$
24	15 23	sylan	$⊢ ((z : A \underset{1-1 onto}{⟶} x \land B \subseteq A) \land z [B] \approx y) \to B \approx y$
25	24	ex	$⊢ (z : A \underset{1-1 onto}{⟶} x \land B \subseteq A) \to (z [B] \approx y \to B \approx y)$
26	25	reximdv	$⊢ (z : A \underset{1-1 onto}{⟶} x \land B \subseteq A) \to (\exists y \in ω z [B] \approx y \to \exists y \in ω B \approx y)$
27		isfi	$⊢ B \in Fin \leftrightarrow \exists y \in ω B \approx y$
28	26 27	syl6ibr	$⊢ (z : A \underset{1-1 onto}{⟶} x \land B \subseteq A) \to (\exists y \in ω z [B] \approx y \to B \in Fin)$
29	28	adantl	$⊢ (x \in ω \land (z : A \underset{1-1 onto}{⟶} x \land B \subseteq A)) \to (\exists y \in ω z [B] \approx y \to B \in Fin)$
30	12 29	mpd	$⊢ (x \in ω \land (z : A \underset{1-1 onto}{⟶} x \land B \subseteq A)) \to B \in Fin$
31	30	exp32	$⊢ x \in ω \to (z : A \underset{1-1 onto}{⟶} x \to (B \subseteq A \to B \in Fin))$
32	31	exlimdv	$⊢ x \in ω \to (\exists z z : A \underset{1-1 onto}{⟶} x \to (B \subseteq A \to B \in Fin))$
33	2 32	syl5bi	$⊢ x \in ω \to (A \approx x \to (B \subseteq A \to B \in Fin))$
34	33	rexlimiv	$⊢ \exists x \in ω A \approx x \to (B \subseteq A \to B \in Fin)$
35	1 34	sylbi	$⊢ A \in Fin \to (B \subseteq A \to B \in Fin)$
36	35	imp	$⊢ (A \in Fin \land B \subseteq A) \to B \in Fin$

Metamath Proof Explorer

Theorem ssfi

Proof