This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐴 ∈ 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 ‘ 𝐵 ) ) )