Definition df-qtop

Description: Define the quotient topology given a function f and topology j on the domain of f . (Contributed by Mario Carneiro, 23-Mar-2015)

	Ref	Expression
Assertion	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)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cqtop	$$class\mathrm{qTop}$$
1		vj	$$setvarj$$
2		cvv	$$class\mathrm{V}$$
3		vf	$$setvarf$$
4		vs	$$setvars$$
5	3	cv	$$setvarf$$
6	1	cv	$$setvarj$$
7	6	cuni	$$class\bigcup j$$
8	5 7	cima	$$classf\left[\bigcup j\right]$$
9	8	cpw	$$class𝒫f\left[\bigcup j\right]$$
10	5	ccnv	$$class{f}^{-1}$$
11	4	cv	$$setvars$$
12	10 11	cima	$$class{f}^{-1}\left[s\right]$$
13	12 7	cin	$$class\left(f^{-1}\left[s\right]\cap \bigcup j\right)$$
14	13 6	wcel	$$wff{f}^{-1}\left[s\right]\cap \bigcup j\in j$$
15	14 4 9	crab	$$class\left\{s\in 𝒫f\left[\bigcup j\right]|f^{-1}\left[s\right]\cap \bigcup j\in j\right\}$$
16	1 3 2 2 15	cmpo	$$class\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)$$
17	0 16	wceq	$$wff\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)$$