Theorem reldmun

Description: Split a relation into two parts based on its domain. (Contributed by Thierry Arnoux, 9-Oct-2023) Remove requirement that A and B are disjoint. (Revised by Eric Schmidt, 20-Jun-2026)

	Ref	Expression
Assertion	reldmun	$$⊢\left(\mathrm{Rel}R\wedge \mathrm{dom}R=A\cup B\right)\to R=\left({R\upharpoonright }_A\right)\cup \left({R\upharpoonright }_B\right)$$

Proof

Step	Hyp	Ref	Expression
1		reseq2	$$⊢\mathrm{dom}R=A\cup B\to {R\upharpoonright }_{\mathrm{dom}R}={R\upharpoonright }_{\left(A\cup B\right)}$$
2	1	adantl	$$⊢\left(\mathrm{Rel}R\wedge \mathrm{dom}R=A\cup B\right)\to {R\upharpoonright }_{\mathrm{dom}R}={R\upharpoonright }_{\left(A\cup B\right)}$$
3		resdm	$$⊢\mathrm{Rel}R\to {R\upharpoonright }_{\mathrm{dom}R}=R$$
4	3	adantr	$$⊢\left(\mathrm{Rel}R\wedge \mathrm{dom}R=A\cup B\right)\to {R\upharpoonright }_{\mathrm{dom}R}=R$$
5		resundi	$$⊢{R\upharpoonright }_{\left(A\cup B\right)}=\left({R\upharpoonright }_A\right)\cup \left({R\upharpoonright }_B\right)$$
6	5	a1i	$$⊢\left(\mathrm{Rel}R\wedge \mathrm{dom}R=A\cup B\right)\to {R\upharpoonright }_{\left(A\cup B\right)}=\left({R\upharpoonright }_A\right)\cup \left({R\upharpoonright }_B\right)$$
7	2 4 6	3eqtr3d	$$⊢\left(\mathrm{Rel}R\wedge \mathrm{dom}R=A\cup B\right)\to R=\left({R\upharpoonright }_A\right)\cup \left({R\upharpoonright }_B\right)$$