Theorem domfin4

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

	Ref	Expression
Assertion	domfin4	$$⊢\left(A\in {\mathrm{Fin}}^{\mathrm{IV}}\wedge B\preccurlyeq A\right)\to B\in {\mathrm{Fin}}^{\mathrm{IV}}$$

Proof

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