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	$$⊢\forall x\in A\forall y\in BC\in V$$
Assertion	mpocti	$$⊢\left(A\preccurlyeq \mathrm{\omega }\wedge B\preccurlyeq \mathrm{\omega }\right)\to \left(x\in A,y\in B⟼C\right)\preccurlyeq \mathrm{\omega }$$

Proof

Step	Hyp	Ref	Expression
1		mpocti.1	$$⊢\forall x\in A\forall y\in BC\in V$$
2		eqid	$$⊢\left(x\in A,y\in B⟼C\right)=\left(x\in A,y\in B⟼C\right)$$
3	2	fnmpo	$$⊢\forall x\in A\forall y\in BC\in V\to \left(x\in A,y\in B⟼C\right)Fn\left(A\times B\right)$$
4	1 3	ax-mp	$$⊢\left(x\in A,y\in B⟼C\right)Fn\left(A\times B\right)$$
5		xpct	$$⊢\left(A\preccurlyeq \mathrm{\omega }\wedge B\preccurlyeq \mathrm{\omega }\right)\to \left(A\times B\right)\preccurlyeq \mathrm{\omega }$$
6		fnct	$$⊢\left(\left(x\in A,y\in B⟼C\right)Fn\left(A\times B\right)\wedge \left(A\times B\right)\preccurlyeq \mathrm{\omega }\right)\to \left(x\in A,y\in B⟼C\right)\preccurlyeq \mathrm{\omega }$$
7	4 5 6	sylancr	$$⊢\left(A\preccurlyeq \mathrm{\omega }\wedge B\preccurlyeq \mathrm{\omega }\right)\to \left(x\in A,y\in B⟼C\right)\preccurlyeq \mathrm{\omega }$$