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

Definition df-qtop 14437
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
Distinct variable group:   , ,

Detailed syntax breakdown of Definition df-qtop
StepHypRef Expression
1 cqtop 14433 . 2
2 vj . . 3
3 vf . . 3
4 cvv 2967 . . 3
53cv 1368 . . . . . . . 8
65ccnv 4834 . . . . . . 7
7 vs . . . . . . . 8
87cv 1368 . . . . . . 7
96, 8cima 4838 . . . . . 6
102cv 1368 . . . . . . 7
1110cuni 4086 . . . . . 6
129, 11cin 3322 . . . . 5
1312, 10wcel 1756 . . . 4
145, 11cima 4838 . . . . 5
1514cpw 3855 . . . 4
1613, 7, 15crab 2714 . . 3
172, 3, 4, 4, 16cmpt2 6088 . 2
181, 17wceq 1369 1
Colors of variables: wff setvar class
This definition is referenced by:  qtopval  19248  qtopres  19251
  Copyright terms: Public domain W3C validator