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 )