This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐴 ∈ 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 )