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 16368
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 16364 . 2 class qTop
2 vj . . 3 setvar 𝑗
3 vf . . 3 setvar 𝑓
4 cvv 3391 . . 3 class V
53cv 1636 . . . . . . . 8 class 𝑓
65ccnv 5310 . . . . . . 7 class 𝑓
7 vs . . . . . . . 8 setvar 𝑠
87cv 1636 . . . . . . 7 class 𝑠
96, 8cima 5314 . . . . . 6 class (𝑓𝑠)
102cv 1636 . . . . . . 7 class 𝑗
1110cuni 4630 . . . . . 6 class 𝑗
129, 11cin 3768 . . . . 5 class ((𝑓𝑠) ∩ 𝑗)
1312, 10wcel 2156 . . . 4 wff ((𝑓𝑠) ∩ 𝑗) ∈ 𝑗
145, 11cima 5314 . . . . 5 class (𝑓 𝑗)
1514cpw 4351 . . . 4 class 𝒫 (𝑓 𝑗)
1613, 7, 15crab 3100 . . 3 class {𝑠 ∈ 𝒫 (𝑓 𝑗) ∣ ((𝑓𝑠) ∩ 𝑗) ∈ 𝑗}
172, 3, 4, 4, 16cmpt2 6872 . 2 class (𝑗 ∈ V, 𝑓 ∈ V ↦ {𝑠 ∈ 𝒫 (𝑓 𝑗) ∣ ((𝑓𝑠) ∩ 𝑗) ∈ 𝑗})
181, 17wceq 1637 1 wff qTop = (𝑗 ∈ V, 𝑓 ∈ V ↦ {𝑠 ∈ 𝒫 (𝑓 𝑗) ∣ ((𝑓𝑠) ∩ 𝑗) ∈ 𝑗})
Colors of variables: wff setvar class
This definition is referenced by:  qtopval  21708  qtopres  21711
  Copyright terms: Public domain W3C validator