This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∈ V , f ∈ V ⟼ s ∈ 𝒫 f ⋃ j | f -1 s ∩ ⋃ j ∈ j

Detailed syntax breakdown

Step Hyp Ref Expression
0 cqtop class qTop
1 vj setvar j
2 cvv class V
3 vf setvar f
4 vs setvar s
5 3 cv setvar f
6 1 cv setvar j
7 6 cuni class ⋃ j
8 5 7 cima class f ⋃ j
9 8 cpw class 𝒫 f ⋃ j
10 5 ccnv class f -1
11 4 cv setvar s
12 10 11 cima class f -1 s
13 12 7 cin class f -1 s ∩ ⋃ j
14 13 6 wcel wff f -1 s ∩ ⋃ j ∈ j
15 14 4 9 crab class s ∈ 𝒫 f ⋃ j | f -1 s ∩ ⋃ j ∈ j
16 1 3 2 2 15 cmpo class j ∈ V , f ∈ V ⟼ s ∈ 𝒫 f ⋃ j | f -1 s ∩ ⋃ j ∈ j
17 0 16 wceq wff qTop = j ∈ V , f ∈ V ⟼ s ∈ 𝒫 f ⋃ j | f -1 s ∩ ⋃ j ∈ j