Metamath Proof Explorer

Theorem cardadju

Description: The cardinal sum is equinumerous to an ordinal sum of the cardinals. (Contributed by Mario Carneiro, 6-Feb-2013) (Revised by Mario Carneiro, 28-Apr-2015)

Ref Expression
Assertion cardadju ⊢ A ∈ dom ⁡ card ∧ B ∈ dom ⁡ card → A ⊔︀ B ≈ card ⁡ A + 𝑜 card ⁡ B

Proof

Step Hyp Ref Expression
1 cardon ⊢ card ⁡ A ∈ On
2 cardon ⊢ card ⁡ B ∈ On
3 onadju ⊢ card ⁡ A ∈ On ∧ card ⁡ B ∈ On → card ⁡ A + 𝑜 card ⁡ B ≈ card ⁡ A ⊔︀ card ⁡ B
4 1 2 3 mp2an ⊢ card ⁡ A + 𝑜 card ⁡ B ≈ card ⁡ A ⊔︀ card ⁡ B
5 cardid2 ⊢ A ∈ dom ⁡ card → card ⁡ A ≈ A
6 cardid2 ⊢ B ∈ dom ⁡ card → card ⁡ B ≈ B
7 djuen ⊢ card ⁡ A ≈ A ∧ card ⁡ B ≈ B → card ⁡ A ⊔︀ card ⁡ B ≈ A ⊔︀ B
8 5 6 7 syl2an ⊢ A ∈ dom ⁡ card ∧ B ∈ dom ⁡ card → card ⁡ A ⊔︀ card ⁡ B ≈ A ⊔︀ B
9 entr ⊢ card ⁡ A + 𝑜 card ⁡ B ≈ card ⁡ A ⊔︀ card ⁡ B ∧ card ⁡ A ⊔︀ card ⁡ B ≈ A ⊔︀ B → card ⁡ A + 𝑜 card ⁡ B ≈ A ⊔︀ B
10 4 8 9 sylancr ⊢ A ∈ dom ⁡ card ∧ B ∈ dom ⁡ card → card ⁡ A + 𝑜 card ⁡ B ≈ A ⊔︀ B
11 10 ensymd ⊢ A ∈ dom ⁡ card ∧ B ∈ dom ⁡ card → A ⊔︀ B ≈ card ⁡ A + 𝑜 card ⁡ B