Theorem relresfld

Description: Restriction of a relation to its field. (Contributed by FL, 15-Apr-2012) (Proof shortened by Eric Schmidt, 16-Aug-2026)

	Ref	Expression
Assertion	relresfld	$$⊢\mathrm{Rel}R\to {R\upharpoonright }_{\bigcup \bigcup R}=R$$

Proof

Step	Hyp	Ref	Expression
1		relfld	$$⊢\mathrm{Rel}R\to \bigcup \bigcup R=\mathrm{dom}R\cup \mathrm{ran}R$$
2	1	reseq2d	$$⊢\mathrm{Rel}R\to {R\upharpoonright }_{\bigcup \bigcup R}={R\upharpoonright }_{\left(\mathrm{dom}R\cup \mathrm{ran}R\right)}$$
3		ssun1	$$⊢\mathrm{dom}R\subseteq \mathrm{dom}R\cup \mathrm{ran}R$$
4		relssres	$$⊢\left(\mathrm{Rel}R\wedge \mathrm{dom}R\subseteq \mathrm{dom}R\cup \mathrm{ran}R\right)\to {R\upharpoonright }_{\left(\mathrm{dom}R\cup \mathrm{ran}R\right)}=R$$
5	3 4	mpan2	$$⊢\mathrm{Rel}R\to {R\upharpoonright }_{\left(\mathrm{dom}R\cup \mathrm{ran}R\right)}=R$$
6	2 5	eqtrd	$$⊢\mathrm{Rel}R\to {R\upharpoonright }_{\bigcup \bigcup R}=R$$