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 )