Theorem dmrnxp 48815

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

Assertion

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

Proof of Theorem dmrnxp

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   = wceq 1540   ≠ wne 2926  ∅c0 4298   × cxp 5638  dom cdm 5640  ran crn 5641

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5253  ax-nul 5263  ax-pr 5389

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3919  df-un 3921  df-ss 3933  df-nul 4299  df-if 4491  df-sn 4592  df-pr 4594  df-op 4598  df-br 5110  df-opab 5172  df-xp 5646  df-rel 5647  df-cnv 5648  df-dm 5650  df-rn 5651

This theorem is referenced by: (None)