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