Metamath Proof Explorer

Theorem djunum

Description: The disjoint union of two numerable sets is numerable. (Contributed by Mario Carneiro, 29-Apr-2015)

Ref Expression
Assertion djunum 
|- ( ( A e. dom card /\ B e. dom card ) -> ( A |_| B ) e. dom card )

Proof

Step Hyp Ref Expression
1 cardon 
 |-  ( card ` A ) e. On
2 cardon 
 |-  ( card ` B ) e. On
3 oacl 
 |-  ( ( ( card ` A ) e. On /\ ( card ` B ) e. On ) -> ( ( card ` A ) +o ( card ` B ) ) e. On )
4 1 2 3 mp2an 
 |-  ( ( card ` A ) +o ( card ` B ) ) e. On
5 cardadju 
 |-  ( ( A e. dom card /\ B e. dom card ) -> ( A |_| B ) ~~ ( ( card ` A ) +o ( card ` B ) ) )
6 5 ensymd 
 |-  ( ( A e. dom card /\ B e. dom card ) -> ( ( card ` A ) +o ( card ` B ) ) ~~ ( A |_| B ) )
7 isnumi 
 |-  ( ( ( ( card ` A ) +o ( card ` B ) ) e. On /\ ( ( card ` A ) +o ( card ` B ) ) ~~ ( A |_| B ) ) -> ( A |_| B ) e. dom card )
8 4 6 7 sylancr 
 |-  ( ( A e. dom card /\ B e. dom card ) -> ( A |_| B ) e. dom card )