Theorem qtopval

Description: Value of the quotient topology function. (Contributed by Mario Carneiro, 23-Mar-2015)

	Ref	Expression
Hypothesis	qtopval.1	⊢ 𝑋 = ∪ 𝐽
Assertion	qtopval	⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐹 ∈ 𝑊 ) → ( 𝐽 qTop 𝐹 ) = { 𝑠 ∈ 𝒫 ( 𝐹 “ 𝑋 ) ∣ ( ( ◡ 𝐹 “ 𝑠 ) ∩ 𝑋 ) ∈ 𝐽 } )

Proof

Step	Hyp	Ref	Expression
1		qtopval.1	⊢ 𝑋 = ∪ 𝐽
2		elex	⊢ ( 𝐽 ∈ 𝑉 → 𝐽 ∈ V )
3		elex	⊢ ( 𝐹 ∈ 𝑊 → 𝐹 ∈ V )
4		imaexg	⊢ ( 𝐹 ∈ V → ( 𝐹 “ 𝑋 ) ∈ V )
5		pwexg	⊢ ( ( 𝐹 “ 𝑋 ) ∈ V → 𝒫 ( 𝐹 “ 𝑋 ) ∈ V )
6		rabexg	⊢ ( 𝒫 ( 𝐹 “ 𝑋 ) ∈ V → { 𝑠 ∈ 𝒫 ( 𝐹 “ 𝑋 ) ∣ ( ( ◡ 𝐹 “ 𝑠 ) ∩ 𝑋 ) ∈ 𝐽 } ∈ V )
7	4 5 6	3syl	⊢ ( 𝐹 ∈ V → { 𝑠 ∈ 𝒫 ( 𝐹 “ 𝑋 ) ∣ ( ( ◡ 𝐹 “ 𝑠 ) ∩ 𝑋 ) ∈ 𝐽 } ∈ V )
8	7	adantl	⊢ ( ( 𝐽 ∈ V ∧ 𝐹 ∈ V ) → { 𝑠 ∈ 𝒫 ( 𝐹 “ 𝑋 ) ∣ ( ( ◡ 𝐹 “ 𝑠 ) ∩ 𝑋 ) ∈ 𝐽 } ∈ V )
9		simpr	⊢ ( ( 𝑗 = 𝐽 ∧ 𝑓 = 𝐹 ) → 𝑓 = 𝐹 )
10		simpl	⊢ ( ( 𝑗 = 𝐽 ∧ 𝑓 = 𝐹 ) → 𝑗 = 𝐽 )
11	10	unieqd	⊢ ( ( 𝑗 = 𝐽 ∧ 𝑓 = 𝐹 ) → ∪ 𝑗 = ∪ 𝐽 )
12	11 1	eqtr4di	⊢ ( ( 𝑗 = 𝐽 ∧ 𝑓 = 𝐹 ) → ∪ 𝑗 = 𝑋 )
13	9 12	imaeq12d	⊢ ( ( 𝑗 = 𝐽 ∧ 𝑓 = 𝐹 ) → ( 𝑓 “ ∪ 𝑗 ) = ( 𝐹 “ 𝑋 ) )
14	13	pweqd	⊢ ( ( 𝑗 = 𝐽 ∧ 𝑓 = 𝐹 ) → 𝒫 ( 𝑓 “ ∪ 𝑗 ) = 𝒫 ( 𝐹 “ 𝑋 ) )
15	9	cnveqd	⊢ ( ( 𝑗 = 𝐽 ∧ 𝑓 = 𝐹 ) → ◡ 𝑓 = ◡ 𝐹 )
16	15	imaeq1d	⊢ ( ( 𝑗 = 𝐽 ∧ 𝑓 = 𝐹 ) → ( ◡ 𝑓 “ 𝑠 ) = ( ◡ 𝐹 “ 𝑠 ) )
17	16 12	ineq12d	⊢ ( ( 𝑗 = 𝐽 ∧ 𝑓 = 𝐹 ) → ( ( ◡ 𝑓 “ 𝑠 ) ∩ ∪ 𝑗 ) = ( ( ◡ 𝐹 “ 𝑠 ) ∩ 𝑋 ) )
18	17 10	eleq12d	⊢ ( ( 𝑗 = 𝐽 ∧ 𝑓 = 𝐹 ) → ( ( ( ◡ 𝑓 “ 𝑠 ) ∩ ∪ 𝑗 ) ∈ 𝑗 ↔ ( ( ◡ 𝐹 “ 𝑠 ) ∩ 𝑋 ) ∈ 𝐽 ) )
19	14 18	rabeqbidv	⊢ ( ( 𝑗 = 𝐽 ∧ 𝑓 = 𝐹 ) → { 𝑠 ∈ 𝒫 ( 𝑓 “ ∪ 𝑗 ) ∣ ( ( ◡ 𝑓 “ 𝑠 ) ∩ ∪ 𝑗 ) ∈ 𝑗 } = { 𝑠 ∈ 𝒫 ( 𝐹 “ 𝑋 ) ∣ ( ( ◡ 𝐹 “ 𝑠 ) ∩ 𝑋 ) ∈ 𝐽 } )
20		df-qtop	⊢ qTop = ( 𝑗 ∈ V , 𝑓 ∈ V ↦ { 𝑠 ∈ 𝒫 ( 𝑓 “ ∪ 𝑗 ) ∣ ( ( ◡ 𝑓 “ 𝑠 ) ∩ ∪ 𝑗 ) ∈ 𝑗 } )
21	19 20	ovmpoga	⊢ ( ( 𝐽 ∈ V ∧ 𝐹 ∈ V ∧ { 𝑠 ∈ 𝒫 ( 𝐹 “ 𝑋 ) ∣ ( ( ◡ 𝐹 “ 𝑠 ) ∩ 𝑋 ) ∈ 𝐽 } ∈ V ) → ( 𝐽 qTop 𝐹 ) = { 𝑠 ∈ 𝒫 ( 𝐹 “ 𝑋 ) ∣ ( ( ◡ 𝐹 “ 𝑠 ) ∩ 𝑋 ) ∈ 𝐽 } )
22	8 21	mpd3an3	⊢ ( ( 𝐽 ∈ V ∧ 𝐹 ∈ V ) → ( 𝐽 qTop 𝐹 ) = { 𝑠 ∈ 𝒫 ( 𝐹 “ 𝑋 ) ∣ ( ( ◡ 𝐹 “ 𝑠 ) ∩ 𝑋 ) ∈ 𝐽 } )
23	2 3 22	syl2an	⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐹 ∈ 𝑊 ) → ( 𝐽 qTop 𝐹 ) = { 𝑠 ∈ 𝒫 ( 𝐹 “ 𝑋 ) ∣ ( ( ◡ 𝐹 “ 𝑠 ) ∩ 𝑋 ) ∈ 𝐽 } )