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 ( ( 𝐴 ≼ ω ∧ 𝐵 ≼ ω ) → ( 𝐴 × 𝐵 ) ≼ ω )

Proof

Step Hyp Ref Expression
1 ctex ( 𝐵 ≼ ω → 𝐵 ∈ V )
2 1 adantl ( ( 𝐴 ≼ ω ∧ 𝐵 ≼ ω ) → 𝐵 ∈ V )
3 simpl ( ( 𝐴 ≼ ω ∧ 𝐵 ≼ ω ) → 𝐴 ≼ ω )
4 xpdom1g ( ( 𝐵 ∈ V ∧ 𝐴 ≼ ω ) → ( 𝐴 × 𝐵 ) ≼ ( ω × 𝐵 ) )
5 2 3 4 syl2anc ( ( 𝐴 ≼ ω ∧ 𝐵 ≼ ω ) → ( 𝐴 × 𝐵 ) ≼ ( ω × 𝐵 ) )
6 omex ω ∈ V
7 6 xpdom2 ( 𝐵 ≼ ω → ( ω × 𝐵 ) ≼ ( ω × ω ) )
8 7 adantl ( ( 𝐴 ≼ ω ∧ 𝐵 ≼ ω ) → ( ω × 𝐵 ) ≼ ( ω × ω ) )
9 domtr ( ( ( 𝐴 × 𝐵 ) ≼ ( ω × 𝐵 ) ∧ ( ω × 𝐵 ) ≼ ( ω × ω ) ) → ( 𝐴 × 𝐵 ) ≼ ( ω × ω ) )
10 5 8 9 syl2anc ( ( 𝐴 ≼ ω ∧ 𝐵 ≼ ω ) → ( 𝐴 × 𝐵 ) ≼ ( ω × ω ) )
11 xpomen ( ω × ω ) ≈ ω
12 domentr ( ( ( 𝐴 × 𝐵 ) ≼ ( ω × ω ) ∧ ( ω × ω ) ≈ ω ) → ( 𝐴 × 𝐵 ) ≼ ω )
13 10 11 12 sylancl ( ( 𝐴 ≼ ω ∧ 𝐵 ≼ ω ) → ( 𝐴 × 𝐵 ) ≼ ω )