Metamath Proof Explorer

Theorem xpct

Description: The cartesian product of two countable sets is countable. (Contributed by Thierry Arnoux, 24-Sep-2017)

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

Proof

Step Hyp Ref Expression
1 ctex 
 |-  ( B ~<_ _om -> B e. _V )
2 1 adantl 
 |-  ( ( A ~<_ _om /\ B ~<_ _om ) -> B e. _V )
3 simpl 
 |-  ( ( A ~<_ _om /\ B ~<_ _om ) -> A ~<_ _om )
4 xpdom1g 
 |-  ( ( B e. _V /\ A ~<_ _om ) -> ( A X. B ) ~<_ ( _om X. B ) )
5 2 3 4 syl2anc 
 |-  ( ( A ~<_ _om /\ B ~<_ _om ) -> ( A X. B ) ~<_ ( _om X. B ) )
6 omex 
 |-  _om e. _V
7 6 xpdom2 
 |-  ( B ~<_ _om -> ( _om X. B ) ~<_ ( _om X. _om ) )
8 7 adantl 
 |-  ( ( A ~<_ _om /\ B ~<_ _om ) -> ( _om X. B ) ~<_ ( _om X. _om ) )
9 domtr 
 |-  ( ( ( A X. B ) ~<_ ( _om X. B ) /\ ( _om X. B ) ~<_ ( _om X. _om ) ) -> ( A X. B ) ~<_ ( _om X. _om ) )
10 5 8 9 syl2anc 
 |-  ( ( A ~<_ _om /\ B ~<_ _om ) -> ( A X. B ) ~<_ ( _om X. _om ) )
11 xpomen 
 |-  ( _om X. _om ) ~~ _om
12 domentr 
 |-  ( ( ( A X. B ) ~<_ ( _om X. _om ) /\ ( _om X. _om ) ~~ _om ) -> ( A X. B ) ~<_ _om )
13 10 11 12 sylancl 
 |-  ( ( A ~<_ _om /\ B ~<_ _om ) -> ( A X. B ) ~<_ _om )