Metamath Proof Explorer

Theorem mpocti

Description: An operation is countable if both its domains are countable. (Contributed by Thierry Arnoux, 17-Sep-2017)

Ref Expression
Hypothesis mpocti.1 ⊢ ∀ x ∈ A ∀ y ∈ B C ∈ V
Assertion mpocti ⊢ A ≼ ω ∧ B ≼ ω → x ∈ A , y ∈ B ⟼ C ≼ ω

Proof

Step Hyp Ref Expression
1 mpocti.1 ⊢ ∀ x ∈ A ∀ y ∈ B C ∈ V
2 eqid ⊢ x ∈ A , y ∈ B ⟼ C = x ∈ A , y ∈ B ⟼ C
3 2 fnmpo ⊢ ∀ x ∈ A ∀ y ∈ B C ∈ V → x ∈ A , y ∈ B ⟼ C Fn A × B
4 1 3 ax-mp ⊢ x ∈ A , y ∈ B ⟼ C Fn A × B
5 xpct ⊢ A ≼ ω ∧ B ≼ ω → A × B ≼ ω
6 fnct ⊢ x ∈ A , y ∈ B ⟼ C Fn A × B ∧ A × B ≼ ω → x ∈ A , y ∈ B ⟼ C ≼ ω
7 4 5 6 sylancr ⊢ A ≼ ω ∧ B ≼ ω → x ∈ A , y ∈ B ⟼ C ≼ ω