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	⊢ ( 𝐴 ∈ Fin → ( 𝐴 ∩ 𝐵 ) ∈ Fin )

Proof

Step	Hyp	Ref	Expression
1		inss1	⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴
2		ssfi	⊢ ( ( 𝐴 ∈ Fin ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴 ) → ( 𝐴 ∩ 𝐵 ) ∈ Fin )
3	1 2	mpan2	⊢ ( 𝐴 ∈ Fin → ( 𝐴 ∩ 𝐵 ) ∈ Fin )