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	⊢ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝐶 ∈ 𝑉
Assertion	mpocti	⊢ ( ( 𝐴 ≼ ω ∧ 𝐵 ≼ ω ) → ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) ≼ ω )

Proof

Step	Hyp	Ref	Expression
1		mpocti.1	⊢ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝐶 ∈ 𝑉
2		eqid	⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 )
3	2	fnmpo	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝐶 ∈ 𝑉 → ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) Fn ( 𝐴 × 𝐵 ) )
4	1 3	ax-mp	⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) Fn ( 𝐴 × 𝐵 )
5		xpct	⊢ ( ( 𝐴 ≼ ω ∧ 𝐵 ≼ ω ) → ( 𝐴 × 𝐵 ) ≼ ω )
6		fnct	⊢ ( ( ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) Fn ( 𝐴 × 𝐵 ) ∧ ( 𝐴 × 𝐵 ) ≼ ω ) → ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) ≼ ω )
7	4 5 6	sylancr	⊢ ( ( 𝐴 ≼ ω ∧ 𝐵 ≼ ω ) → ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) ≼ ω )