Theorem orvcval4

Description: The value of the preimage mapping operator can be restricted to preimages in the base set of the topology. Cf. orvcval . (Contributed by Thierry Arnoux, 21-Jan-2017)

	Ref	Expression
Hypotheses	orvccel.1	$$⊢\phi \to S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$$
	orvccel.2	$$⊢\phi \to J\in \mathrm{Top}$$
	orvccel.3	$$⊢\phi \to X\in \left(S{\mathrm{MblFn}}_{\mu }𝛔\left(J\right)\right)$$
	orvccel.4	$$⊢\phi \to A\in V$$
Assertion	orvcval4	$$⊢\phi \to X{R}_{\mathrm{RV/c}}A=X^{-1}\left[\left\{y\in \bigcup J|yRA\right\}\right]$$

Proof

Step	Hyp	Ref	Expression
1		orvccel.1	$$⊢\phi \to S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$$
2		orvccel.2	$$⊢\phi \to J\in \mathrm{Top}$$
3		orvccel.3	$$⊢\phi \to X\in \left(S{\mathrm{MblFn}}_{\mu }𝛔\left(J\right)\right)$$
4		orvccel.4	$$⊢\phi \to A\in V$$
5	3	isanmbfm	$$⊢\phi \to X\in \bigcup \mathrm{ran}{\mathrm{MblFn}}_{\mu }$$
6	5	mbfmfun	$$⊢\phi \to \mathrm{Fun}X$$
7	2	sgsiga	$$⊢\phi \to 𝛔\left(J\right)\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$$
8	1 7 3	mbfmf	$$⊢\phi \to X:\bigcup S⟶\bigcup 𝛔\left(J\right)$$
9		elex	$$⊢J\in \mathrm{Top}\to J\in \mathrm{V}$$
10		unisg	$$⊢J\in \mathrm{V}\to \bigcup 𝛔\left(J\right)=\bigcup J$$
11	2 9 10	3syl	$$⊢\phi \to \bigcup 𝛔\left(J\right)=\bigcup J$$
12	11	feq3d	$$⊢\phi \to \left(X:\bigcup S⟶\bigcup 𝛔\left(J\right)\leftrightarrow X:\bigcup S⟶\bigcup J\right)$$
13	8 12	mpbid	$$⊢\phi \to X:\bigcup S⟶\bigcup J$$
14	13	frnd	$$⊢\phi \to \mathrm{ran}X\subseteq \bigcup J$$
15		fimacnvinrn2	$$⊢\left(\mathrm{Fun}X\wedge \mathrm{ran}X\subseteq \bigcup J\right)\to X^{-1}\left[\left\{y|yRA\right\}\right]=X^{-1}\left[\left\{y|yRA\right\}\cap \bigcup J\right]$$
16	6 14 15	syl2anc	$$⊢\phi \to X^{-1}\left[\left\{y|yRA\right\}\right]=X^{-1}\left[\left\{y|yRA\right\}\cap \bigcup J\right]$$
17	6 3 4	orvcval	$$⊢\phi \to X{R}_{\mathrm{RV/c}}A=X^{-1}\left[\left\{y|yRA\right\}\right]$$
18		dfrab2	$$⊢\left\{y\in \bigcup J|yRA\right\}=\left\{y|yRA\right\}\cap \bigcup J$$
19	18	a1i	$$⊢\phi \to \left\{y\in \bigcup J|yRA\right\}=\left\{y|yRA\right\}\cap \bigcup J$$
20	19	imaeq2d	$$⊢\phi \to X^{-1}\left[\left\{y\in \bigcup J|yRA\right\}\right]=X^{-1}\left[\left\{y|yRA\right\}\cap \bigcup J\right]$$
21	16 17 20	3eqtr4d	$$⊢\phi \to X{R}_{\mathrm{RV/c}}A=X^{-1}\left[\left\{y\in \bigcup J|yRA\right\}\right]$$