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 ≼ ω ∧ B ≼ ω → A × B ≼ ω

Proof

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