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 e. dom card /\ B e. dom card ) -> ( A |_| B ) ~~ ( ( card ` A ) +o ( card ` B ) ) )

Proof

Step Hyp Ref Expression
1 cardon 
 |-  ( card ` A ) e. On
2 cardon 
 |-  ( card ` B ) e. On
3 onadju 
 |-  ( ( ( card ` A ) e. On /\ ( card ` B ) e. On ) -> ( ( card ` A ) +o ( card ` B ) ) ~~ ( ( card ` A ) |_| ( card ` B ) ) )
4 1 2 3 mp2an 
 |-  ( ( card ` A ) +o ( card ` B ) ) ~~ ( ( card ` A ) |_| ( card ` B ) )
5 cardid2 
 |-  ( A e. dom card -> ( card ` A ) ~~ A )
6 cardid2 
 |-  ( B e. 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 e. dom card /\ B e. dom card ) -> ( ( card ` A ) |_| ( card ` B ) ) ~~ ( A |_| B ) )
9 entr 
 |-  ( ( ( ( card ` A ) +o ( card ` B ) ) ~~ ( ( card ` A ) |_| ( card ` B ) ) /\ ( ( card ` A ) |_| ( card ` B ) ) ~~ ( A |_| B ) ) -> ( ( card ` A ) +o ( card ` B ) ) ~~ ( A |_| B ) )
10 4 8 9 sylancr 
 |-  ( ( A e. dom card /\ B e. dom card ) -> ( ( card ` A ) +o ( card ` B ) ) ~~ ( A |_| B ) )
11 10 ensymd 
 |-  ( ( A e. dom card /\ B e. dom card ) -> ( A |_| B ) ~~ ( ( card ` A ) +o ( card ` B ) ) )