domfi

Description: A set dominated by a finite set is finite. (Contributed by NM, 23-Mar-2006) (Revised by Mario Carneiro, 12-Mar-2015)

		Ref	Expression
	Assertion	domfi	$⊢ (A \in Fin \land B ≼ A) \to B \in Fin$

Step	Hyp	Ref	Expression
1		domeng	$⊢ A \in Fin \to (B ≼ A \leftrightarrow \exists x (B \approx x \land x \subseteq A))$
2		ssfi	$⊢ (A \in Fin \land x \subseteq A) \to x \in Fin$
3	2	adantrl	$⊢ (A \in Fin \land (B \approx x \land x \subseteq A)) \to x \in Fin$
4		enfii	$⊢ (x \in Fin \land B \approx x) \to B \in Fin$
5	4	adantrr	$⊢ (x \in Fin \land (B \approx x \land x \subseteq A)) \to B \in Fin$
6	3 5	sylancom	$⊢ (A \in Fin \land (B \approx x \land x \subseteq A)) \to B \in Fin$
7	6	ex	$⊢ A \in Fin \to ((B \approx x \land x \subseteq A) \to B \in Fin)$
8	7	exlimdv	$⊢ A \in Fin \to (\exists x (B \approx x \land x \subseteq A) \to B \in Fin)$
9	1 8	sylbid	$⊢ A \in Fin \to (B ≼ A \to B \in Fin)$
10	9	imp	$⊢ (A \in Fin \land B ≼ A) \to B \in Fin$

Metamath Proof Explorer