Theorem qtopres

Description: The quotient topology is unaffected by restriction to the base set. This property makes it slightly more convenient to use, since we don't have to require that F be a function with domain X . (Contributed by Mario Carneiro, 23-Mar-2015)

	Ref	Expression
Hypothesis	qtopval.1	$$⊢X=\bigcup J$$
Assertion	qtopres	$$⊢F\in V\to J\mathrm{qTop}F=J\mathrm{qTop}\left({F\upharpoonright }_X\right)$$

Proof

Step	Hyp	Ref	Expression
1		qtopval.1	$$⊢X=\bigcup J$$
2		resima	$$⊢\left({F\upharpoonright }_X\right)\left[X\right]=F\left[X\right]$$
3	2	pweqi	$$⊢𝒫\left({F\upharpoonright }_X\right)\left[X\right]=𝒫F\left[X\right]$$
4	3	rabeqi	$$⊢\left\{s\in 𝒫\left({F\upharpoonright }_X\right)\left[X\right]|{\left({F\upharpoonright }_X\right)}^{-1}\left[s\right]\cap X\in J\right\}=\left\{s\in 𝒫F\left[X\right]|{\left({F\upharpoonright }_X\right)}^{-1}\left[s\right]\cap X\in J\right\}$$
5		residm	$$⊢{\left({F\upharpoonright }_X\right)\upharpoonright }_X={F\upharpoonright }_X$$
6	5	cnveqi	$$⊢{\left({\left({F\upharpoonright }_X\right)\upharpoonright }_X\right)}^{-1}={\left({F\upharpoonright }_X\right)}^{-1}$$
7	6	imaeq1i	$$⊢{\left({\left({F\upharpoonright }_X\right)\upharpoonright }_X\right)}^{-1}\left[s\right]={\left({F\upharpoonright }_X\right)}^{-1}\left[s\right]$$
8		cnvresima	$$⊢{\left({\left({F\upharpoonright }_X\right)\upharpoonright }_X\right)}^{-1}\left[s\right]={\left({F\upharpoonright }_X\right)}^{-1}\left[s\right]\cap X$$
9		cnvresima	$$⊢{\left({F\upharpoonright }_X\right)}^{-1}\left[s\right]=F^{-1}\left[s\right]\cap X$$
10	7 8 9	3eqtr3i	$$⊢{\left({F\upharpoonright }_X\right)}^{-1}\left[s\right]\cap X=F^{-1}\left[s\right]\cap X$$
11	10	eleq1i	$$⊢{\left({F\upharpoonright }_X\right)}^{-1}\left[s\right]\cap X\in J\leftrightarrow F^{-1}\left[s\right]\cap X\in J$$
12	11	rabbii	$$⊢\left\{s\in 𝒫F\left[X\right]|{\left({F\upharpoonright }_X\right)}^{-1}\left[s\right]\cap X\in J\right\}=\left\{s\in 𝒫F\left[X\right]|F^{-1}\left[s\right]\cap X\in J\right\}$$
13	4 12	eqtr2i	$$⊢\left\{s\in 𝒫F\left[X\right]|F^{-1}\left[s\right]\cap X\in J\right\}=\left\{s\in 𝒫\left({F\upharpoonright }_X\right)\left[X\right]|{\left({F\upharpoonright }_X\right)}^{-1}\left[s\right]\cap X\in J\right\}$$
14	1	qtopval	$$⊢\left(J\in \mathrm{V}\wedge F\in V\right)\to J\mathrm{qTop}F=\left\{s\in 𝒫F\left[X\right]|F^{-1}\left[s\right]\cap X\in J\right\}$$
15		resexg	$$⊢F\in V\to {F\upharpoonright }_X\in \mathrm{V}$$
16	1	qtopval	$$⊢\left(J\in \mathrm{V}\wedge {F\upharpoonright }_X\in \mathrm{V}\right)\to J\mathrm{qTop}\left({F\upharpoonright }_X\right)=\left\{s\in 𝒫\left({F\upharpoonright }_X\right)\left[X\right]|{\left({F\upharpoonright }_X\right)}^{-1}\left[s\right]\cap X\in J\right\}$$
17	15 16	sylan2	$$⊢\left(J\in \mathrm{V}\wedge F\in V\right)\to J\mathrm{qTop}\left({F\upharpoonright }_X\right)=\left\{s\in 𝒫\left({F\upharpoonright }_X\right)\left[X\right]|{\left({F\upharpoonright }_X\right)}^{-1}\left[s\right]\cap X\in J\right\}$$
18	13 14 17	3eqtr4a	$$⊢\left(J\in \mathrm{V}\wedge F\in V\right)\to J\mathrm{qTop}F=J\mathrm{qTop}\left({F\upharpoonright }_X\right)$$
19	18	expcom	$$⊢F\in V\to \left(J\in \mathrm{V}\to J\mathrm{qTop}F=J\mathrm{qTop}\left({F\upharpoonright }_X\right)\right)$$
20		df-qtop	$$⊢\mathrm{qTop}=\left(j\in \mathrm{V},f\in \mathrm{V}⟼\left\{s\in 𝒫f\left[\bigcup j\right]|f^{-1}\left[s\right]\cap \bigcup j\in j\right\}\right)$$
21	20	reldmmpo	$$⊢\mathrm{Rel}\mathrm{dom}\mathrm{qTop}$$
22	21	ovprc1	$$⊢\neg J\in \mathrm{V}\to J\mathrm{qTop}F=\varnothing$$
23	21	ovprc1	$$⊢\neg J\in \mathrm{V}\to J\mathrm{qTop}\left({F\upharpoonright }_X\right)=\varnothing$$
24	22 23	eqtr4d	$$⊢\neg J\in \mathrm{V}\to J\mathrm{qTop}F=J\mathrm{qTop}\left({F\upharpoonright }_X\right)$$
25	19 24	pm2.61d1	$$⊢F\in V\to J\mathrm{qTop}F=J\mathrm{qTop}\left({F\upharpoonright }_X\right)$$