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	⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ) → ( 𝐴 × 𝐵 ) ∈ dom card )

Proof

Step	Hyp	Ref	Expression
1		isnum2	⊢ ( 𝐴 ∈ dom card ↔ ∃ 𝑥 ∈ On 𝑥 ≈ 𝐴 )
2		isnum2	⊢ ( 𝐵 ∈ dom card ↔ ∃ 𝑦 ∈ On 𝑦 ≈ 𝐵 )
3		reeanv	⊢ ( ∃ 𝑥 ∈ On ∃ 𝑦 ∈ On ( 𝑥 ≈ 𝐴 ∧ 𝑦 ≈ 𝐵 ) ↔ ( ∃ 𝑥 ∈ On 𝑥 ≈ 𝐴 ∧ ∃ 𝑦 ∈ On 𝑦 ≈ 𝐵 ) )
4		omcl	⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ On ) → ( 𝑥 ·o 𝑦 ) ∈ On )
5		omxpen	⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ On ) → ( 𝑥 ·o 𝑦 ) ≈ ( 𝑥 × 𝑦 ) )
6		xpen	⊢ ( ( 𝑥 ≈ 𝐴 ∧ 𝑦 ≈ 𝐵 ) → ( 𝑥 × 𝑦 ) ≈ ( 𝐴 × 𝐵 ) )
7		entr	⊢ ( ( ( 𝑥 ·o 𝑦 ) ≈ ( 𝑥 × 𝑦 ) ∧ ( 𝑥 × 𝑦 ) ≈ ( 𝐴 × 𝐵 ) ) → ( 𝑥 ·o 𝑦 ) ≈ ( 𝐴 × 𝐵 ) )
8	5 6 7	syl2an	⊢ ( ( ( 𝑥 ∈ On ∧ 𝑦 ∈ On ) ∧ ( 𝑥 ≈ 𝐴 ∧ 𝑦 ≈ 𝐵 ) ) → ( 𝑥 ·o 𝑦 ) ≈ ( 𝐴 × 𝐵 ) )
9		isnumi	⊢ ( ( ( 𝑥 ·o 𝑦 ) ∈ On ∧ ( 𝑥 ·o 𝑦 ) ≈ ( 𝐴 × 𝐵 ) ) → ( 𝐴 × 𝐵 ) ∈ dom card )
10	4 8 9	syl2an2r	⊢ ( ( ( 𝑥 ∈ On ∧ 𝑦 ∈ On ) ∧ ( 𝑥 ≈ 𝐴 ∧ 𝑦 ≈ 𝐵 ) ) → ( 𝐴 × 𝐵 ) ∈ dom card )
11	10	ex	⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ On ) → ( ( 𝑥 ≈ 𝐴 ∧ 𝑦 ≈ 𝐵 ) → ( 𝐴 × 𝐵 ) ∈ dom card ) )
12	11	rexlimivv	⊢ ( ∃ 𝑥 ∈ On ∃ 𝑦 ∈ On ( 𝑥 ≈ 𝐴 ∧ 𝑦 ≈ 𝐵 ) → ( 𝐴 × 𝐵 ) ∈ dom card )
13	3 12	sylbir	⊢ ( ( ∃ 𝑥 ∈ On 𝑥 ≈ 𝐴 ∧ ∃ 𝑦 ∈ On 𝑦 ≈ 𝐵 ) → ( 𝐴 × 𝐵 ) ∈ dom card )
14	1 2 13	syl2anb	⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ) → ( 𝐴 × 𝐵 ) ∈ dom card )