Metamath Proof Explorer

Theorem unctb

Description: The union of two countable sets is countable. (Contributed by FL, 25-Aug-2006) (Proof shortened by Mario Carneiro, 30-Apr-2015)

Ref Expression
Assertion unctb 
|- ( ( A ~<_ _om /\ B ~<_ _om ) -> ( A u. B ) ~<_ _om )

Proof

Step Hyp Ref Expression
1 ctex 
 |-  ( A ~<_ _om -> A e. _V )
2 ctex 
 |-  ( B ~<_ _om -> B e. _V )
3 undjudom 
 |-  ( ( A e. _V /\ B e. _V ) -> ( A u. B ) ~<_ ( A |_| B ) )
4 1 2 3 syl2an 
 |-  ( ( A ~<_ _om /\ B ~<_ _om ) -> ( A u. B ) ~<_ ( A |_| B ) )
5 djudom1 
 |-  ( ( A ~<_ _om /\ B e. _V ) -> ( A |_| B ) ~<_ ( _om |_| B ) )
6 2 5 sylan2 
 |-  ( ( A ~<_ _om /\ B ~<_ _om ) -> ( A |_| B ) ~<_ ( _om |_| B ) )
7 simpr 
 |-  ( ( A ~<_ _om /\ B ~<_ _om ) -> B ~<_ _om )
8 omex 
 |-  _om e. _V
9 djudom2 
 |-  ( ( B ~<_ _om /\ _om e. _V ) -> ( _om |_| B ) ~<_ ( _om |_| _om ) )
10 7 8 9 sylancl 
 |-  ( ( A ~<_ _om /\ B ~<_ _om ) -> ( _om |_| B ) ~<_ ( _om |_| _om ) )
11 domtr 
 |-  ( ( ( A |_| B ) ~<_ ( _om |_| B ) /\ ( _om |_| B ) ~<_ ( _om |_| _om ) ) -> ( A |_| B ) ~<_ ( _om |_| _om ) )
12 6 10 11 syl2anc 
 |-  ( ( A ~<_ _om /\ B ~<_ _om ) -> ( A |_| B ) ~<_ ( _om |_| _om ) )
13 8 8 xpex 
 |-  ( _om X. _om ) e. _V
14 xp2dju 
 |-  ( 2o X. _om ) = ( _om |_| _om )
15 ordom 
 |-  Ord _om
16 2onn 
 |-  2o e. _om
17 ordelss 
 |-  ( ( Ord _om /\ 2o e. _om ) -> 2o C_ _om )
18 15 16 17 mp2an 
 |-  2o C_ _om
19 xpss1 
 |-  ( 2o C_ _om -> ( 2o X. _om ) C_ ( _om X. _om ) )
20 18 19 ax-mp 
 |-  ( 2o X. _om ) C_ ( _om X. _om )
21 14 20 eqsstrri 
 |-  ( _om |_| _om ) C_ ( _om X. _om )
22 ssdomg 
 |-  ( ( _om X. _om ) e. _V -> ( ( _om |_| _om ) C_ ( _om X. _om ) -> ( _om |_| _om ) ~<_ ( _om X. _om ) ) )
23 13 21 22 mp2 
 |-  ( _om |_| _om ) ~<_ ( _om X. _om )
24 xpomen 
 |-  ( _om X. _om ) ~~ _om
25 domentr 
 |-  ( ( ( _om |_| _om ) ~<_ ( _om X. _om ) /\ ( _om X. _om ) ~~ _om ) -> ( _om |_| _om ) ~<_ _om )
26 23 24 25 mp2an 
 |-  ( _om |_| _om ) ~<_ _om
27 domtr 
 |-  ( ( ( A |_| B ) ~<_ ( _om |_| _om ) /\ ( _om |_| _om ) ~<_ _om ) -> ( A |_| B ) ~<_ _om )
28 12 26 27 sylancl 
 |-  ( ( A ~<_ _om /\ B ~<_ _om ) -> ( A |_| B ) ~<_ _om )
29 domtr 
 |-  ( ( ( A u. B ) ~<_ ( A |_| B ) /\ ( A |_| B ) ~<_ _om ) -> ( A u. B ) ~<_ _om )
30 4 28 29 syl2anc 
 |-  ( ( A ~<_ _om /\ B ~<_ _om ) -> ( A u. B ) ~<_ _om )