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	$$⊢R=A\times B\to R=\mathrm{dom}R\times \mathrm{ran}R$$

Proof

Step	Hyp	Ref	Expression
1		simpl	$$⊢\left(R=A\times B\wedge \neg A\ne \varnothing \right)\to R=A\times B$$
2		simpr	$$⊢\left(R=A\times B\wedge \neg A\ne \varnothing \right)\to \neg A\ne \varnothing$$
3		nne	$$⊢\neg A\ne \varnothing \leftrightarrow A=\varnothing$$
4	2 3	sylib	$$⊢\left(R=A\times B\wedge \neg A\ne \varnothing \right)\to A=\varnothing$$
5	4	xpeq1d	$$⊢\left(R=A\times B\wedge \neg A\ne \varnothing \right)\to A\times B=\varnothing \times B$$
6		0xp	$$⊢\varnothing \times B=\varnothing$$
7	5 6	eqtrdi	$$⊢\left(R=A\times B\wedge \neg A\ne \varnothing \right)\to A\times B=\varnothing$$
8	1 7	eqtrd	$$⊢\left(R=A\times B\wedge \neg A\ne \varnothing \right)\to R=\varnothing$$
9	8	dmeqd	$$⊢\left(R=A\times B\wedge \neg A\ne \varnothing \right)\to \mathrm{dom}R=\mathrm{dom}\varnothing$$
10		dm0	$$⊢\mathrm{dom}\varnothing =\varnothing$$
11	9 10	eqtrdi	$$⊢\left(R=A\times B\wedge \neg A\ne \varnothing \right)\to \mathrm{dom}R=\varnothing$$
12	8	rneqd	$$⊢\left(R=A\times B\wedge \neg A\ne \varnothing \right)\to \mathrm{ran}R=\mathrm{ran}\varnothing$$
13		rn0	$$⊢\mathrm{ran}\varnothing =\varnothing$$
14	12 13	eqtrdi	$$⊢\left(R=A\times B\wedge \neg A\ne \varnothing \right)\to \mathrm{ran}R=\varnothing$$
15	11 14	xpeq12d	$$⊢\left(R=A\times B\wedge \neg A\ne \varnothing \right)\to \mathrm{dom}R\times \mathrm{ran}R=\varnothing \times \varnothing$$
16		0xp	$$⊢\varnothing \times \varnothing =\varnothing$$
17	15 16	eqtrdi	$$⊢\left(R=A\times B\wedge \neg A\ne \varnothing \right)\to \mathrm{dom}R\times \mathrm{ran}R=\varnothing$$
18	8 17	eqtr4d	$$⊢\left(R=A\times B\wedge \neg A\ne \varnothing \right)\to R=\mathrm{dom}R\times \mathrm{ran}R$$
19		simpl	$$⊢\left(R=A\times B\wedge \neg B\ne \varnothing \right)\to R=A\times B$$
20		simpr	$$⊢\left(R=A\times B\wedge \neg B\ne \varnothing \right)\to \neg B\ne \varnothing$$
21		nne	$$⊢\neg B\ne \varnothing \leftrightarrow B=\varnothing$$
22	20 21	sylib	$$⊢\left(R=A\times B\wedge \neg B\ne \varnothing \right)\to B=\varnothing$$
23	22	xpeq2d	$$⊢\left(R=A\times B\wedge \neg B\ne \varnothing \right)\to A\times B=A\times \varnothing$$
24		xp0	$$⊢A\times \varnothing =\varnothing$$
25	23 24	eqtrdi	$$⊢\left(R=A\times B\wedge \neg B\ne \varnothing \right)\to A\times B=\varnothing$$
26	19 25	eqtrd	$$⊢\left(R=A\times B\wedge \neg B\ne \varnothing \right)\to R=\varnothing$$
27	26	dmeqd	$$⊢\left(R=A\times B\wedge \neg B\ne \varnothing \right)\to \mathrm{dom}R=\mathrm{dom}\varnothing$$
28	27 10	eqtrdi	$$⊢\left(R=A\times B\wedge \neg B\ne \varnothing \right)\to \mathrm{dom}R=\varnothing$$
29	26	rneqd	$$⊢\left(R=A\times B\wedge \neg B\ne \varnothing \right)\to \mathrm{ran}R=\mathrm{ran}\varnothing$$
30	29 13	eqtrdi	$$⊢\left(R=A\times B\wedge \neg B\ne \varnothing \right)\to \mathrm{ran}R=\varnothing$$
31	28 30	xpeq12d	$$⊢\left(R=A\times B\wedge \neg B\ne \varnothing \right)\to \mathrm{dom}R\times \mathrm{ran}R=\varnothing \times \varnothing$$
32	31 16	eqtrdi	$$⊢\left(R=A\times B\wedge \neg B\ne \varnothing \right)\to \mathrm{dom}R\times \mathrm{ran}R=\varnothing$$
33	26 32	eqtr4d	$$⊢\left(R=A\times B\wedge \neg B\ne \varnothing \right)\to R=\mathrm{dom}R\times \mathrm{ran}R$$
34		simpl	$$⊢\left(R=A\times B\wedge \left(A\ne \varnothing \wedge B\ne \varnothing \right)\right)\to R=A\times B$$
35	34	dmeqd	$$⊢\left(R=A\times B\wedge \left(A\ne \varnothing \wedge B\ne \varnothing \right)\right)\to \mathrm{dom}R=\mathrm{dom}\left(A\times B\right)$$
36		dmxp	$$⊢B\ne \varnothing \to \mathrm{dom}\left(A\times B\right)=A$$
37	36	ad2antll	$$⊢\left(R=A\times B\wedge \left(A\ne \varnothing \wedge B\ne \varnothing \right)\right)\to \mathrm{dom}\left(A\times B\right)=A$$
38	35 37	eqtrd	$$⊢\left(R=A\times B\wedge \left(A\ne \varnothing \wedge B\ne \varnothing \right)\right)\to \mathrm{dom}R=A$$
39	34	rneqd	$$⊢\left(R=A\times B\wedge \left(A\ne \varnothing \wedge B\ne \varnothing \right)\right)\to \mathrm{ran}R=\mathrm{ran}\left(A\times B\right)$$
40		rnxp	$$⊢A\ne \varnothing \to \mathrm{ran}\left(A\times B\right)=B$$
41	40	ad2antrl	$$⊢\left(R=A\times B\wedge \left(A\ne \varnothing \wedge B\ne \varnothing \right)\right)\to \mathrm{ran}\left(A\times B\right)=B$$
42	39 41	eqtrd	$$⊢\left(R=A\times B\wedge \left(A\ne \varnothing \wedge B\ne \varnothing \right)\right)\to \mathrm{ran}R=B$$
43	38 42	xpeq12d	$$⊢\left(R=A\times B\wedge \left(A\ne \varnothing \wedge B\ne \varnothing \right)\right)\to \mathrm{dom}R\times \mathrm{ran}R=A\times B$$
44	34 43	eqtr4d	$$⊢\left(R=A\times B\wedge \left(A\ne \varnothing \wedge B\ne \varnothing \right)\right)\to R=\mathrm{dom}R\times \mathrm{ran}R$$
45	18 33 44	pm2.61dda	$$⊢R=A\times B\to R=\mathrm{dom}R\times \mathrm{ran}R$$