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