Metamath Proof Explorer

Theorem djunum

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

Ref Expression
Assertion djunum ⊢A∈dom⁡card∧B∈dom⁡card→A⊔︀B∈dom⁡card

Proof

Step Hyp Ref Expression
1 cardon ⊢card⁡A∈On
2 cardon ⊢card⁡B∈On
3 oacl ⊢card⁡A∈On∧card⁡B∈On→card⁡A+𝑜card⁡B∈On
4 1 2 3 mp2an ⊢card⁡A+𝑜card⁡B∈On
5 cardadju ⊢A∈dom⁡card∧B∈dom⁡card→A⊔︀B≈card⁡A+𝑜card⁡B
6 5 ensymd ⊢A∈dom⁡card∧B∈dom⁡card→card⁡A+𝑜card⁡B≈A⊔︀B
7 isnumi ⊢card⁡A+𝑜card⁡B∈On∧card⁡A+𝑜card⁡B≈A⊔︀B→A⊔︀B∈dom⁡card
8 4 6 7 sylancr ⊢A∈dom⁡card∧B∈dom⁡card→A⊔︀B∈dom⁡card