Theorem fvmptiunrelexplb0da

Description: If the indexed union ranges over the zeroth power of the relation, then a restriction of the identity relation is a subset of the appliction of the function to the relation. (Contributed by RP, 22-Jul-2020)

	Ref	Expression
Hypotheses	fvmptiunrelexplb0da.c	$$⊢C=\left(r\in \mathrm{V}⟼\bigcup _{n\in N}\left(r{\uparrow }_{r}n\right)\right)$$
	fvmptiunrelexplb0da.r	$$⊢\phi \to R\in \mathrm{V}$$
	fvmptiunrelexplb0da.n	$$⊢\phi \to N\in \mathrm{V}$$
	fvmptiunrelexplb0da.rel	$$⊢\phi \to \mathrm{Rel}R$$
	fvmptiunrelexplb0da.0	$$⊢\phi \to 0\in N$$
Assertion	fvmptiunrelexplb0da	$$⊢\phi \to {\mathrm{I}\upharpoonright }_{\bigcup \bigcup R}\subseteq C\left(R\right)$$

Proof

Step	Hyp	Ref	Expression
1		fvmptiunrelexplb0da.c	$$⊢C=\left(r\in \mathrm{V}⟼\bigcup _{n\in N}\left(r{\uparrow }_{r}n\right)\right)$$
2		fvmptiunrelexplb0da.r	$$⊢\phi \to R\in \mathrm{V}$$
3		fvmptiunrelexplb0da.n	$$⊢\phi \to N\in \mathrm{V}$$
4		fvmptiunrelexplb0da.rel	$$⊢\phi \to \mathrm{Rel}R$$
5		fvmptiunrelexplb0da.0	$$⊢\phi \to 0\in N$$
6		relfld	$$⊢\mathrm{Rel}R\to \bigcup \bigcup R=\mathrm{dom}R\cup \mathrm{ran}R$$
7	4 6	syl	$$⊢\phi \to \bigcup \bigcup R=\mathrm{dom}R\cup \mathrm{ran}R$$
8	7	reseq2d	$$⊢\phi \to {\mathrm{I}\upharpoonright }_{\bigcup \bigcup R}={\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}R\cup \mathrm{ran}R\right)}$$
9	1 2 3 5	fvmptiunrelexplb0d	$$⊢\phi \to {\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}R\cup \mathrm{ran}R\right)}\subseteq C\left(R\right)$$
10	8 9	eqsstrd	$$⊢\phi \to {\mathrm{I}\upharpoonright }_{\bigcup \bigcup R}\subseteq C\left(R\right)$$