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

Proof

Step Hyp Ref Expression
1 ssun1 ⊢ A ⊆ A ∪ B
2 ssfi ⊢ A ∪ B ∈ Fin ∧ A ⊆ A ∪ B → A ∈ Fin
3 1 2 mpan2 ⊢ A ∪ B ∈ Fin → A ∈ Fin
4 ssun2 ⊢ B ⊆ A ∪ B
5 ssfi ⊢ A ∪ B ∈ Fin ∧ B ⊆ A ∪ B → B ∈ Fin
6 4 5 mpan2 ⊢ A ∪ B ∈ Fin → B ∈ Fin
7 3 6 jca ⊢ A ∪ B ∈ Fin → A ∈ Fin ∧ B ∈ Fin