MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-qtop Unicode version

Definition df-qtop 13503
Description: Define the quotient topology given a function  f and topology  j on the domain of  f. (Contributed by Mario Carneiro, 23-Mar-2015.)
Assertion
Ref Expression
df-qtop  |- qTop  =  ( j  e.  _V , 
f  e.  _V  |->  { s  e.  ~P (
f " U. j
)  |  ( ( `' f " s
)  i^i  U. j
)  e.  j } )
Distinct variable group:    f, j, s

Detailed syntax breakdown of Definition df-qtop
StepHypRef Expression
1 cqtop 13499 . 2  class qTop
2 vj . . 3  set  j
3 vf . . 3  set  f
4 cvv 2864 . . 3  class  _V
53cv 1641 . . . . . . . 8  class  f
65ccnv 4767 . . . . . . 7  class  `' f
7 vs . . . . . . . 8  set  s
87cv 1641 . . . . . . 7  class  s
96, 8cima 4771 . . . . . 6  class  ( `' f " s )
102cv 1641 . . . . . . 7  class  j
1110cuni 3906 . . . . . 6  class  U. j
129, 11cin 3227 . . . . 5  class  ( ( `' f " s
)  i^i  U. j
)
1312, 10wcel 1710 . . . 4  wff  ( ( `' f " s
)  i^i  U. j
)  e.  j
145, 11cima 4771 . . . . 5  class  ( f
" U. j )
1514cpw 3701 . . . 4  class  ~P (
f " U. j
)
1613, 7, 15crab 2623 . . 3  class  { s  e.  ~P ( f
" U. j )  |  ( ( `' f " s )  i^i  U. j )  e.  j }
172, 3, 4, 4, 16cmpt2 5944 . 2  class  ( j  e.  _V ,  f  e.  _V  |->  { s  e.  ~P ( f
" U. j )  |  ( ( `' f " s )  i^i  U. j )  e.  j } )
181, 17wceq 1642 1  wff qTop  =  ( j  e.  _V , 
f  e.  _V  |->  { s  e.  ~P (
f " U. j
)  |  ( ( `' f " s
)  i^i  U. j
)  e.  j } )
Colors of variables: wff set class
This definition is referenced by:  qtopval  17486  qtopres  17489
  Copyright terms: Public domain W3C validator