Metamath Proof Explorer

Theorem unnum

Description: The union of two numerable sets is numerable. (Contributed by Mario Carneiro, 29-Apr-2015)

Ref Expression
Assertion unnum ⊢ A ∈ dom ⁡ card ∧ B ∈ dom ⁡ card → A ∪ B ∈ dom ⁡ card

Proof

Step Hyp Ref Expression
1 djunum ⊢ A ∈ dom ⁡ card ∧ B ∈ dom ⁡ card → A ⊔︀ B ∈ dom ⁡ card
2 undjudom ⊢ A ∈ dom ⁡ card ∧ B ∈ dom ⁡ card → A ∪ B ≼ A ⊔︀ B
3 numdom ⊢ A ⊔︀ B ∈ dom ⁡ card ∧ A ∪ B ≼ A ⊔︀ B → A ∪ B ∈ dom ⁡ card
4 1 2 3 syl2anc ⊢ A ∈ dom ⁡ card ∧ B ∈ dom ⁡ card → A ∪ B ∈ dom ⁡ card