Metamath Proof Explorer

Theorem unfir

Description: If a union is finite, the operands are finite. Converse of unfi . (Contributed by FL, 3-Aug-2009)

Ref Expression
Assertion unfir 
|- ( ( A u. B ) e. Fin -> ( A e. Fin /\ B e. Fin ) )

Proof

Step Hyp Ref Expression
1 ssun1 
 |-  A C_ ( A u. B )
2 ssfi 
 |-  ( ( ( A u. B ) e. Fin /\ A C_ ( A u. B ) ) -> A e. Fin )
3 1 2 mpan2 
 |-  ( ( A u. B ) e. Fin -> A e. Fin )
4 ssun2 
 |-  B C_ ( A u. B )
5 ssfi 
 |-  ( ( ( A u. B ) e. Fin /\ B C_ ( A u. B ) ) -> B e. Fin )
6 4 5 mpan2 
 |-  ( ( A u. B ) e. Fin -> B e. Fin )
7 3 6 jca 
 |-  ( ( A u. B ) e. Fin -> ( A e. Fin /\ B e. Fin ) )