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

Metamath Proof Explorer

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 𝐹 ) = { 𝑠 ∈ 𝒫 ( 𝐹 “ 𝑋 ) ∣ ( ( ◡ 𝐹 “ 𝑠 ) ∩ 𝑋 ) ∈ 𝐽 } )