Theorem iunrelexp0

Description: Simplification of zeroth power of indexed union of powers of relations. (Contributed by RP, 19-Jun-2020)

	Ref	Expression
Assertion	iunrelexp0	$$⊢\left(R\in V\wedge Z\subseteq {\mathbb{N}}_0\wedge \left\{0,1\right\}\cap Z\ne \varnothing \right)\to \bigcup _{x\in Z}\left(R{\uparrow }_{r}x\right){\uparrow }_{r}0=R{\uparrow }_{r}0$$

Proof

Step	Hyp	Ref	Expression
1		df-pr	$$⊢\left\{0,1\right\}=\left\{0\right\}\cup \left\{1\right\}$$
2	1	ineq1i	$$⊢\left\{0,1\right\}\cap Z=\left(\left\{0\right\}\cup \left\{1\right\}\right)\cap Z$$
3		indir	$$⊢\left(\left\{0\right\}\cup \left\{1\right\}\right)\cap Z=\left(\left\{0\right\}\cap Z\right)\cup \left(\left\{1\right\}\cap Z\right)$$
4	2 3	eqtr2i	$$⊢\left(\left\{0\right\}\cap Z\right)\cup \left(\left\{1\right\}\cap Z\right)=\left\{0,1\right\}\cap Z$$
5	4	uneq1i	$$⊢\left(\left(\left\{0\right\}\cap Z\right)\cup \left(\left\{1\right\}\cap Z\right)\right)\cup Z=\left(\left\{0,1\right\}\cap Z\right)\cup Z$$
6		inss2	$$⊢\left\{0,1\right\}\cap Z\subseteq Z$$
7		ssequn1	$$⊢\left\{0,1\right\}\cap Z\subseteq Z\leftrightarrow \left(\left\{0,1\right\}\cap Z\right)\cup Z=Z$$
8	6 7	mpbi	$$⊢\left(\left\{0,1\right\}\cap Z\right)\cup Z=Z$$
9	5 8	eqtr2i	$$⊢Z=\left(\left(\left\{0\right\}\cap Z\right)\cup \left(\left\{1\right\}\cap Z\right)\right)\cup Z$$
10		iuneq1	$$⊢Z=\left(\left(\left\{0\right\}\cap Z\right)\cup \left(\left\{1\right\}\cap Z\right)\right)\cup Z\to \bigcup _{x\in Z}\left(R{\uparrow }_{r}x\right)=\bigcup _{x\in \left(\left(\left\{0\right\}\cap Z\right)\cup \left(\left\{1\right\}\cap Z\right)\right)\cup Z}\left(R{\uparrow }_{r}x\right)$$
11	10	oveq1d	$$⊢Z=\left(\left(\left\{0\right\}\cap Z\right)\cup \left(\left\{1\right\}\cap Z\right)\right)\cup Z\to \bigcup _{x\in Z}\left(R{\uparrow }_{r}x\right){\uparrow }_{r}0=\bigcup _{x\in \left(\left(\left\{0\right\}\cap Z\right)\cup \left(\left\{1\right\}\cap Z\right)\right)\cup Z}\left(R{\uparrow }_{r}x\right){\uparrow }_{r}0$$
12	9 11	ax-mp	$$⊢\bigcup _{x\in Z}\left(R{\uparrow }_{r}x\right){\uparrow }_{r}0=\bigcup _{x\in \left(\left(\left\{0\right\}\cap Z\right)\cup \left(\left\{1\right\}\cap Z\right)\right)\cup Z}\left(R{\uparrow }_{r}x\right){\uparrow }_{r}0$$
13		dmiun	$$⊢\mathrm{dom}\bigcup _{x\in \left(\left(\left\{0\right\}\cap Z\right)\cup \left(\left\{1\right\}\cap Z\right)\right)\cup Z}\left(R{\uparrow }_{r}x\right)=\bigcup _{x\in \left(\left(\left\{0\right\}\cap Z\right)\cup \left(\left\{1\right\}\cap Z\right)\right)\cup Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)$$
14		iunxun	$$⊢\bigcup _{x\in \left(\left(\left\{0\right\}\cap Z\right)\cup \left(\left\{1\right\}\cap Z\right)\right)\cup Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)=\bigcup _{x\in \left(\left\{0\right\}\cap Z\right)\cup \left(\left\{1\right\}\cap Z\right)}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)$$
15		iunxun	$$⊢\bigcup _{x\in \left(\left\{0\right\}\cap Z\right)\cup \left(\left\{1\right\}\cap Z\right)}\mathrm{dom}\left(R{\uparrow }_{r}x\right)=\bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)$$
16	15	equncomi	$$⊢\bigcup _{x\in \left(\left\{0\right\}\cap Z\right)\cup \left(\left\{1\right\}\cap Z\right)}\mathrm{dom}\left(R{\uparrow }_{r}x\right)=\bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)$$
17	16	uneq1i	$$⊢\bigcup _{x\in \left(\left\{0\right\}\cap Z\right)\cup \left(\left\{1\right\}\cap Z\right)}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)=\left(\bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\right)\cup \bigcup _{x\in Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)$$
18	17	equncomi	$$⊢\bigcup _{x\in \left(\left\{0\right\}\cap Z\right)\cup \left(\left\{1\right\}\cap Z\right)}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)=\bigcup _{x\in Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \left(\bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\right)$$
19	13 14 18	3eqtri	$$⊢\mathrm{dom}\bigcup _{x\in \left(\left(\left\{0\right\}\cap Z\right)\cup \left(\left\{1\right\}\cap Z\right)\right)\cup Z}\left(R{\uparrow }_{r}x\right)=\bigcup _{x\in Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \left(\bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\right)$$
20		rniun	$$⊢\mathrm{ran}\bigcup _{x\in \left(\left(\left\{0\right\}\cap Z\right)\cup \left(\left\{1\right\}\cap Z\right)\right)\cup Z}\left(R{\uparrow }_{r}x\right)=\bigcup _{x\in \left(\left(\left\{0\right\}\cap Z\right)\cup \left(\left\{1\right\}\cap Z\right)\right)\cup Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)$$
21		iunxun	$$⊢\bigcup _{x\in \left(\left(\left\{0\right\}\cap Z\right)\cup \left(\left\{1\right\}\cap Z\right)\right)\cup Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)=\bigcup _{x\in \left(\left\{0\right\}\cap Z\right)\cup \left(\left\{1\right\}\cap Z\right)}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)$$
22		iunxun	$$⊢\bigcup _{x\in \left(\left\{0\right\}\cap Z\right)\cup \left(\left\{1\right\}\cap Z\right)}\mathrm{ran}\left(R{\uparrow }_{r}x\right)=\bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)$$
23	22	uneq1i	$$⊢\bigcup _{x\in \left(\left\{0\right\}\cap Z\right)\cup \left(\left\{1\right\}\cap Z\right)}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)=\left(\bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\right)\cup \bigcup _{x\in Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)$$
24	20 21 23	3eqtri	$$⊢\mathrm{ran}\bigcup _{x\in \left(\left(\left\{0\right\}\cap Z\right)\cup \left(\left\{1\right\}\cap Z\right)\right)\cup Z}\left(R{\uparrow }_{r}x\right)=\left(\bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\right)\cup \bigcup _{x\in Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)$$
25	19 24	uneq12i	$$⊢\mathrm{dom}\bigcup _{x\in \left(\left(\left\{0\right\}\cap Z\right)\cup \left(\left\{1\right\}\cap Z\right)\right)\cup Z}\left(R{\uparrow }_{r}x\right)\cup \mathrm{ran}\bigcup _{x\in \left(\left(\left\{0\right\}\cap Z\right)\cup \left(\left\{1\right\}\cap Z\right)\right)\cup Z}\left(R{\uparrow }_{r}x\right)=\left(\bigcup _{x\in Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \left(\bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\right)\right)\cup \left(\left(\bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\right)\cup \bigcup _{x\in Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\right)$$
26		uncom	$$⊢\bigcup _{x\in Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \left(\bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\right)=\left(\bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\right)\cup \bigcup _{x\in Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)$$
27	26	uneq1i	$$⊢\left(\bigcup _{x\in Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \left(\bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\right)\right)\cup \left(\left(\bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\right)\cup \bigcup _{x\in Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\right)=\left(\left(\bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\right)\cup \bigcup _{x\in Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\right)\cup \left(\left(\bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\right)\cup \bigcup _{x\in Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\right)$$
28		un4	$$⊢\left(\left(\bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\right)\cup \bigcup _{x\in Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\right)\cup \left(\left(\bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\right)\cup \bigcup _{x\in Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\right)=\left(\left(\bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\right)\cup \left(\bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\right)\right)\cup \left(\bigcup _{x\in Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\right)$$
29	27 28	eqtri	$$⊢\left(\bigcup _{x\in Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \left(\bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\right)\right)\cup \left(\left(\bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\right)\cup \bigcup _{x\in Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\right)=\left(\left(\bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\right)\cup \left(\bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\right)\right)\cup \left(\bigcup _{x\in Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\right)$$
30		uncom	$$⊢\bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)=\bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)$$
31	30	uneq1i	$$⊢\left(\bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\right)\cup \left(\bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\right)=\left(\bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\right)\cup \left(\bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\right)$$
32		un4	$$⊢\left(\bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\right)\cup \left(\bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\right)=\left(\bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\right)\cup \left(\bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\right)$$
33	31 32	eqtri	$$⊢\left(\bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\right)\cup \left(\bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\right)=\left(\bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\right)\cup \left(\bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\right)$$
34	33	uneq1i	$$⊢\left(\left(\bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\right)\cup \left(\bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\right)\right)\cup \left(\bigcup _{x\in Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\right)=\left(\left(\bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\right)\cup \left(\bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\right)\right)\cup \left(\bigcup _{x\in Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\right)$$
35	25 29 34	3eqtri	$$⊢\mathrm{dom}\bigcup _{x\in \left(\left(\left\{0\right\}\cap Z\right)\cup \left(\left\{1\right\}\cap Z\right)\right)\cup Z}\left(R{\uparrow }_{r}x\right)\cup \mathrm{ran}\bigcup _{x\in \left(\left(\left\{0\right\}\cap Z\right)\cup \left(\left\{1\right\}\cap Z\right)\right)\cup Z}\left(R{\uparrow }_{r}x\right)=\left(\left(\bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\right)\cup \left(\bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\right)\right)\cup \left(\bigcup _{x\in Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\right)$$
36		df-ne	$$⊢\left\{0,1\right\}\cap Z\ne \varnothing \leftrightarrow \neg \left\{0,1\right\}\cap Z=\varnothing$$
37		incom	$$⊢\left\{0,1\right\}\cap Z=Z\cap \left\{0,1\right\}$$
38	1	ineq2i	$$⊢Z\cap \left\{0,1\right\}=Z\cap \left(\left\{0\right\}\cup \left\{1\right\}\right)$$
39		indi	$$⊢Z\cap \left(\left\{0\right\}\cup \left\{1\right\}\right)=\left(Z\cap \left\{0\right\}\right)\cup \left(Z\cap \left\{1\right\}\right)$$
40	37 38 39	3eqtri	$$⊢\left\{0,1\right\}\cap Z=\left(Z\cap \left\{0\right\}\right)\cup \left(Z\cap \left\{1\right\}\right)$$
41	40	eqeq1i	$$⊢\left\{0,1\right\}\cap Z=\varnothing \leftrightarrow \left(Z\cap \left\{0\right\}\right)\cup \left(Z\cap \left\{1\right\}\right)=\varnothing$$
42		un00	$$⊢\left(Z\cap \left\{0\right\}=\varnothing \wedge Z\cap \left\{1\right\}=\varnothing \right)\leftrightarrow \left(Z\cap \left\{0\right\}\right)\cup \left(Z\cap \left\{1\right\}\right)=\varnothing$$
43		anor	$$⊢\left(Z\cap \left\{0\right\}=\varnothing \wedge Z\cap \left\{1\right\}=\varnothing \right)\leftrightarrow \neg \left(\neg Z\cap \left\{0\right\}=\varnothing \vee \neg Z\cap \left\{1\right\}=\varnothing \right)$$
44	41 42 43	3bitr2i	$$⊢\left\{0,1\right\}\cap Z=\varnothing \leftrightarrow \neg \left(\neg Z\cap \left\{0\right\}=\varnothing \vee \neg Z\cap \left\{1\right\}=\varnothing \right)$$
45	44	notbii	$$⊢\neg \left\{0,1\right\}\cap Z=\varnothing \leftrightarrow \neg \neg \left(\neg Z\cap \left\{0\right\}=\varnothing \vee \neg Z\cap \left\{1\right\}=\varnothing \right)$$
46		notnotb	$$⊢\left(\neg Z\cap \left\{0\right\}=\varnothing \vee \neg Z\cap \left\{1\right\}=\varnothing \right)\leftrightarrow \neg \neg \left(\neg Z\cap \left\{0\right\}=\varnothing \vee \neg Z\cap \left\{1\right\}=\varnothing \right)$$
47		disjsn	$$⊢Z\cap \left\{0\right\}=\varnothing \leftrightarrow \neg 0\in Z$$
48	47	notbii	$$⊢\neg Z\cap \left\{0\right\}=\varnothing \leftrightarrow \neg \neg 0\in Z$$
49		notnotb	$$⊢0\in Z\leftrightarrow \neg \neg 0\in Z$$
50	48 49	bitr4i	$$⊢\neg Z\cap \left\{0\right\}=\varnothing \leftrightarrow 0\in Z$$
51		disjsn	$$⊢Z\cap \left\{1\right\}=\varnothing \leftrightarrow \neg 1\in Z$$
52	51	notbii	$$⊢\neg Z\cap \left\{1\right\}=\varnothing \leftrightarrow \neg \neg 1\in Z$$
53		notnotb	$$⊢1\in Z\leftrightarrow \neg \neg 1\in Z$$
54	52 53	bitr4i	$$⊢\neg Z\cap \left\{1\right\}=\varnothing \leftrightarrow 1\in Z$$
55	50 54	orbi12i	$$⊢\left(\neg Z\cap \left\{0\right\}=\varnothing \vee \neg Z\cap \left\{1\right\}=\varnothing \right)\leftrightarrow \left(0\in Z\vee 1\in Z\right)$$
56	45 46 55	3bitr2i	$$⊢\neg \left\{0,1\right\}\cap Z=\varnothing \leftrightarrow \left(0\in Z\vee 1\in Z\right)$$
57	36 56	sylbb	$$⊢\left\{0,1\right\}\cap Z\ne \varnothing \to \left(0\in Z\vee 1\in Z\right)$$
58		simpl	$$⊢\left(0\in Z\wedge \left(Z\subseteq {\mathbb{N}}_0\wedge R\in V\right)\right)\to 0\in Z$$
59	58	snssd	$$⊢\left(0\in Z\wedge \left(Z\subseteq {\mathbb{N}}_0\wedge R\in V\right)\right)\to \left\{0\right\}\subseteq Z$$
60		df-ss	$$⊢\left\{0\right\}\subseteq Z\leftrightarrow \left\{0\right\}\cap Z=\left\{0\right\}$$
61	59 60	sylib	$$⊢\left(0\in Z\wedge \left(Z\subseteq {\mathbb{N}}_0\wedge R\in V\right)\right)\to \left\{0\right\}\cap Z=\left\{0\right\}$$
62	61	iuneq1d	$$⊢\left(0\in Z\wedge \left(Z\subseteq {\mathbb{N}}_0\wedge R\in V\right)\right)\to \bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)=\bigcup _{x\in \left\{0\right\}}\mathrm{dom}\left(R{\uparrow }_{r}x\right)$$
63		c0ex	$$⊢0\in \mathrm{V}$$
64		oveq2	$$⊢x=0\to R{\uparrow }_{r}x=R{\uparrow }_{r}0$$
65	64	dmeqd	$$⊢x=0\to \mathrm{dom}\left(R{\uparrow }_{r}x\right)=\mathrm{dom}\left(R{\uparrow }_{r}0\right)$$
66	63 65	iunxsn	$$⊢\bigcup _{x\in \left\{0\right\}}\mathrm{dom}\left(R{\uparrow }_{r}x\right)=\mathrm{dom}\left(R{\uparrow }_{r}0\right)$$
67	62 66	eqtrdi	$$⊢\left(0\in Z\wedge \left(Z\subseteq {\mathbb{N}}_0\wedge R\in V\right)\right)\to \bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)=\mathrm{dom}\left(R{\uparrow }_{r}0\right)$$
68		relexp0g	$$⊢R\in V\to R{\uparrow }_{r}0={\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}R\cup \mathrm{ran}R\right)}$$
69	68	ad2antll	$$⊢\left(0\in Z\wedge \left(Z\subseteq {\mathbb{N}}_0\wedge R\in V\right)\right)\to R{\uparrow }_{r}0={\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}R\cup \mathrm{ran}R\right)}$$
70	69	dmeqd	$$⊢\left(0\in Z\wedge \left(Z\subseteq {\mathbb{N}}_0\wedge R\in V\right)\right)\to \mathrm{dom}\left(R{\uparrow }_{r}0\right)=\mathrm{dom}\left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}R\cup \mathrm{ran}R\right)}\right)$$
71		dmresi	$$⊢\mathrm{dom}\left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}R\cup \mathrm{ran}R\right)}\right)=\mathrm{dom}R\cup \mathrm{ran}R$$
72	70 71	eqtrdi	$$⊢\left(0\in Z\wedge \left(Z\subseteq {\mathbb{N}}_0\wedge R\in V\right)\right)\to \mathrm{dom}\left(R{\uparrow }_{r}0\right)=\mathrm{dom}R\cup \mathrm{ran}R$$
73	67 72	eqtrd	$$⊢\left(0\in Z\wedge \left(Z\subseteq {\mathbb{N}}_0\wedge R\in V\right)\right)\to \bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)=\mathrm{dom}R\cup \mathrm{ran}R$$
74	61	iuneq1d	$$⊢\left(0\in Z\wedge \left(Z\subseteq {\mathbb{N}}_0\wedge R\in V\right)\right)\to \bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)=\bigcup _{x\in \left\{0\right\}}\mathrm{ran}\left(R{\uparrow }_{r}x\right)$$
75	64	rneqd	$$⊢x=0\to \mathrm{ran}\left(R{\uparrow }_{r}x\right)=\mathrm{ran}\left(R{\uparrow }_{r}0\right)$$
76	63 75	iunxsn	$$⊢\bigcup _{x\in \left\{0\right\}}\mathrm{ran}\left(R{\uparrow }_{r}x\right)=\mathrm{ran}\left(R{\uparrow }_{r}0\right)$$
77	74 76	eqtrdi	$$⊢\left(0\in Z\wedge \left(Z\subseteq {\mathbb{N}}_0\wedge R\in V\right)\right)\to \bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)=\mathrm{ran}\left(R{\uparrow }_{r}0\right)$$
78	69	rneqd	$$⊢\left(0\in Z\wedge \left(Z\subseteq {\mathbb{N}}_0\wedge R\in V\right)\right)\to \mathrm{ran}\left(R{\uparrow }_{r}0\right)=\mathrm{ran}\left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}R\cup \mathrm{ran}R\right)}\right)$$
79		rnresi	$$⊢\mathrm{ran}\left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}R\cup \mathrm{ran}R\right)}\right)=\mathrm{dom}R\cup \mathrm{ran}R$$
80	78 79	eqtrdi	$$⊢\left(0\in Z\wedge \left(Z\subseteq {\mathbb{N}}_0\wedge R\in V\right)\right)\to \mathrm{ran}\left(R{\uparrow }_{r}0\right)=\mathrm{dom}R\cup \mathrm{ran}R$$
81	77 80	eqtrd	$$⊢\left(0\in Z\wedge \left(Z\subseteq {\mathbb{N}}_0\wedge R\in V\right)\right)\to \bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)=\mathrm{dom}R\cup \mathrm{ran}R$$
82	73 81	uneq12d	$$⊢\left(0\in Z\wedge \left(Z\subseteq {\mathbb{N}}_0\wedge R\in V\right)\right)\to \bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)=\left(\mathrm{dom}R\cup \mathrm{ran}R\right)\cup \left(\mathrm{dom}R\cup \mathrm{ran}R\right)$$
83		unidm	$$⊢\left(\mathrm{dom}R\cup \mathrm{ran}R\right)\cup \left(\mathrm{dom}R\cup \mathrm{ran}R\right)=\mathrm{dom}R\cup \mathrm{ran}R$$
84	82 83	eqtrdi	$$⊢\left(0\in Z\wedge \left(Z\subseteq {\mathbb{N}}_0\wedge R\in V\right)\right)\to \bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)=\mathrm{dom}R\cup \mathrm{ran}R$$
85	84	uneq1d	$$⊢\left(0\in Z\wedge \left(Z\subseteq {\mathbb{N}}_0\wedge R\in V\right)\right)\to \left(\bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\right)\cup \left(\bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\right)=\left(\mathrm{dom}R\cup \mathrm{ran}R\right)\cup \left(\bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\right)$$
86		relexpdmg	$$⊢\left(x\in {\mathbb{N}}_0\wedge R\in V\right)\to \mathrm{dom}\left(R{\uparrow }_{r}x\right)\subseteq \mathrm{dom}R\cup \mathrm{ran}R$$
87	86	expcom	$$⊢R\in V\to \left(x\in {\mathbb{N}}_0\to \mathrm{dom}\left(R{\uparrow }_{r}x\right)\subseteq \mathrm{dom}R\cup \mathrm{ran}R\right)$$
88	87	ralrimiv	$$⊢R\in V\to \forall x\in {\mathbb{N}}_0\mathrm{dom}\left(R{\uparrow }_{r}x\right)\subseteq \mathrm{dom}R\cup \mathrm{ran}R$$
89	88	ad2antll	$$⊢\left(0\in Z\wedge \left(Z\subseteq {\mathbb{N}}_0\wedge R\in V\right)\right)\to \forall x\in {\mathbb{N}}_0\mathrm{dom}\left(R{\uparrow }_{r}x\right)\subseteq \mathrm{dom}R\cup \mathrm{ran}R$$
90		olc	$$⊢Z\subseteq {\mathbb{N}}_0\to \left(\left\{1\right\}\subseteq {\mathbb{N}}_0\vee Z\subseteq {\mathbb{N}}_0\right)$$
91	90	ad2antrl	$$⊢\left(0\in Z\wedge \left(Z\subseteq {\mathbb{N}}_0\wedge R\in V\right)\right)\to \left(\left\{1\right\}\subseteq {\mathbb{N}}_0\vee Z\subseteq {\mathbb{N}}_0\right)$$
92		inss	$$⊢\left(\left\{1\right\}\subseteq {\mathbb{N}}_0\vee Z\subseteq {\mathbb{N}}_0\right)\to \left\{1\right\}\cap Z\subseteq {\mathbb{N}}_0$$
93	91 92	syl	$$⊢\left(0\in Z\wedge \left(Z\subseteq {\mathbb{N}}_0\wedge R\in V\right)\right)\to \left\{1\right\}\cap Z\subseteq {\mathbb{N}}_0$$
94	93	sseld	$$⊢\left(0\in Z\wedge \left(Z\subseteq {\mathbb{N}}_0\wedge R\in V\right)\right)\to \left(x\in \left(\left\{1\right\}\cap Z\right)\to x\in {\mathbb{N}}_0\right)$$
95	94	imim1d	$$⊢\left(0\in Z\wedge \left(Z\subseteq {\mathbb{N}}_0\wedge R\in V\right)\right)\to \left(\left(x\in {\mathbb{N}}_0\to \mathrm{dom}\left(R{\uparrow }_{r}x\right)\subseteq \mathrm{dom}R\cup \mathrm{ran}R\right)\to \left(x\in \left(\left\{1\right\}\cap Z\right)\to \mathrm{dom}\left(R{\uparrow }_{r}x\right)\subseteq \mathrm{dom}R\cup \mathrm{ran}R\right)\right)$$
96	95	ralimdv2	$$⊢\left(0\in Z\wedge \left(Z\subseteq {\mathbb{N}}_0\wedge R\in V\right)\right)\to \left(\forall x\in {\mathbb{N}}_0\mathrm{dom}\left(R{\uparrow }_{r}x\right)\subseteq \mathrm{dom}R\cup \mathrm{ran}R\to \forall x\in \left(\left\{1\right\}\cap Z\right)\mathrm{dom}\left(R{\uparrow }_{r}x\right)\subseteq \mathrm{dom}R\cup \mathrm{ran}R\right)$$
97	89 96	mpd	$$⊢\left(0\in Z\wedge \left(Z\subseteq {\mathbb{N}}_0\wedge R\in V\right)\right)\to \forall x\in \left(\left\{1\right\}\cap Z\right)\mathrm{dom}\left(R{\uparrow }_{r}x\right)\subseteq \mathrm{dom}R\cup \mathrm{ran}R$$
98		iunss	$$⊢\bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\subseteq \mathrm{dom}R\cup \mathrm{ran}R\leftrightarrow \forall x\in \left(\left\{1\right\}\cap Z\right)\mathrm{dom}\left(R{\uparrow }_{r}x\right)\subseteq \mathrm{dom}R\cup \mathrm{ran}R$$
99	97 98	sylibr	$$⊢\left(0\in Z\wedge \left(Z\subseteq {\mathbb{N}}_0\wedge R\in V\right)\right)\to \bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\subseteq \mathrm{dom}R\cup \mathrm{ran}R$$
100		relexprng	$$⊢\left(x\in {\mathbb{N}}_0\wedge R\in V\right)\to \mathrm{ran}\left(R{\uparrow }_{r}x\right)\subseteq \mathrm{dom}R\cup \mathrm{ran}R$$
101	100	expcom	$$⊢R\in V\to \left(x\in {\mathbb{N}}_0\to \mathrm{ran}\left(R{\uparrow }_{r}x\right)\subseteq \mathrm{dom}R\cup \mathrm{ran}R\right)$$
102	101	ralrimiv	$$⊢R\in V\to \forall x\in {\mathbb{N}}_0\mathrm{ran}\left(R{\uparrow }_{r}x\right)\subseteq \mathrm{dom}R\cup \mathrm{ran}R$$
103	102	ad2antll	$$⊢\left(0\in Z\wedge \left(Z\subseteq {\mathbb{N}}_0\wedge R\in V\right)\right)\to \forall x\in {\mathbb{N}}_0\mathrm{ran}\left(R{\uparrow }_{r}x\right)\subseteq \mathrm{dom}R\cup \mathrm{ran}R$$
104	94	imim1d	$$⊢\left(0\in Z\wedge \left(Z\subseteq {\mathbb{N}}_0\wedge R\in V\right)\right)\to \left(\left(x\in {\mathbb{N}}_0\to \mathrm{ran}\left(R{\uparrow }_{r}x\right)\subseteq \mathrm{dom}R\cup \mathrm{ran}R\right)\to \left(x\in \left(\left\{1\right\}\cap Z\right)\to \mathrm{ran}\left(R{\uparrow }_{r}x\right)\subseteq \mathrm{dom}R\cup \mathrm{ran}R\right)\right)$$
105	104	ralimdv2	$$⊢\left(0\in Z\wedge \left(Z\subseteq {\mathbb{N}}_0\wedge R\in V\right)\right)\to \left(\forall x\in {\mathbb{N}}_0\mathrm{ran}\left(R{\uparrow }_{r}x\right)\subseteq \mathrm{dom}R\cup \mathrm{ran}R\to \forall x\in \left(\left\{1\right\}\cap Z\right)\mathrm{ran}\left(R{\uparrow }_{r}x\right)\subseteq \mathrm{dom}R\cup \mathrm{ran}R\right)$$
106	103 105	mpd	$$⊢\left(0\in Z\wedge \left(Z\subseteq {\mathbb{N}}_0\wedge R\in V\right)\right)\to \forall x\in \left(\left\{1\right\}\cap Z\right)\mathrm{ran}\left(R{\uparrow }_{r}x\right)\subseteq \mathrm{dom}R\cup \mathrm{ran}R$$
107		iunss	$$⊢\bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\subseteq \mathrm{dom}R\cup \mathrm{ran}R\leftrightarrow \forall x\in \left(\left\{1\right\}\cap Z\right)\mathrm{ran}\left(R{\uparrow }_{r}x\right)\subseteq \mathrm{dom}R\cup \mathrm{ran}R$$
108	106 107	sylibr	$$⊢\left(0\in Z\wedge \left(Z\subseteq {\mathbb{N}}_0\wedge R\in V\right)\right)\to \bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\subseteq \mathrm{dom}R\cup \mathrm{ran}R$$
109	99 108	unssd	$$⊢\left(0\in Z\wedge \left(Z\subseteq {\mathbb{N}}_0\wedge R\in V\right)\right)\to \bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\subseteq \mathrm{dom}R\cup \mathrm{ran}R$$
110		ssequn2	$$⊢\bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\subseteq \mathrm{dom}R\cup \mathrm{ran}R\leftrightarrow \left(\mathrm{dom}R\cup \mathrm{ran}R\right)\cup \left(\bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\right)=\mathrm{dom}R\cup \mathrm{ran}R$$
111	109 110	sylib	$$⊢\left(0\in Z\wedge \left(Z\subseteq {\mathbb{N}}_0\wedge R\in V\right)\right)\to \left(\mathrm{dom}R\cup \mathrm{ran}R\right)\cup \left(\bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\right)=\mathrm{dom}R\cup \mathrm{ran}R$$
112	85 111	eqtrd	$$⊢\left(0\in Z\wedge \left(Z\subseteq {\mathbb{N}}_0\wedge R\in V\right)\right)\to \left(\bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\right)\cup \left(\bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\right)=\mathrm{dom}R\cup \mathrm{ran}R$$
113	112	ex	$$⊢0\in Z\to \left(\left(Z\subseteq {\mathbb{N}}_0\wedge R\in V\right)\to \left(\bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\right)\cup \left(\bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\right)=\mathrm{dom}R\cup \mathrm{ran}R\right)$$
114		simpl	$$⊢\left(1\in Z\wedge \left(Z\subseteq {\mathbb{N}}_0\wedge R\in V\right)\right)\to 1\in Z$$
115	114	snssd	$$⊢\left(1\in Z\wedge \left(Z\subseteq {\mathbb{N}}_0\wedge R\in V\right)\right)\to \left\{1\right\}\subseteq Z$$
116		df-ss	$$⊢\left\{1\right\}\subseteq Z\leftrightarrow \left\{1\right\}\cap Z=\left\{1\right\}$$
117	115 116	sylib	$$⊢\left(1\in Z\wedge \left(Z\subseteq {\mathbb{N}}_0\wedge R\in V\right)\right)\to \left\{1\right\}\cap Z=\left\{1\right\}$$
118	117	iuneq1d	$$⊢\left(1\in Z\wedge \left(Z\subseteq {\mathbb{N}}_0\wedge R\in V\right)\right)\to \bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)=\bigcup _{x\in \left\{1\right\}}\mathrm{dom}\left(R{\uparrow }_{r}x\right)$$
119		1ex	$$⊢1\in \mathrm{V}$$
120		oveq2	$$⊢x=1\to R{\uparrow }_{r}x=R{\uparrow }_{r}1$$
121	120	dmeqd	$$⊢x=1\to \mathrm{dom}\left(R{\uparrow }_{r}x\right)=\mathrm{dom}\left(R{\uparrow }_{r}1\right)$$
122	119 121	iunxsn	$$⊢\bigcup _{x\in \left\{1\right\}}\mathrm{dom}\left(R{\uparrow }_{r}x\right)=\mathrm{dom}\left(R{\uparrow }_{r}1\right)$$
123	118 122	eqtrdi	$$⊢\left(1\in Z\wedge \left(Z\subseteq {\mathbb{N}}_0\wedge R\in V\right)\right)\to \bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)=\mathrm{dom}\left(R{\uparrow }_{r}1\right)$$
124		relexp1g	$$⊢R\in V\to R{\uparrow }_{r}1=R$$
125	124	ad2antll	$$⊢\left(1\in Z\wedge \left(Z\subseteq {\mathbb{N}}_0\wedge R\in V\right)\right)\to R{\uparrow }_{r}1=R$$
126	125	dmeqd	$$⊢\left(1\in Z\wedge \left(Z\subseteq {\mathbb{N}}_0\wedge R\in V\right)\right)\to \mathrm{dom}\left(R{\uparrow }_{r}1\right)=\mathrm{dom}R$$
127	123 126	eqtrd	$$⊢\left(1\in Z\wedge \left(Z\subseteq {\mathbb{N}}_0\wedge R\in V\right)\right)\to \bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)=\mathrm{dom}R$$
128	117	iuneq1d	$$⊢\left(1\in Z\wedge \left(Z\subseteq {\mathbb{N}}_0\wedge R\in V\right)\right)\to \bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)=\bigcup _{x\in \left\{1\right\}}\mathrm{ran}\left(R{\uparrow }_{r}x\right)$$
129	120	rneqd	$$⊢x=1\to \mathrm{ran}\left(R{\uparrow }_{r}x\right)=\mathrm{ran}\left(R{\uparrow }_{r}1\right)$$
130	119 129	iunxsn	$$⊢\bigcup _{x\in \left\{1\right\}}\mathrm{ran}\left(R{\uparrow }_{r}x\right)=\mathrm{ran}\left(R{\uparrow }_{r}1\right)$$
131	128 130	eqtrdi	$$⊢\left(1\in Z\wedge \left(Z\subseteq {\mathbb{N}}_0\wedge R\in V\right)\right)\to \bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)=\mathrm{ran}\left(R{\uparrow }_{r}1\right)$$
132	125	rneqd	$$⊢\left(1\in Z\wedge \left(Z\subseteq {\mathbb{N}}_0\wedge R\in V\right)\right)\to \mathrm{ran}\left(R{\uparrow }_{r}1\right)=\mathrm{ran}R$$
133	131 132	eqtrd	$$⊢\left(1\in Z\wedge \left(Z\subseteq {\mathbb{N}}_0\wedge R\in V\right)\right)\to \bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)=\mathrm{ran}R$$
134	127 133	uneq12d	$$⊢\left(1\in Z\wedge \left(Z\subseteq {\mathbb{N}}_0\wedge R\in V\right)\right)\to \bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)=\mathrm{dom}R\cup \mathrm{ran}R$$
135	134	uneq2d	$$⊢\left(1\in Z\wedge \left(Z\subseteq {\mathbb{N}}_0\wedge R\in V\right)\right)\to \left(\bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\right)\cup \left(\bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\right)=\left(\bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\right)\cup \left(\mathrm{dom}R\cup \mathrm{ran}R\right)$$
136	88	ad2antll	$$⊢\left(1\in Z\wedge \left(Z\subseteq {\mathbb{N}}_0\wedge R\in V\right)\right)\to \forall x\in {\mathbb{N}}_0\mathrm{dom}\left(R{\uparrow }_{r}x\right)\subseteq \mathrm{dom}R\cup \mathrm{ran}R$$
137		olc	$$⊢Z\subseteq {\mathbb{N}}_0\to \left(\left\{0\right\}\subseteq {\mathbb{N}}_0\vee Z\subseteq {\mathbb{N}}_0\right)$$
138	137	ad2antrl	$$⊢\left(1\in Z\wedge \left(Z\subseteq {\mathbb{N}}_0\wedge R\in V\right)\right)\to \left(\left\{0\right\}\subseteq {\mathbb{N}}_0\vee Z\subseteq {\mathbb{N}}_0\right)$$
139		inss	$$⊢\left(\left\{0\right\}\subseteq {\mathbb{N}}_0\vee Z\subseteq {\mathbb{N}}_0\right)\to \left\{0\right\}\cap Z\subseteq {\mathbb{N}}_0$$
140	138 139	syl	$$⊢\left(1\in Z\wedge \left(Z\subseteq {\mathbb{N}}_0\wedge R\in V\right)\right)\to \left\{0\right\}\cap Z\subseteq {\mathbb{N}}_0$$
141	140	sseld	$$⊢\left(1\in Z\wedge \left(Z\subseteq {\mathbb{N}}_0\wedge R\in V\right)\right)\to \left(x\in \left(\left\{0\right\}\cap Z\right)\to x\in {\mathbb{N}}_0\right)$$
142	141	imim1d	$$⊢\left(1\in Z\wedge \left(Z\subseteq {\mathbb{N}}_0\wedge R\in V\right)\right)\to \left(\left(x\in {\mathbb{N}}_0\to \mathrm{dom}\left(R{\uparrow }_{r}x\right)\subseteq \mathrm{dom}R\cup \mathrm{ran}R\right)\to \left(x\in \left(\left\{0\right\}\cap Z\right)\to \mathrm{dom}\left(R{\uparrow }_{r}x\right)\subseteq \mathrm{dom}R\cup \mathrm{ran}R\right)\right)$$
143	142	ralimdv2	$$⊢\left(1\in Z\wedge \left(Z\subseteq {\mathbb{N}}_0\wedge R\in V\right)\right)\to \left(\forall x\in {\mathbb{N}}_0\mathrm{dom}\left(R{\uparrow }_{r}x\right)\subseteq \mathrm{dom}R\cup \mathrm{ran}R\to \forall x\in \left(\left\{0\right\}\cap Z\right)\mathrm{dom}\left(R{\uparrow }_{r}x\right)\subseteq \mathrm{dom}R\cup \mathrm{ran}R\right)$$
144	136 143	mpd	$$⊢\left(1\in Z\wedge \left(Z\subseteq {\mathbb{N}}_0\wedge R\in V\right)\right)\to \forall x\in \left(\left\{0\right\}\cap Z\right)\mathrm{dom}\left(R{\uparrow }_{r}x\right)\subseteq \mathrm{dom}R\cup \mathrm{ran}R$$
145		iunss	$$⊢\bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\subseteq \mathrm{dom}R\cup \mathrm{ran}R\leftrightarrow \forall x\in \left(\left\{0\right\}\cap Z\right)\mathrm{dom}\left(R{\uparrow }_{r}x\right)\subseteq \mathrm{dom}R\cup \mathrm{ran}R$$
146	144 145	sylibr	$$⊢\left(1\in Z\wedge \left(Z\subseteq {\mathbb{N}}_0\wedge R\in V\right)\right)\to \bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\subseteq \mathrm{dom}R\cup \mathrm{ran}R$$
147	102	ad2antll	$$⊢\left(1\in Z\wedge \left(Z\subseteq {\mathbb{N}}_0\wedge R\in V\right)\right)\to \forall x\in {\mathbb{N}}_0\mathrm{ran}\left(R{\uparrow }_{r}x\right)\subseteq \mathrm{dom}R\cup \mathrm{ran}R$$
148	141	imim1d	$$⊢\left(1\in Z\wedge \left(Z\subseteq {\mathbb{N}}_0\wedge R\in V\right)\right)\to \left(\left(x\in {\mathbb{N}}_0\to \mathrm{ran}\left(R{\uparrow }_{r}x\right)\subseteq \mathrm{dom}R\cup \mathrm{ran}R\right)\to \left(x\in \left(\left\{0\right\}\cap Z\right)\to \mathrm{ran}\left(R{\uparrow }_{r}x\right)\subseteq \mathrm{dom}R\cup \mathrm{ran}R\right)\right)$$
149	148	ralimdv2	$$⊢\left(1\in Z\wedge \left(Z\subseteq {\mathbb{N}}_0\wedge R\in V\right)\right)\to \left(\forall x\in {\mathbb{N}}_0\mathrm{ran}\left(R{\uparrow }_{r}x\right)\subseteq \mathrm{dom}R\cup \mathrm{ran}R\to \forall x\in \left(\left\{0\right\}\cap Z\right)\mathrm{ran}\left(R{\uparrow }_{r}x\right)\subseteq \mathrm{dom}R\cup \mathrm{ran}R\right)$$
150	147 149	mpd	$$⊢\left(1\in Z\wedge \left(Z\subseteq {\mathbb{N}}_0\wedge R\in V\right)\right)\to \forall x\in \left(\left\{0\right\}\cap Z\right)\mathrm{ran}\left(R{\uparrow }_{r}x\right)\subseteq \mathrm{dom}R\cup \mathrm{ran}R$$
151		iunss	$$⊢\bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\subseteq \mathrm{dom}R\cup \mathrm{ran}R\leftrightarrow \forall x\in \left(\left\{0\right\}\cap Z\right)\mathrm{ran}\left(R{\uparrow }_{r}x\right)\subseteq \mathrm{dom}R\cup \mathrm{ran}R$$
152	150 151	sylibr	$$⊢\left(1\in Z\wedge \left(Z\subseteq {\mathbb{N}}_0\wedge R\in V\right)\right)\to \bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\subseteq \mathrm{dom}R\cup \mathrm{ran}R$$
153	146 152	unssd	$$⊢\left(1\in Z\wedge \left(Z\subseteq {\mathbb{N}}_0\wedge R\in V\right)\right)\to \bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\subseteq \mathrm{dom}R\cup \mathrm{ran}R$$
154		ssequn1	$$⊢\bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\subseteq \mathrm{dom}R\cup \mathrm{ran}R\leftrightarrow \left(\bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\right)\cup \left(\mathrm{dom}R\cup \mathrm{ran}R\right)=\mathrm{dom}R\cup \mathrm{ran}R$$
155	153 154	sylib	$$⊢\left(1\in Z\wedge \left(Z\subseteq {\mathbb{N}}_0\wedge R\in V\right)\right)\to \left(\bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\right)\cup \left(\mathrm{dom}R\cup \mathrm{ran}R\right)=\mathrm{dom}R\cup \mathrm{ran}R$$
156	135 155	eqtrd	$$⊢\left(1\in Z\wedge \left(Z\subseteq {\mathbb{N}}_0\wedge R\in V\right)\right)\to \left(\bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\right)\cup \left(\bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\right)=\mathrm{dom}R\cup \mathrm{ran}R$$
157	156	ex	$$⊢1\in Z\to \left(\left(Z\subseteq {\mathbb{N}}_0\wedge R\in V\right)\to \left(\bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\right)\cup \left(\bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\right)=\mathrm{dom}R\cup \mathrm{ran}R\right)$$
158	113 157	jaoi	$$⊢\left(0\in Z\vee 1\in Z\right)\to \left(\left(Z\subseteq {\mathbb{N}}_0\wedge R\in V\right)\to \left(\bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\right)\cup \left(\bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\right)=\mathrm{dom}R\cup \mathrm{ran}R\right)$$
159	57 158	syl	$$⊢\left\{0,1\right\}\cap Z\ne \varnothing \to \left(\left(Z\subseteq {\mathbb{N}}_0\wedge R\in V\right)\to \left(\bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\right)\cup \left(\bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\right)=\mathrm{dom}R\cup \mathrm{ran}R\right)$$
160	159	3impib	$$⊢\left(\left\{0,1\right\}\cap Z\ne \varnothing \wedge Z\subseteq {\mathbb{N}}_0\wedge R\in V\right)\to \left(\bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\right)\cup \left(\bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\right)=\mathrm{dom}R\cup \mathrm{ran}R$$
161	160	3com13	$$⊢\left(R\in V\wedge Z\subseteq {\mathbb{N}}_0\wedge \left\{0,1\right\}\cap Z\ne \varnothing \right)\to \left(\bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\right)\cup \left(\bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\right)=\mathrm{dom}R\cup \mathrm{ran}R$$
162	161	uneq1d	$$⊢\left(R\in V\wedge Z\subseteq {\mathbb{N}}_0\wedge \left\{0,1\right\}\cap Z\ne \varnothing \right)\to \left(\left(\bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\right)\cup \left(\bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\right)\right)\cup \left(\bigcup _{x\in Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\right)=\left(\mathrm{dom}R\cup \mathrm{ran}R\right)\cup \left(\bigcup _{x\in Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\right)$$
163	88	adantr	$$⊢\left(R\in V\wedge Z\subseteq {\mathbb{N}}_0\right)\to \forall x\in {\mathbb{N}}_0\mathrm{dom}\left(R{\uparrow }_{r}x\right)\subseteq \mathrm{dom}R\cup \mathrm{ran}R$$
164		ssel	$$⊢Z\subseteq {\mathbb{N}}_0\to \left(x\in Z\to x\in {\mathbb{N}}_0\right)$$
165	164	adantl	$$⊢\left(R\in V\wedge Z\subseteq {\mathbb{N}}_0\right)\to \left(x\in Z\to x\in {\mathbb{N}}_0\right)$$
166	165	imim1d	$$⊢\left(R\in V\wedge Z\subseteq {\mathbb{N}}_0\right)\to \left(\left(x\in {\mathbb{N}}_0\to \mathrm{dom}\left(R{\uparrow }_{r}x\right)\subseteq \mathrm{dom}R\cup \mathrm{ran}R\right)\to \left(x\in Z\to \mathrm{dom}\left(R{\uparrow }_{r}x\right)\subseteq \mathrm{dom}R\cup \mathrm{ran}R\right)\right)$$
167	166	ralimdv2	$$⊢\left(R\in V\wedge Z\subseteq {\mathbb{N}}_0\right)\to \left(\forall x\in {\mathbb{N}}_0\mathrm{dom}\left(R{\uparrow }_{r}x\right)\subseteq \mathrm{dom}R\cup \mathrm{ran}R\to \forall x\in Z\mathrm{dom}\left(R{\uparrow }_{r}x\right)\subseteq \mathrm{dom}R\cup \mathrm{ran}R\right)$$
168	163 167	mpd	$$⊢\left(R\in V\wedge Z\subseteq {\mathbb{N}}_0\right)\to \forall x\in Z\mathrm{dom}\left(R{\uparrow }_{r}x\right)\subseteq \mathrm{dom}R\cup \mathrm{ran}R$$
169		iunss	$$⊢\bigcup _{x\in Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\subseteq \mathrm{dom}R\cup \mathrm{ran}R\leftrightarrow \forall x\in Z\mathrm{dom}\left(R{\uparrow }_{r}x\right)\subseteq \mathrm{dom}R\cup \mathrm{ran}R$$
170	168 169	sylibr	$$⊢\left(R\in V\wedge Z\subseteq {\mathbb{N}}_0\right)\to \bigcup _{x\in Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\subseteq \mathrm{dom}R\cup \mathrm{ran}R$$
171	102	adantr	$$⊢\left(R\in V\wedge Z\subseteq {\mathbb{N}}_0\right)\to \forall x\in {\mathbb{N}}_0\mathrm{ran}\left(R{\uparrow }_{r}x\right)\subseteq \mathrm{dom}R\cup \mathrm{ran}R$$
172	165	imim1d	$$⊢\left(R\in V\wedge Z\subseteq {\mathbb{N}}_0\right)\to \left(\left(x\in {\mathbb{N}}_0\to \mathrm{ran}\left(R{\uparrow }_{r}x\right)\subseteq \mathrm{dom}R\cup \mathrm{ran}R\right)\to \left(x\in Z\to \mathrm{ran}\left(R{\uparrow }_{r}x\right)\subseteq \mathrm{dom}R\cup \mathrm{ran}R\right)\right)$$
173	172	ralimdv2	$$⊢\left(R\in V\wedge Z\subseteq {\mathbb{N}}_0\right)\to \left(\forall x\in {\mathbb{N}}_0\mathrm{ran}\left(R{\uparrow }_{r}x\right)\subseteq \mathrm{dom}R\cup \mathrm{ran}R\to \forall x\in Z\mathrm{ran}\left(R{\uparrow }_{r}x\right)\subseteq \mathrm{dom}R\cup \mathrm{ran}R\right)$$
174	171 173	mpd	$$⊢\left(R\in V\wedge Z\subseteq {\mathbb{N}}_0\right)\to \forall x\in Z\mathrm{ran}\left(R{\uparrow }_{r}x\right)\subseteq \mathrm{dom}R\cup \mathrm{ran}R$$
175		iunss	$$⊢\bigcup _{x\in Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\subseteq \mathrm{dom}R\cup \mathrm{ran}R\leftrightarrow \forall x\in Z\mathrm{ran}\left(R{\uparrow }_{r}x\right)\subseteq \mathrm{dom}R\cup \mathrm{ran}R$$
176	174 175	sylibr	$$⊢\left(R\in V\wedge Z\subseteq {\mathbb{N}}_0\right)\to \bigcup _{x\in Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\subseteq \mathrm{dom}R\cup \mathrm{ran}R$$
177	170 176	unssd	$$⊢\left(R\in V\wedge Z\subseteq {\mathbb{N}}_0\right)\to \bigcup _{x\in Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\subseteq \mathrm{dom}R\cup \mathrm{ran}R$$
178	177	3adant3	$$⊢\left(R\in V\wedge Z\subseteq {\mathbb{N}}_0\wedge \left\{0,1\right\}\cap Z\ne \varnothing \right)\to \bigcup _{x\in Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\subseteq \mathrm{dom}R\cup \mathrm{ran}R$$
179		ssequn2	$$⊢\bigcup _{x\in Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\subseteq \mathrm{dom}R\cup \mathrm{ran}R\leftrightarrow \left(\mathrm{dom}R\cup \mathrm{ran}R\right)\cup \left(\bigcup _{x\in Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\right)=\mathrm{dom}R\cup \mathrm{ran}R$$
180	178 179	sylib	$$⊢\left(R\in V\wedge Z\subseteq {\mathbb{N}}_0\wedge \left\{0,1\right\}\cap Z\ne \varnothing \right)\to \left(\mathrm{dom}R\cup \mathrm{ran}R\right)\cup \left(\bigcup _{x\in Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\right)=\mathrm{dom}R\cup \mathrm{ran}R$$
181	162 180	eqtrd	$$⊢\left(R\in V\wedge Z\subseteq {\mathbb{N}}_0\wedge \left\{0,1\right\}\cap Z\ne \varnothing \right)\to \left(\left(\bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in \left\{0\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\right)\cup \left(\bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in \left\{1\right\}\cap Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\right)\right)\cup \left(\bigcup _{x\in Z}\mathrm{dom}\left(R{\uparrow }_{r}x\right)\cup \bigcup _{x\in Z}\mathrm{ran}\left(R{\uparrow }_{r}x\right)\right)=\mathrm{dom}R\cup \mathrm{ran}R$$
182	35 181	syl5eq	$$⊢\left(R\in V\wedge Z\subseteq {\mathbb{N}}_0\wedge \left\{0,1\right\}\cap Z\ne \varnothing \right)\to \mathrm{dom}\bigcup _{x\in \left(\left(\left\{0\right\}\cap Z\right)\cup \left(\left\{1\right\}\cap Z\right)\right)\cup Z}\left(R{\uparrow }_{r}x\right)\cup \mathrm{ran}\bigcup _{x\in \left(\left(\left\{0\right\}\cap Z\right)\cup \left(\left\{1\right\}\cap Z\right)\right)\cup Z}\left(R{\uparrow }_{r}x\right)=\mathrm{dom}R\cup \mathrm{ran}R$$
183		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
184	183	ssex	$$⊢Z\subseteq {\mathbb{N}}_0\to Z\in \mathrm{V}$$
185		incom	$$⊢Z\cap \left\{0\right\}=\left\{0\right\}\cap Z$$
186		inex1g	$$⊢Z\in \mathrm{V}\to Z\cap \left\{0\right\}\in \mathrm{V}$$
187	185 186	eqeltrrid	$$⊢Z\in \mathrm{V}\to \left\{0\right\}\cap Z\in \mathrm{V}$$
188		incom	$$⊢Z\cap \left\{1\right\}=\left\{1\right\}\cap Z$$
189		inex1g	$$⊢Z\in \mathrm{V}\to Z\cap \left\{1\right\}\in \mathrm{V}$$
190	188 189	eqeltrrid	$$⊢Z\in \mathrm{V}\to \left\{1\right\}\cap Z\in \mathrm{V}$$
191		unexg	$$⊢\left(\left\{0\right\}\cap Z\in \mathrm{V}\wedge \left\{1\right\}\cap Z\in \mathrm{V}\right)\to \left(\left\{0\right\}\cap Z\right)\cup \left(\left\{1\right\}\cap Z\right)\in \mathrm{V}$$
192	187 190 191	syl2anc	$$⊢Z\in \mathrm{V}\to \left(\left\{0\right\}\cap Z\right)\cup \left(\left\{1\right\}\cap Z\right)\in \mathrm{V}$$
193		unexg	$$⊢\left(\left(\left\{0\right\}\cap Z\right)\cup \left(\left\{1\right\}\cap Z\right)\in \mathrm{V}\wedge Z\in \mathrm{V}\right)\to \left(\left(\left\{0\right\}\cap Z\right)\cup \left(\left\{1\right\}\cap Z\right)\right)\cup Z\in \mathrm{V}$$
194	192 193	mpancom	$$⊢Z\in \mathrm{V}\to \left(\left(\left\{0\right\}\cap Z\right)\cup \left(\left\{1\right\}\cap Z\right)\right)\cup Z\in \mathrm{V}$$
195		ovex	$$⊢R{\uparrow }_{r}x\in \mathrm{V}$$
196	195	rgenw	$$⊢\forall x\in \left(\left(\left(\left\{0\right\}\cap Z\right)\cup \left(\left\{1\right\}\cap Z\right)\right)\cup Z\right)R{\uparrow }_{r}x\in \mathrm{V}$$
197		iunexg	$$⊢\left(\left(\left(\left\{0\right\}\cap Z\right)\cup \left(\left\{1\right\}\cap Z\right)\right)\cup Z\in \mathrm{V}\wedge \forall x\in \left(\left(\left(\left\{0\right\}\cap Z\right)\cup \left(\left\{1\right\}\cap Z\right)\right)\cup Z\right)R{\uparrow }_{r}x\in \mathrm{V}\right)\to \bigcup _{x\in \left(\left(\left\{0\right\}\cap Z\right)\cup \left(\left\{1\right\}\cap Z\right)\right)\cup Z}\left(R{\uparrow }_{r}x\right)\in \mathrm{V}$$
198	194 196 197	sylancl	$$⊢Z\in \mathrm{V}\to \bigcup _{x\in \left(\left(\left\{0\right\}\cap Z\right)\cup \left(\left\{1\right\}\cap Z\right)\right)\cup Z}\left(R{\uparrow }_{r}x\right)\in \mathrm{V}$$
199	184 198	syl	$$⊢Z\subseteq {\mathbb{N}}_0\to \bigcup _{x\in \left(\left(\left\{0\right\}\cap Z\right)\cup \left(\left\{1\right\}\cap Z\right)\right)\cup Z}\left(R{\uparrow }_{r}x\right)\in \mathrm{V}$$
200	199	3ad2ant2	$$⊢\left(R\in V\wedge Z\subseteq {\mathbb{N}}_0\wedge \left\{0,1\right\}\cap Z\ne \varnothing \right)\to \bigcup _{x\in \left(\left(\left\{0\right\}\cap Z\right)\cup \left(\left\{1\right\}\cap Z\right)\right)\cup Z}\left(R{\uparrow }_{r}x\right)\in \mathrm{V}$$
201		simp1	$$⊢\left(R\in V\wedge Z\subseteq {\mathbb{N}}_0\wedge \left\{0,1\right\}\cap Z\ne \varnothing \right)\to R\in V$$
202		relexp0eq	$$⊢\left(\bigcup _{x\in \left(\left(\left\{0\right\}\cap Z\right)\cup \left(\left\{1\right\}\cap Z\right)\right)\cup Z}\left(R{\uparrow }_{r}x\right)\in \mathrm{V}\wedge R\in V\right)\to \left(\mathrm{dom}\bigcup _{x\in \left(\left(\left\{0\right\}\cap Z\right)\cup \left(\left\{1\right\}\cap Z\right)\right)\cup Z}\left(R{\uparrow }_{r}x\right)\cup \mathrm{ran}\bigcup _{x\in \left(\left(\left\{0\right\}\cap Z\right)\cup \left(\left\{1\right\}\cap Z\right)\right)\cup Z}\left(R{\uparrow }_{r}x\right)=\mathrm{dom}R\cup \mathrm{ran}R\leftrightarrow \bigcup _{x\in \left(\left(\left\{0\right\}\cap Z\right)\cup \left(\left\{1\right\}\cap Z\right)\right)\cup Z}\left(R{\uparrow }_{r}x\right){\uparrow }_{r}0=R{\uparrow }_{r}0\right)$$
203	200 201 202	syl2anc	$$⊢\left(R\in V\wedge Z\subseteq {\mathbb{N}}_0\wedge \left\{0,1\right\}\cap Z\ne \varnothing \right)\to \left(\mathrm{dom}\bigcup _{x\in \left(\left(\left\{0\right\}\cap Z\right)\cup \left(\left\{1\right\}\cap Z\right)\right)\cup Z}\left(R{\uparrow }_{r}x\right)\cup \mathrm{ran}\bigcup _{x\in \left(\left(\left\{0\right\}\cap Z\right)\cup \left(\left\{1\right\}\cap Z\right)\right)\cup Z}\left(R{\uparrow }_{r}x\right)=\mathrm{dom}R\cup \mathrm{ran}R\leftrightarrow \bigcup _{x\in \left(\left(\left\{0\right\}\cap Z\right)\cup \left(\left\{1\right\}\cap Z\right)\right)\cup Z}\left(R{\uparrow }_{r}x\right){\uparrow }_{r}0=R{\uparrow }_{r}0\right)$$
204	182 203	mpbid	$$⊢\left(R\in V\wedge Z\subseteq {\mathbb{N}}_0\wedge \left\{0,1\right\}\cap Z\ne \varnothing \right)\to \bigcup _{x\in \left(\left(\left\{0\right\}\cap Z\right)\cup \left(\left\{1\right\}\cap Z\right)\right)\cup Z}\left(R{\uparrow }_{r}x\right){\uparrow }_{r}0=R{\uparrow }_{r}0$$
205	12 204	syl5eq	$$⊢\left(R\in V\wedge Z\subseteq {\mathbb{N}}_0\wedge \left\{0,1\right\}\cap Z\ne \varnothing \right)\to \bigcup _{x\in Z}\left(R{\uparrow }_{r}x\right){\uparrow }_{r}0=R{\uparrow }_{r}0$$