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 ∪ B ∈ Fin ↔ A ∈ Fin ∧ B ∈ Fin

Proof

Step Hyp Ref Expression
1 unfir ⊢ A ∪ B ∈ Fin → A ∈ Fin ∧ B ∈ Fin
2 unfi ⊢ A ∈ Fin ∧ B ∈ Fin → A ∪ B ∈ Fin
3 1 2 impbii ⊢ A ∪ B ∈ Fin ↔ A ∈ Fin ∧ B ∈ Fin