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