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	|- qTop = ( j e. _V , f e. _V |-> { s e. ~P ( f " U. j ) | ( ( `' f " s ) i^i U. j ) e. j } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cqtop	|- qTop
1		vj	|- j
2		cvv	|- _V
3		vf	|- f
4		vs	|- s
5	3	cv	|- f
6	1	cv	|- j
7	6	cuni	|- U. j
8	5 7	cima	|- ( f " U. j )
9	8	cpw	|- ~P ( f " U. j )
10	5	ccnv	|- `' f
11	4	cv	|- s
12	10 11	cima	|- ( `' f " s )
13	12 7	cin	|- ( ( `' f " s ) i^i U. j )
14	13 6	wcel	|- ( ( `' f " s ) i^i U. j ) e. j
15	14 4 9	crab	|- { s e. ~P ( f " U. j ) | ( ( `' f " s ) i^i U. j ) e. j }
16	1 3 2 2 15	cmpo	|- ( j e. _V , f e. _V |-> { s e. ~P ( f " U. j ) | ( ( `' f " s ) i^i U. j ) e. j } )
17	0 16	wceq	|- qTop = ( j e. _V , f e. _V |-> { s e. ~P ( f " U. j ) | ( ( `' f " s ) i^i U. j ) e. j } )