# Metamath Proof Explorer

## 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 ${setvar}{j}$
2 cvv ${class}\mathrm{V}$
3 vf ${setvar}{f}$
4 vs ${setvar}{s}$
5 3 cv ${setvar}{f}$
6 1 cv ${setvar}{j}$
7 6 cuni ${class}\bigcup {j}$
8 5 7 cima ${class}{f}\left[\bigcup {j}\right]$
9 8 cpw ${class}𝒫{f}\left[\bigcup {j}\right]$
10 5 ccnv ${class}{{f}}^{-1}$
11 4 cv ${setvar}{s}$
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)$