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