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

Metamath Proof Explorer

Theorem dmrnxp

Description: A Cartesian product is the Cartesian product of its domain and range. (Contributed by Zhi Wang, 30-Oct-2025)

Ref Expression
Assertion dmrnxp ( 𝑅 = ( 𝐴 × 𝐵 ) → 𝑅 = ( dom 𝑅 × ran 𝑅 ) )

Proof

Step Hyp Ref Expression
1 simpl ⊢ ( ( 𝑅 = ( 𝐴 × 𝐵 ) ∧ ¬ 𝐴 ≠ ∅ ) → 𝑅 = ( 𝐴 × 𝐵 ) )
2 simpr ⊢ ( ( 𝑅 = ( 𝐴 × 𝐵 ) ∧ ¬ 𝐴 ≠ ∅ ) → ¬ 𝐴 ≠ ∅ )
3 nne ⊢ ( ¬ 𝐴 ≠ ∅ ↔ 𝐴 = ∅ )
4 2 3 sylib ⊢ ( ( 𝑅 = ( 𝐴 × 𝐵 ) ∧ ¬ 𝐴 ≠ ∅ ) → 𝐴 = ∅ )
5 4 xpeq1d ⊢ ( ( 𝑅 = ( 𝐴 × 𝐵 ) ∧ ¬ 𝐴 ≠ ∅ ) → ( 𝐴 × 𝐵 ) = ( ∅ × 𝐵 ) )
6 0xp ⊢ ( ∅ × 𝐵 ) = ∅
7 5 6 eqtrdi ⊢ ( ( 𝑅 = ( 𝐴 × 𝐵 ) ∧ ¬ 𝐴 ≠ ∅ ) → ( 𝐴 × 𝐵 ) = ∅ )
8 1 7 eqtrd ⊢ ( ( 𝑅 = ( 𝐴 × 𝐵 ) ∧ ¬ 𝐴 ≠ ∅ ) → 𝑅 = ∅ )
9 8 dmeqd ⊢ ( ( 𝑅 = ( 𝐴 × 𝐵 ) ∧ ¬ 𝐴 ≠ ∅ ) → dom 𝑅 = dom ∅ )
10 dm0 ⊢ dom ∅ = ∅
11 9 10 eqtrdi ⊢ ( ( 𝑅 = ( 𝐴 × 𝐵 ) ∧ ¬ 𝐴 ≠ ∅ ) → dom 𝑅 = ∅ )
12 8 rneqd ⊢ ( ( 𝑅 = ( 𝐴 × 𝐵 ) ∧ ¬ 𝐴 ≠ ∅ ) → ran 𝑅 = ran ∅ )
13 rn0 ⊢ ran ∅ = ∅
14 12 13 eqtrdi ⊢ ( ( 𝑅 = ( 𝐴 × 𝐵 ) ∧ ¬ 𝐴 ≠ ∅ ) → ran 𝑅 = ∅ )
15 11 14 xpeq12d ⊢ ( ( 𝑅 = ( 𝐴 × 𝐵 ) ∧ ¬ 𝐴 ≠ ∅ ) → ( dom 𝑅 × ran 𝑅 ) = ( ∅ × ∅ ) )
16 0xp ⊢ ( ∅ × ∅ ) = ∅
17 15 16 eqtrdi ⊢ ( ( 𝑅 = ( 𝐴 × 𝐵 ) ∧ ¬ 𝐴 ≠ ∅ ) → ( dom 𝑅 × ran 𝑅 ) = ∅ )
18 8 17 eqtr4d ⊢ ( ( 𝑅 = ( 𝐴 × 𝐵 ) ∧ ¬ 𝐴 ≠ ∅ ) → 𝑅 = ( dom 𝑅 × ran 𝑅 ) )
19 simpl ⊢ ( ( 𝑅 = ( 𝐴 × 𝐵 ) ∧ ¬ 𝐵 ≠ ∅ ) → 𝑅 = ( 𝐴 × 𝐵 ) )
20 simpr ⊢ ( ( 𝑅 = ( 𝐴 × 𝐵 ) ∧ ¬ 𝐵 ≠ ∅ ) → ¬ 𝐵 ≠ ∅ )
21 nne ⊢ ( ¬ 𝐵 ≠ ∅ ↔ 𝐵 = ∅ )
22 20 21 sylib ⊢ ( ( 𝑅 = ( 𝐴 × 𝐵 ) ∧ ¬ 𝐵 ≠ ∅ ) → 𝐵 = ∅ )
23 22 xpeq2d ⊢ ( ( 𝑅 = ( 𝐴 × 𝐵 ) ∧ ¬ 𝐵 ≠ ∅ ) → ( 𝐴 × 𝐵 ) = ( 𝐴 × ∅ ) )
24 xp0 ⊢ ( 𝐴 × ∅ ) = ∅
25 23 24 eqtrdi ⊢ ( ( 𝑅 = ( 𝐴 × 𝐵 ) ∧ ¬ 𝐵 ≠ ∅ ) → ( 𝐴 × 𝐵 ) = ∅ )
26 19 25 eqtrd ⊢ ( ( 𝑅 = ( 𝐴 × 𝐵 ) ∧ ¬ 𝐵 ≠ ∅ ) → 𝑅 = ∅ )
27 26 dmeqd ⊢ ( ( 𝑅 = ( 𝐴 × 𝐵 ) ∧ ¬ 𝐵 ≠ ∅ ) → dom 𝑅 = dom ∅ )
28 27 10 eqtrdi ⊢ ( ( 𝑅 = ( 𝐴 × 𝐵 ) ∧ ¬ 𝐵 ≠ ∅ ) → dom 𝑅 = ∅ )
29 26 rneqd ⊢ ( ( 𝑅 = ( 𝐴 × 𝐵 ) ∧ ¬ 𝐵 ≠ ∅ ) → ran 𝑅 = ran ∅ )
30 29 13 eqtrdi ⊢ ( ( 𝑅 = ( 𝐴 × 𝐵 ) ∧ ¬ 𝐵 ≠ ∅ ) → ran 𝑅 = ∅ )
31 28 30 xpeq12d ⊢ ( ( 𝑅 = ( 𝐴 × 𝐵 ) ∧ ¬ 𝐵 ≠ ∅ ) → ( dom 𝑅 × ran 𝑅 ) = ( ∅ × ∅ ) )
32 31 16 eqtrdi ⊢ ( ( 𝑅 = ( 𝐴 × 𝐵 ) ∧ ¬ 𝐵 ≠ ∅ ) → ( dom 𝑅 × ran 𝑅 ) = ∅ )
33 26 32 eqtr4d ⊢ ( ( 𝑅 = ( 𝐴 × 𝐵 ) ∧ ¬ 𝐵 ≠ ∅ ) → 𝑅 = ( dom 𝑅 × ran 𝑅 ) )
34 simpl ⊢ ( ( 𝑅 = ( 𝐴 × 𝐵 ) ∧ ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ) → 𝑅 = ( 𝐴 × 𝐵 ) )
35 34 dmeqd ⊢ ( ( 𝑅 = ( 𝐴 × 𝐵 ) ∧ ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ) → dom 𝑅 = dom ( 𝐴 × 𝐵 ) )
36 dmxp ⊢ ( 𝐵 ≠ ∅ → dom ( 𝐴 × 𝐵 ) = 𝐴 )
37 36 ad2antll ⊢ ( ( 𝑅 = ( 𝐴 × 𝐵 ) ∧ ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ) → dom ( 𝐴 × 𝐵 ) = 𝐴 )
38 35 37 eqtrd ⊢ ( ( 𝑅 = ( 𝐴 × 𝐵 ) ∧ ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ) → dom 𝑅 = 𝐴 )
39 34 rneqd ⊢ ( ( 𝑅 = ( 𝐴 × 𝐵 ) ∧ ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ) → ran 𝑅 = ran ( 𝐴 × 𝐵 ) )
40 rnxp ⊢ ( 𝐴 ≠ ∅ → ran ( 𝐴 × 𝐵 ) = 𝐵 )
41 40 ad2antrl ⊢ ( ( 𝑅 = ( 𝐴 × 𝐵 ) ∧ ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ) → ran ( 𝐴 × 𝐵 ) = 𝐵 )
42 39 41 eqtrd ⊢ ( ( 𝑅 = ( 𝐴 × 𝐵 ) ∧ ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ) → ran 𝑅 = 𝐵 )
43 38 42 xpeq12d ⊢ ( ( 𝑅 = ( 𝐴 × 𝐵 ) ∧ ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ) → ( dom 𝑅 × ran 𝑅 ) = ( 𝐴 × 𝐵 ) )
44 34 43 eqtr4d ⊢ ( ( 𝑅 = ( 𝐴 × 𝐵 ) ∧ ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ) → 𝑅 = ( dom 𝑅 × ran 𝑅 ) )
45 18 33 44 pm2.61dda ⊢ ( 𝑅 = ( 𝐴 × 𝐵 ) → 𝑅 = ( dom 𝑅 × ran 𝑅 ) )