domfin4

Description: A set dominated by a Dedekind finite set is Dedekind finite. (Contributed by Mario Carneiro, 16-May-2015)

		Ref	Expression
	Assertion	domfin4	$⊢ (A \in {Fin}^{IV} \land B ≼ A) \to B \in {Fin}^{IV}$

Step	Hyp	Ref	Expression
1		domeng	$⊢ A \in {Fin}^{IV} \to (B ≼ A \leftrightarrow \exists x (B \approx x \land x \subseteq A))$
2	1	biimpa	$⊢ (A \in {Fin}^{IV} \land B ≼ A) \to \exists x (B \approx x \land x \subseteq A)$
3		ensym	$⊢ B \approx x \to x \approx B$
4	3	ad2antrl	$⊢ ((A \in {Fin}^{IV} \land B ≼ A) \land (B \approx x \land x \subseteq A)) \to x \approx B$
5		ssfin4	$⊢ (A \in {Fin}^{IV} \land x \subseteq A) \to x \in {Fin}^{IV}$
6	5	ad2ant2rl	$⊢ ((A \in {Fin}^{IV} \land B ≼ A) \land (B \approx x \land x \subseteq A)) \to x \in {Fin}^{IV}$
7		fin4en1	$⊢ x \approx B \to (x \in {Fin}^{IV} \to B \in {Fin}^{IV})$
8	4 6 7	sylc	$⊢ ((A \in {Fin}^{IV} \land B ≼ A) \land (B \approx x \land x \subseteq A)) \to B \in {Fin}^{IV}$
9	2 8	exlimddv	$⊢ (A \in {Fin}^{IV} \land B ≼ A) \to B \in {Fin}^{IV}$

Metamath Proof Explorer