Metamath Proof Explorer

Theorem unfib

Description: A union is finite if and only if the operands are finite. (Contributed by AV, 10-May-2025)

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

Proof

Step Hyp Ref Expression
1 unfir 
 |-  ( ( A u. B ) e. Fin -> ( A e. Fin /\ B e. Fin ) )
2 unfi 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( A u. B ) e. Fin )
3 1 2 impbii 
 |-  ( ( A u. B ) e. Fin <-> ( A e. Fin /\ B e. Fin ) )