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