This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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