xpct

Description: The cartesian product of two countable sets is countable. (Contributed by Thierry Arnoux, 24-Sep-2017)

		Ref	Expression
	Assertion	xpct	$⊢ (A ≼ ω \land B ≼ ω) \to (A \times B) ≼ ω$

Step	Hyp	Ref	Expression
1		ctex	$⊢ B ≼ ω \to B \in V$
2	1	adantl	$⊢ (A ≼ ω \land B ≼ ω) \to B \in V$
3		simpl	$⊢ (A ≼ ω \land B ≼ ω) \to A ≼ ω$
4		xpdom1g	$⊢ (B \in V \land A ≼ ω) \to (A \times B) ≼ (ω \times B)$
5	2 3 4	syl2anc	$⊢ (A ≼ ω \land B ≼ ω) \to (A \times B) ≼ (ω \times B)$
6		omex	$⊢ ω \in V$
7	6	xpdom2	$⊢ B ≼ ω \to (ω \times B) ≼ (ω \times ω)$
8	7	adantl	$⊢ (A ≼ ω \land B ≼ ω) \to (ω \times B) ≼ (ω \times ω)$
9		domtr	$⊢ ((A \times B) ≼ (ω \times B) \land (ω \times B) ≼ (ω \times ω)) \to (A \times B) ≼ (ω \times ω)$
10	5 8 9	syl2anc	$⊢ (A ≼ ω \land B ≼ ω) \to (A \times B) ≼ (ω \times ω)$
11		xpomen	$⊢ (ω \times ω) \approx ω$
12		domentr	$⊢ ((A \times B) ≼ (ω \times ω) \land (ω \times ω) \approx ω) \to (A \times B) ≼ ω$
13	10 11 12	sylancl	$⊢ (A ≼ ω \land B ≼ ω) \to (A \times B) ≼ ω$

Metamath Proof Explorer