Theorem relresfld

Description: Restriction of a relation to its field. (Contributed by FL, 15-Apr-2012)

	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		resundi	$$⊢{R\upharpoonright }_{\left(\mathrm{dom}R\cup \mathrm{ran}R\right)}=\left({R\upharpoonright }_{\mathrm{dom}R}\right)\cup \left({R\upharpoonright }_{\mathrm{ran}R}\right)$$
4		eqtr	$$⊢\left({R\upharpoonright }_{\bigcup \bigcup R}={R\upharpoonright }_{\left(\mathrm{dom}R\cup \mathrm{ran}R\right)}\wedge {R\upharpoonright }_{\left(\mathrm{dom}R\cup \mathrm{ran}R\right)}=\left({R\upharpoonright }_{\mathrm{dom}R}\right)\cup \left({R\upharpoonright }_{\mathrm{ran}R}\right)\right)\to {R\upharpoonright }_{\bigcup \bigcup R}=\left({R\upharpoonright }_{\mathrm{dom}R}\right)\cup \left({R\upharpoonright }_{\mathrm{ran}R}\right)$$
5		resss	$$⊢{R\upharpoonright }_{\mathrm{ran}R}\subseteq R$$
6		resdm	$$⊢\mathrm{Rel}R\to {R\upharpoonright }_{\mathrm{dom}R}=R$$
7		ssequn2	$$⊢{R\upharpoonright }_{\mathrm{ran}R}\subseteq R\leftrightarrow R\cup \left({R\upharpoonright }_{\mathrm{ran}R}\right)=R$$
8		uneq1	$$⊢{R\upharpoonright }_{\mathrm{dom}R}=R\to \left({R\upharpoonright }_{\mathrm{dom}R}\right)\cup \left({R\upharpoonright }_{\mathrm{ran}R}\right)=R\cup \left({R\upharpoonright }_{\mathrm{ran}R}\right)$$
9	8	eqeq2d	$$⊢{R\upharpoonright }_{\mathrm{dom}R}=R\to \left({R\upharpoonright }_{\bigcup \bigcup R}=\left({R\upharpoonright }_{\mathrm{dom}R}\right)\cup \left({R\upharpoonright }_{\mathrm{ran}R}\right)\leftrightarrow {R\upharpoonright }_{\bigcup \bigcup R}=R\cup \left({R\upharpoonright }_{\mathrm{ran}R}\right)\right)$$
10		eqtr	$$⊢\left({R\upharpoonright }_{\bigcup \bigcup R}=R\cup \left({R\upharpoonright }_{\mathrm{ran}R}\right)\wedge R\cup \left({R\upharpoonright }_{\mathrm{ran}R}\right)=R\right)\to {R\upharpoonright }_{\bigcup \bigcup R}=R$$
11	10	ex	$$⊢{R\upharpoonright }_{\bigcup \bigcup R}=R\cup \left({R\upharpoonright }_{\mathrm{ran}R}\right)\to \left(R\cup \left({R\upharpoonright }_{\mathrm{ran}R}\right)=R\to {R\upharpoonright }_{\bigcup \bigcup R}=R\right)$$
12	9 11	syl6bi	$$⊢{R\upharpoonright }_{\mathrm{dom}R}=R\to \left({R\upharpoonright }_{\bigcup \bigcup R}=\left({R\upharpoonright }_{\mathrm{dom}R}\right)\cup \left({R\upharpoonright }_{\mathrm{ran}R}\right)\to \left(R\cup \left({R\upharpoonright }_{\mathrm{ran}R}\right)=R\to {R\upharpoonright }_{\bigcup \bigcup R}=R\right)\right)$$
13	12	com3r	$$⊢R\cup \left({R\upharpoonright }_{\mathrm{ran}R}\right)=R\to \left({R\upharpoonright }_{\mathrm{dom}R}=R\to \left({R\upharpoonright }_{\bigcup \bigcup R}=\left({R\upharpoonright }_{\mathrm{dom}R}\right)\cup \left({R\upharpoonright }_{\mathrm{ran}R}\right)\to {R\upharpoonright }_{\bigcup \bigcup R}=R\right)\right)$$
14	7 13	sylbi	$$⊢{R\upharpoonright }_{\mathrm{ran}R}\subseteq R\to \left({R\upharpoonright }_{\mathrm{dom}R}=R\to \left({R\upharpoonright }_{\bigcup \bigcup R}=\left({R\upharpoonright }_{\mathrm{dom}R}\right)\cup \left({R\upharpoonright }_{\mathrm{ran}R}\right)\to {R\upharpoonright }_{\bigcup \bigcup R}=R\right)\right)$$
15	5 6 14	mpsyl	$$⊢\mathrm{Rel}R\to \left({R\upharpoonright }_{\bigcup \bigcup R}=\left({R\upharpoonright }_{\mathrm{dom}R}\right)\cup \left({R\upharpoonright }_{\mathrm{ran}R}\right)\to {R\upharpoonright }_{\bigcup \bigcup R}=R\right)$$
16	4 15	syl5com	$$⊢\left({R\upharpoonright }_{\bigcup \bigcup R}={R\upharpoonright }_{\left(\mathrm{dom}R\cup \mathrm{ran}R\right)}\wedge {R\upharpoonright }_{\left(\mathrm{dom}R\cup \mathrm{ran}R\right)}=\left({R\upharpoonright }_{\mathrm{dom}R}\right)\cup \left({R\upharpoonright }_{\mathrm{ran}R}\right)\right)\to \left(\mathrm{Rel}R\to {R\upharpoonright }_{\bigcup \bigcup R}=R\right)$$
17	2 3 16	sylancl	$$⊢\mathrm{Rel}R\to \left(\mathrm{Rel}R\to {R\upharpoonright }_{\bigcup \bigcup R}=R\right)$$
18	17	pm2.43i	$$⊢\mathrm{Rel}R\to {R\upharpoonright }_{\bigcup \bigcup R}=R$$