Definition df-qtop 16167

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

Step	Hyp	Ref	Expression
1		cqtop 16163	. 2 class qTop
2		vj	. . 3 setvar j
3		vf	. . 3 setvar f
4		cvv 3200	. . 3 class _V
5	3	cv 1482	. . . . . . . 8 class f
6	5	ccnv 5113	. . . . . . 7 class `' f
7		vs	. . . . . . . 8 setvar s
8	7	cv 1482	. . . . . . 7 class s
9	6, 8	cima 5117	. . . . . 6 class ( `' f " s )
10	2	cv 1482	. . . . . . 7 class j
11	10	cuni 4436	. . . . . 6 class U. j
12	9, 11	cin 3573	. . . . 5 class ( ( `' f " s ) i^i U. j )
13	12, 10	wcel 1990	. . . 4 wff ( ( `' f " s ) i^i U. j ) e. j
14	5, 11	cima 5117	. . . . 5 class ( f " U. j )
15	14	cpw 4158	. . . 4 class ~P ( f " U. j )
16	13, 7, 15	crab 2916	. . 3 class { s e. ~P ( f " U. j ) | ( ( `' f " s ) i^i U. j ) e. j }
17	2, 3, 4, 4, 16	cmpt2 6652	. 2 class ( j e. _V , f e. _V |-> { s e. ~P ( f " U. j ) | ( ( `' f " s ) i^i U. j ) e. j } )
18	1, 17	wceq 1483	1 wff qTop = ( j e. _V , f e. _V |-> { s e. ~P ( f " U. j ) | ( ( `' f " s ) i^i U. j ) e. j } )

This definition is referenced by:  qtopval  21498  qtopres  21501