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	⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ) → ( 𝐴 ⊔ 𝐵 ) ≈ ( ( card ‘ 𝐴 ) +o ( card ‘ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		cardon	⊢ ( card ‘ 𝐴 ) ∈ On
2		cardon	⊢ ( card ‘ 𝐵 ) ∈ On
3		onadju	⊢ ( ( ( card ‘ 𝐴 ) ∈ On ∧ ( card ‘ 𝐵 ) ∈ On ) → ( ( card ‘ 𝐴 ) +o ( card ‘ 𝐵 ) ) ≈ ( ( card ‘ 𝐴 ) ⊔ ( card ‘ 𝐵 ) ) )
4	1 2 3	mp2an	⊢ ( ( card ‘ 𝐴 ) +o ( card ‘ 𝐵 ) ) ≈ ( ( card ‘ 𝐴 ) ⊔ ( card ‘ 𝐵 ) )
5		cardid2	⊢ ( 𝐴 ∈ dom card → ( card ‘ 𝐴 ) ≈ 𝐴 )
6		cardid2	⊢ ( 𝐵 ∈ dom card → ( card ‘ 𝐵 ) ≈ 𝐵 )
7		djuen	⊢ ( ( ( card ‘ 𝐴 ) ≈ 𝐴 ∧ ( card ‘ 𝐵 ) ≈ 𝐵 ) → ( ( card ‘ 𝐴 ) ⊔ ( card ‘ 𝐵 ) ) ≈ ( 𝐴 ⊔ 𝐵 ) )
8	5 6 7	syl2an	⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ) → ( ( card ‘ 𝐴 ) ⊔ ( card ‘ 𝐵 ) ) ≈ ( 𝐴 ⊔ 𝐵 ) )
9		entr	⊢ ( ( ( ( card ‘ 𝐴 ) +o ( card ‘ 𝐵 ) ) ≈ ( ( card ‘ 𝐴 ) ⊔ ( card ‘ 𝐵 ) ) ∧ ( ( card ‘ 𝐴 ) ⊔ ( card ‘ 𝐵 ) ) ≈ ( 𝐴 ⊔ 𝐵 ) ) → ( ( card ‘ 𝐴 ) +o ( card ‘ 𝐵 ) ) ≈ ( 𝐴 ⊔ 𝐵 ) )
10	4 8 9	sylancr	⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ) → ( ( card ‘ 𝐴 ) +o ( card ‘ 𝐵 ) ) ≈ ( 𝐴 ⊔ 𝐵 ) )
11	10	ensymd	⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ) → ( 𝐴 ⊔ 𝐵 ) ≈ ( ( card ‘ 𝐴 ) +o ( card ‘ 𝐵 ) ) )