Theorem xpct

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

	Ref	Expression
Assertion	xpct	⊢ ( ( 𝐴 ≼ ω ∧ 𝐵 ≼ ω ) → ( 𝐴 × 𝐵 ) ≼ ω )

Proof

Step	Hyp	Ref	Expression
1		ctex	⊢ ( 𝐵 ≼ ω → 𝐵 ∈ V )
2	1	adantl	⊢ ( ( 𝐴 ≼ ω ∧ 𝐵 ≼ ω ) → 𝐵 ∈ V )
3		simpl	⊢ ( ( 𝐴 ≼ ω ∧ 𝐵 ≼ ω ) → 𝐴 ≼ ω )
4		xpdom1g	⊢ ( ( 𝐵 ∈ V ∧ 𝐴 ≼ ω ) → ( 𝐴 × 𝐵 ) ≼ ( ω × 𝐵 ) )
5	2 3 4	syl2anc	⊢ ( ( 𝐴 ≼ ω ∧ 𝐵 ≼ ω ) → ( 𝐴 × 𝐵 ) ≼ ( ω × 𝐵 ) )
6		omex	⊢ ω ∈ V
7	6	xpdom2	⊢ ( 𝐵 ≼ ω → ( ω × 𝐵 ) ≼ ( ω × ω ) )
8	7	adantl	⊢ ( ( 𝐴 ≼ ω ∧ 𝐵 ≼ ω ) → ( ω × 𝐵 ) ≼ ( ω × ω ) )
9		domtr	⊢ ( ( ( 𝐴 × 𝐵 ) ≼ ( ω × 𝐵 ) ∧ ( ω × 𝐵 ) ≼ ( ω × ω ) ) → ( 𝐴 × 𝐵 ) ≼ ( ω × ω ) )
10	5 8 9	syl2anc	⊢ ( ( 𝐴 ≼ ω ∧ 𝐵 ≼ ω ) → ( 𝐴 × 𝐵 ) ≼ ( ω × ω ) )
11		xpomen	⊢ ( ω × ω ) ≈ ω
12		domentr	⊢ ( ( ( 𝐴 × 𝐵 ) ≼ ( ω × ω ) ∧ ( ω × ω ) ≈ ω ) → ( 𝐴 × 𝐵 ) ≼ ω )
13	10 11 12	sylancl	⊢ ( ( 𝐴 ≼ ω ∧ 𝐵 ≼ ω ) → ( 𝐴 × 𝐵 ) ≼ ω )