Metamath Proof Explorer


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 )