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	|- A. x e. A A. y e. B C e. V
Assertion	mpocti	|- ( ( A ~<_ _om /\ B ~<_ _om ) -> ( x e. A , y e. B |-> C ) ~<_ _om )

Proof

Step	Hyp	Ref	Expression
1		mpocti.1	|- A. x e. A A. y e. B C e. V
2		eqid	|- ( x e. A , y e. B |-> C ) = ( x e. A , y e. B |-> C )
3	2	fnmpo	|- ( A. x e. A A. y e. B C e. V -> ( x e. A , y e. B |-> C ) Fn ( A X. B ) )
4	1 3	ax-mp	|- ( x e. A , y e. B |-> C ) Fn ( A X. B )
5		xpct	|- ( ( A ~<_ _om /\ B ~<_ _om ) -> ( A X. B ) ~<_ _om )
6		fnct	|- ( ( ( x e. A , y e. B |-> C ) Fn ( A X. B ) /\ ( A X. B ) ~<_ _om ) -> ( x e. A , y e. B |-> C ) ~<_ _om )
7	4 5 6	sylancr	|- ( ( A ~<_ _om /\ B ~<_ _om ) -> ( x e. A , y e. B |-> C ) ~<_ _om )