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

Metamath Proof Explorer

Theorem kqval

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

Ref Expression
Hypothesis kqval.2 ⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } )
Assertion kqval ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( KQ ‘ 𝐽 ) = ( 𝐽 qTop 𝐹 ) )

Proof

Step Hyp Ref Expression
1 kqval.2 ⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } )
2 topontop ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐽 ∈ Top )
3 id ⊢ ( 𝑗 = 𝐽 → 𝑗 = 𝐽 )
4 unieq ⊢ ( 𝑗 = 𝐽 → ∪ 𝑗 = ∪ 𝐽 )
5 rabeq ⊢ ( 𝑗 = 𝐽 → { 𝑦 ∈ 𝑗 ∣ 𝑥 ∈ 𝑦 } = { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } )
6 4 5 mpteq12dv ⊢ ( 𝑗 = 𝐽 → ( 𝑥 ∈ ∪ 𝑗 ↦ { 𝑦 ∈ 𝑗 ∣ 𝑥 ∈ 𝑦 } ) = ( 𝑥 ∈ ∪ 𝐽 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } ) )
7 3 6 oveq12d ⊢ ( 𝑗 = 𝐽 → ( 𝑗 qTop ( 𝑥 ∈ ∪ 𝑗 ↦ { 𝑦 ∈ 𝑗 ∣ 𝑥 ∈ 𝑦 } ) ) = ( 𝐽 qTop ( 𝑥 ∈ ∪ 𝐽 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } ) ) )
8 df-kq ⊢ KQ = ( 𝑗 ∈ Top ↦ ( 𝑗 qTop ( 𝑥 ∈ ∪ 𝑗 ↦ { 𝑦 ∈ 𝑗 ∣ 𝑥 ∈ 𝑦 } ) ) )
9 ovex ⊢ ( 𝐽 qTop ( 𝑥 ∈ ∪ 𝐽 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } ) ) ∈ V
10 7 8 9 fvmpt ⊢ ( 𝐽 ∈ Top → ( KQ ‘ 𝐽 ) = ( 𝐽 qTop ( 𝑥 ∈ ∪ 𝐽 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } ) ) )
11 2 10 syl ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( KQ ‘ 𝐽 ) = ( 𝐽 qTop ( 𝑥 ∈ ∪ 𝐽 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } ) ) )
12 toponuni ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
13 12 mpteq1d ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } ) = ( 𝑥 ∈ ∪ 𝐽 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } ) )
14 1 13 eqtrid ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐹 = ( 𝑥 ∈ ∪ 𝐽 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } ) )
15 14 oveq2d ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝐽 qTop 𝐹 ) = ( 𝐽 qTop ( 𝑥 ∈ ∪ 𝐽 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } ) ) )
16 11 15 eqtr4d ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( KQ ‘ 𝐽 ) = ( 𝐽 qTop 𝐹 ) )