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

Detailed syntax breakdown

Step Hyp Ref Expression
0 cqtop ⊢ qTop
1 vj ⊢ 𝑗
2 cvv ⊢ V
3 vf ⊢ 𝑓
4 vs ⊢ 𝑠
5 3 cv ⊢ 𝑓
6 1 cv ⊢ 𝑗
7 6 cuni ⊢ ∪ 𝑗
8 5 7 cima ⊢ ( 𝑓 “ ∪ 𝑗 )
9 8 cpw ⊢ 𝒫 ( 𝑓 “ ∪ 𝑗 )
10 5 ccnv ⊢ ◡ 𝑓
11 4 cv ⊢ 𝑠
12 10 11 cima ⊢ ( ◡ 𝑓 “ 𝑠 )
13 12 7 cin ⊢ ( ( ◡ 𝑓 “ 𝑠 ) ∩ ∪ 𝑗 )
14 13 6 wcel ⊢ ( ( ◡ 𝑓 “ 𝑠 ) ∩ ∪ 𝑗 ) ∈ 𝑗
15 14 4 9 crab ⊢ { 𝑠 ∈ 𝒫 ( 𝑓 “ ∪ 𝑗 ) ∣ ( ( ◡ 𝑓 “ 𝑠 ) ∩ ∪ 𝑗 ) ∈ 𝑗 }
16 1 3 2 2 15 cmpo ⊢ ( 𝑗 ∈ V , 𝑓 ∈ V ↦ { 𝑠 ∈ 𝒫 ( 𝑓 “ ∪ 𝑗 ) ∣ ( ( ◡ 𝑓 “ 𝑠 ) ∩ ∪ 𝑗 ) ∈ 𝑗 } )
17 0 16 wceq ⊢ qTop = ( 𝑗 ∈ V , 𝑓 ∈ V ↦ { 𝑠 ∈ 𝒫 ( 𝑓 “ ∪ 𝑗 ) ∣ ( ( ◡ 𝑓 “ 𝑠 ) ∩ ∪ 𝑗 ) ∈ 𝑗 } )