Theorem infi

Description: The intersection of two sets is finite if one of them is. (Contributed by Thierry Arnoux, 14-Feb-2017)

	Ref	Expression
Assertion	infi	$$⊢A\in \mathrm{Fin}\to A\cap B\in \mathrm{Fin}$$

Proof

Step	Hyp	Ref	Expression
1		inss1	$$⊢A\cap B\subseteq A$$
2		ssfi	$$⊢\left(A\in \mathrm{Fin}\wedge A\cap B\subseteq A\right)\to A\cap B\in \mathrm{Fin}$$
3	1 2	mpan2	$$⊢A\in \mathrm{Fin}\to A\cap B\in \mathrm{Fin}$$