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

Metamath Proof Explorer

Theorem xpen

Description: Equinumerosity law for Cartesian product. Proposition 4.22(b) of Mendelson p. 254. (Contributed by NM, 24-Jul-2004) (Proof shortened by Mario Carneiro, 26-Apr-2015)

Ref Expression
Assertion xpen ( ( 𝐴 ≈ 𝐵 ∧ 𝐶 ≈ 𝐷 ) → ( 𝐴 × 𝐶 ) ≈ ( 𝐵 × 𝐷 ) )

Proof

Step Hyp Ref Expression
1 relen ⊢ Rel ≈
2 1 brrelex1i ⊢ ( 𝐶 ≈ 𝐷 → 𝐶 ∈ V )
3 endom ⊢ ( 𝐴 ≈ 𝐵 → 𝐴 ≼ 𝐵 )
4 xpdom1g ⊢ ( ( 𝐶 ∈ V ∧ 𝐴 ≼ 𝐵 ) → ( 𝐴 × 𝐶 ) ≼ ( 𝐵 × 𝐶 ) )
5 2 3 4 syl2anr ⊢ ( ( 𝐴 ≈ 𝐵 ∧ 𝐶 ≈ 𝐷 ) → ( 𝐴 × 𝐶 ) ≼ ( 𝐵 × 𝐶 ) )
6 1 brrelex2i ⊢ ( 𝐴 ≈ 𝐵 → 𝐵 ∈ V )
7 endom ⊢ ( 𝐶 ≈ 𝐷 → 𝐶 ≼ 𝐷 )
8 xpdom2g ⊢ ( ( 𝐵 ∈ V ∧ 𝐶 ≼ 𝐷 ) → ( 𝐵 × 𝐶 ) ≼ ( 𝐵 × 𝐷 ) )
9 6 7 8 syl2an ⊢ ( ( 𝐴 ≈ 𝐵 ∧ 𝐶 ≈ 𝐷 ) → ( 𝐵 × 𝐶 ) ≼ ( 𝐵 × 𝐷 ) )
10 domtr ⊢ ( ( ( 𝐴 × 𝐶 ) ≼ ( 𝐵 × 𝐶 ) ∧ ( 𝐵 × 𝐶 ) ≼ ( 𝐵 × 𝐷 ) ) → ( 𝐴 × 𝐶 ) ≼ ( 𝐵 × 𝐷 ) )
11 5 9 10 syl2anc ⊢ ( ( 𝐴 ≈ 𝐵 ∧ 𝐶 ≈ 𝐷 ) → ( 𝐴 × 𝐶 ) ≼ ( 𝐵 × 𝐷 ) )
12 1 brrelex2i ⊢ ( 𝐶 ≈ 𝐷 → 𝐷 ∈ V )
13 ensym ⊢ ( 𝐴 ≈ 𝐵 → 𝐵 ≈ 𝐴 )
14 endom ⊢ ( 𝐵 ≈ 𝐴 → 𝐵 ≼ 𝐴 )
15 13 14 syl ⊢ ( 𝐴 ≈ 𝐵 → 𝐵 ≼ 𝐴 )
16 xpdom1g ⊢ ( ( 𝐷 ∈ V ∧ 𝐵 ≼ 𝐴 ) → ( 𝐵 × 𝐷 ) ≼ ( 𝐴 × 𝐷 ) )
17 12 15 16 syl2anr ⊢ ( ( 𝐴 ≈ 𝐵 ∧ 𝐶 ≈ 𝐷 ) → ( 𝐵 × 𝐷 ) ≼ ( 𝐴 × 𝐷 ) )
18 1 brrelex1i ⊢ ( 𝐴 ≈ 𝐵 → 𝐴 ∈ V )
19 ensym ⊢ ( 𝐶 ≈ 𝐷 → 𝐷 ≈ 𝐶 )
20 endom ⊢ ( 𝐷 ≈ 𝐶 → 𝐷 ≼ 𝐶 )
21 19 20 syl ⊢ ( 𝐶 ≈ 𝐷 → 𝐷 ≼ 𝐶 )
22 xpdom2g ⊢ ( ( 𝐴 ∈ V ∧ 𝐷 ≼ 𝐶 ) → ( 𝐴 × 𝐷 ) ≼ ( 𝐴 × 𝐶 ) )
23 18 21 22 syl2an ⊢ ( ( 𝐴 ≈ 𝐵 ∧ 𝐶 ≈ 𝐷 ) → ( 𝐴 × 𝐷 ) ≼ ( 𝐴 × 𝐶 ) )
24 domtr ⊢ ( ( ( 𝐵 × 𝐷 ) ≼ ( 𝐴 × 𝐷 ) ∧ ( 𝐴 × 𝐷 ) ≼ ( 𝐴 × 𝐶 ) ) → ( 𝐵 × 𝐷 ) ≼ ( 𝐴 × 𝐶 ) )
25 17 23 24 syl2anc ⊢ ( ( 𝐴 ≈ 𝐵 ∧ 𝐶 ≈ 𝐷 ) → ( 𝐵 × 𝐷 ) ≼ ( 𝐴 × 𝐶 ) )
26 sbth ⊢ ( ( ( 𝐴 × 𝐶 ) ≼ ( 𝐵 × 𝐷 ) ∧ ( 𝐵 × 𝐷 ) ≼ ( 𝐴 × 𝐶 ) ) → ( 𝐴 × 𝐶 ) ≈ ( 𝐵 × 𝐷 ) )
27 11 25 26 syl2anc ⊢ ( ( 𝐴 ≈ 𝐵 ∧ 𝐶 ≈ 𝐷 ) → ( 𝐴 × 𝐶 ) ≈ ( 𝐵 × 𝐷 ) )