Metamath Proof Explorer

Theorem xpnum

Description: The cartesian product of numerable sets is numerable. (Contributed by Mario Carneiro, 3-Mar-2013) (Revised by Mario Carneiro, 29-Apr-2015)

		Ref	Expression
	Assertion	xpnum	$⊢ (A \in dom card \land B \in dom card) \to A \times B \in dom card$

Proof

Step	Hyp	Ref	Expression
1		isnum2	$⊢ A \in dom card \leftrightarrow \exists x \in On x \approx A$
2		isnum2	$⊢ B \in dom card \leftrightarrow \exists y \in On y \approx B$
3		reeanv	$⊢ \exists x \in On \exists y \in On (x \approx A \land y \approx B) \leftrightarrow (\exists x \in On x \approx A \land \exists y \in On y \approx B)$
4		omcl	$⊢ (x \in On \land y \in On) \to x \cdot_{𝑜} y \in On$
5		omxpen	$⊢ (x \in On \land y \in On) \to (x \cdot_{𝑜} y) \approx (x \times y)$
6		xpen	$⊢ (x \approx A \land y \approx B) \to (x \times y) \approx (A \times B)$
7		entr	$⊢ ((x \cdot_{𝑜} y) \approx (x \times y) \land (x \times y) \approx (A \times B)) \to (x \cdot_{𝑜} y) \approx (A \times B)$
8	5 6 7	syl2an	$⊢ ((x \in On \land y \in On) \land (x \approx A \land y \approx B)) \to (x \cdot_{𝑜} y) \approx (A \times B)$
9		isnumi	$⊢ (x \cdot_{𝑜} y \in On \land (x \cdot_{𝑜} y) \approx (A \times B)) \to A \times B \in dom card$
10	4 8 9	syl2an2r	$⊢ ((x \in On \land y \in On) \land (x \approx A \land y \approx B)) \to A \times B \in dom card$
11	10	ex	$⊢ (x \in On \land y \in On) \to ((x \approx A \land y \approx B) \to A \times B \in dom card)$
12	11	rexlimivv	$⊢ \exists x \in On \exists y \in On (x \approx A \land y \approx B) \to A \times B \in dom card$
13	3 12	sylbir	$⊢ (\exists x \in On x \approx A \land \exists y \in On y \approx B) \to A \times B \in dom card$
14	1 2 13	syl2anb	$⊢ (A \in dom card \land B \in dom card) \to A \times B \in dom card$