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

Definition df-qtop 13688
 Description: Define the quotient topology given a function and topology on the domain of . (Contributed by Mario Carneiro, 23-Mar-2015.)
Assertion
Ref Expression
df-qtop qTop
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-qtop
StepHypRef Expression
1 cqtop 13684 . 2 qTop
2 vj . . 3
3 vf . . 3
4 cvv 2916 . . 3
53cv 1648 . . . . . . . 8
65ccnv 4836 . . . . . . 7
7 vs . . . . . . . 8
87cv 1648 . . . . . . 7
96, 8cima 4840 . . . . . 6
102cv 1648 . . . . . . 7
1110cuni 3975 . . . . . 6
129, 11cin 3279 . . . . 5
1312, 10wcel 1721 . . . 4
145, 11cima 4840 . . . . 5
1514cpw 3759 . . . 4
1613, 7, 15crab 2670 . . 3
172, 3, 4, 4, 16cmpt2 6042 . 2
181, 17wceq 1649 1 qTop
 Colors of variables: wff set class This definition is referenced by:  qtopval  17680  qtopres  17683
 Copyright terms: Public domain W3C validator