Theorem imastopn

Description: The topology of an image structure. (Contributed by Mario Carneiro, 27-Aug-2015)

	Ref	Expression
Hypotheses	imastps.u	$$⊢\phi \to U=F{“}_{𝑠}R$$
	imastps.v	$$⊢\phi \to V={\mathrm{Base}}_R$$
	imastps.f	$$⊢\phi \to F:V\underset{onto}{⟶}B$$
	imastopn.r	$$⊢\phi \to R\in W$$
	imastopn.j	$$⊢J=\mathrm{TopOpen}\left(R\right)$$
	imastopn.o	$$⊢O=\mathrm{TopOpen}\left(U\right)$$
Assertion	imastopn	$$⊢\phi \to O=J\mathrm{qTop}F$$

Proof

Step	Hyp	Ref	Expression
1		imastps.u	$$⊢\phi \to U=F{“}_{𝑠}R$$
2		imastps.v	$$⊢\phi \to V={\mathrm{Base}}_R$$
3		imastps.f	$$⊢\phi \to F:V\underset{onto}{⟶}B$$
4		imastopn.r	$$⊢\phi \to R\in W$$
5		imastopn.j	$$⊢J=\mathrm{TopOpen}\left(R\right)$$
6		imastopn.o	$$⊢O=\mathrm{TopOpen}\left(U\right)$$
7		eqid	$$⊢\mathrm{TopSet}\left(U\right)=\mathrm{TopSet}\left(U\right)$$
8	1 2 3 4 5 7	imastset	$$⊢\phi \to \mathrm{TopSet}\left(U\right)=J\mathrm{qTop}F$$
9	5	fvexi	$$⊢J\in \mathrm{V}$$
10		fofn	$$⊢F:V\underset{onto}{⟶}B\to FFnV$$
11	3 10	syl	$$⊢\phi \to FFnV$$
12		fvex	$$⊢{\mathrm{Base}}_R\in \mathrm{V}$$
13	2 12	eqeltrdi	$$⊢\phi \to V\in \mathrm{V}$$
14		fnex	$$⊢\left(FFnV\wedge V\in \mathrm{V}\right)\to F\in \mathrm{V}$$
15	11 13 14	syl2anc	$$⊢\phi \to F\in \mathrm{V}$$
16		eqid	$$⊢\bigcup J=\bigcup J$$
17	16	qtopval	$$⊢\left(J\in \mathrm{V}\wedge F\in \mathrm{V}\right)\to J\mathrm{qTop}F=\left\{x\in 𝒫F\left[\bigcup J\right]|F^{-1}\left[x\right]\cap \bigcup J\in J\right\}$$
18	9 15 17	sylancr	$$⊢\phi \to J\mathrm{qTop}F=\left\{x\in 𝒫F\left[\bigcup J\right]|F^{-1}\left[x\right]\cap \bigcup J\in J\right\}$$
19	8 18	eqtrd	$$⊢\phi \to \mathrm{TopSet}\left(U\right)=\left\{x\in 𝒫F\left[\bigcup J\right]|F^{-1}\left[x\right]\cap \bigcup J\in J\right\}$$
20		ssrab2	$$⊢\left\{x\in 𝒫F\left[\bigcup J\right]|F^{-1}\left[x\right]\cap \bigcup J\in J\right\}\subseteq 𝒫F\left[\bigcup J\right]$$
21		imassrn	$$⊢F\left[\bigcup J\right]\subseteq \mathrm{ran}F$$
22		forn	$$⊢F:V\underset{onto}{⟶}B\to \mathrm{ran}F=B$$
23	3 22	syl	$$⊢\phi \to \mathrm{ran}F=B$$
24	1 2 3 4	imasbas	$$⊢\phi \to B={\mathrm{Base}}_U$$
25	23 24	eqtrd	$$⊢\phi \to \mathrm{ran}F={\mathrm{Base}}_U$$
26	21 25	sseqtrid	$$⊢\phi \to F\left[\bigcup J\right]\subseteq {\mathrm{Base}}_U$$
27	26	sspwd	$$⊢\phi \to 𝒫F\left[\bigcup J\right]\subseteq 𝒫{\mathrm{Base}}_U$$
28	20 27	sstrid	$$⊢\phi \to \left\{x\in 𝒫F\left[\bigcup J\right]|F^{-1}\left[x\right]\cap \bigcup J\in J\right\}\subseteq 𝒫{\mathrm{Base}}_U$$
29	19 28	eqsstrd	$$⊢\phi \to \mathrm{TopSet}\left(U\right)\subseteq 𝒫{\mathrm{Base}}_U$$
30		eqid	$$⊢{\mathrm{Base}}_U={\mathrm{Base}}_U$$
31	30 7	topnid	$$⊢\mathrm{TopSet}\left(U\right)\subseteq 𝒫{\mathrm{Base}}_U\to \mathrm{TopSet}\left(U\right)=\mathrm{TopOpen}\left(U\right)$$
32	29 31	syl	$$⊢\phi \to \mathrm{TopSet}\left(U\right)=\mathrm{TopOpen}\left(U\right)$$
33	32 6	eqtr4di	$$⊢\phi \to \mathrm{TopSet}\left(U\right)=O$$
34	33 8	eqtr3d	$$⊢\phi \to O=J\mathrm{qTop}F$$