Definition df-qtop 17587

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 = (𝑗 ∈ V, 𝑓 ∈ V ↦ {𝑠 ∈ 𝒫 (𝑓 “ ∪ 𝑗) ∣ ((◡𝑓 “ 𝑠) ∩ ∪ 𝑗) ∈ 𝑗})

Distinct variable group:   𝑓,𝑗,𝑠

Detailed syntax breakdown of Definition df-qtop

Step	Hyp	Ref	Expression
1		cqtop 17583	. 2 class qTop
2		vj	. . 3 setvar 𝑗
3		vf	. . 3 setvar 𝑓
4		cvv 3457	. . 3 class V
5	3	cv 1569	. . . . . . . 8 class 𝑓
6	5	ccnv 5662	. . . . . . 7 class ◡𝑓
7		vs	. . . . . . . 8 setvar 𝑠
8	7	cv 1569	. . . . . . 7 class 𝑠
9	6, 8	cima 5666	. . . . . 6 class (◡𝑓 “ 𝑠)
10	2	cv 1569	. . . . . . 7 class 𝑗
11	10	cuni 4874	. . . . . 6 class ∪ 𝑗
12	9, 11	cin 3905	. . . . 5 class ((◡𝑓 “ 𝑠) ∩ ∪ 𝑗)
13	12, 10	wcel 2146	. . . 4 wff ((◡𝑓 “ 𝑠) ∩ ∪ 𝑗) ∈ 𝑗
14	5, 11	cima 5666	. . . . 5 class (𝑓 “ ∪ 𝑗)
15	14	cpw 4564	. . . 4 class 𝒫 (𝑓 “ ∪ 𝑗)
16	13, 7, 15	crab 3418	. . 3 class {𝑠 ∈ 𝒫 (𝑓 “ ∪ 𝑗) ∣ ((◡𝑓 “ 𝑠) ∩ ∪ 𝑗) ∈ 𝑗}
17	2, 3, 4, 4, 16	cmpo 7421	. 2 class (𝑗 ∈ V, 𝑓 ∈ V ↦ {𝑠 ∈ 𝒫 (𝑓 “ ∪ 𝑗) ∣ ((◡𝑓 “ 𝑠) ∩ ∪ 𝑗) ∈ 𝑗})
18	1, 17	wceq 1570	1 wff qTop = (𝑗 ∈ V, 𝑓 ∈ V ↦ {𝑠 ∈ 𝒫 (𝑓 “ ∪ 𝑗) ∣ ((◡𝑓 “ 𝑠) ∩ ∪ 𝑗) ∈ 𝑗})

This definition is used by:  qtopval  23907  qtopres  23910