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 
|- ( A e. Fin -> ( A i^i B ) e. Fin )

Proof

Step Hyp Ref Expression
1 inss1 
 |-  ( A i^i B ) C_ A
2 ssfi 
 |-  ( ( A e. Fin /\ ( A i^i B ) C_ A ) -> ( A i^i B ) e. Fin )
3 1 2 mpan2 
 |-  ( A e. Fin -> ( A i^i B ) e. Fin )