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

Definition df-qtop 17199
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
StepHypRef Expression
1 cqtop 17195 . 2 class qTop
2 vj . . 3 setvar 𝑗
3 vf . . 3 setvar 𝑓
4 cvv 3430 . . 3 class V
53cv 1540 . . . . . . . 8 class 𝑓
65ccnv 5587 . . . . . . 7 class 𝑓
7 vs . . . . . . . 8 setvar 𝑠
87cv 1540 . . . . . . 7 class 𝑠
96, 8cima 5591 . . . . . 6 class (𝑓𝑠)
102cv 1540 . . . . . . 7 class 𝑗
1110cuni 4844 . . . . . 6 class 𝑗
129, 11cin 3890 . . . . 5 class ((𝑓𝑠) ∩ 𝑗)
1312, 10wcel 2109 . . . 4 wff ((𝑓𝑠) ∩ 𝑗) ∈ 𝑗
145, 11cima 5591 . . . . 5 class (𝑓 𝑗)
1514cpw 4538 . . . 4 class 𝒫 (𝑓 𝑗)
1613, 7, 15crab 3069 . . 3 class {𝑠 ∈ 𝒫 (𝑓 𝑗) ∣ ((𝑓𝑠) ∩ 𝑗) ∈ 𝑗}
172, 3, 4, 4, 16cmpo 7270 . 2 class (𝑗 ∈ V, 𝑓 ∈ V ↦ {𝑠 ∈ 𝒫 (𝑓 𝑗) ∣ ((𝑓𝑠) ∩ 𝑗) ∈ 𝑗})
181, 17wceq 1541 1 wff qTop = (𝑗 ∈ V, 𝑓 ∈ V ↦ {𝑠 ∈ 𝒫 (𝑓 𝑗) ∣ ((𝑓𝑠) ∩ 𝑗) ∈ 𝑗})
Colors of variables: wff setvar class
This definition is referenced by:  qtopval  22827  qtopres  22830
  Copyright terms: Public domain W3C validator