Metamath Proof Explorer

Theorem kqval

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

Ref Expression
Hypothesis kqval.2 ⊢ F = x ∈ X ⟼ y ∈ J | x ∈ y
Assertion kqval ⊢ J ∈ TopOn ⁡ X → KQ ⁡ J = J qTop F

Proof

Step Hyp Ref Expression
1 kqval.2 ⊢ F = x ∈ X ⟼ y ∈ J | x ∈ y
2 topontop ⊢ J ∈ TopOn ⁡ X → J ∈ Top
3 id ⊢ j = J → j = J
4 unieq ⊢ j = J → ⋃ j = ⋃ J
5 rabeq ⊢ j = J → y ∈ j | x ∈ y = y ∈ J | x ∈ y
6 4 5 mpteq12dv ⊢ j = J → x ∈ ⋃ j ⟼ y ∈ j | x ∈ y = x ∈ ⋃ J ⟼ y ∈ J | x ∈ y
7 3 6 oveq12d ⊢ j = J → j qTop x ∈ ⋃ j ⟼ y ∈ j | x ∈ y = J qTop x ∈ ⋃ J ⟼ y ∈ J | x ∈ y
8 df-kq ⊢ KQ = j ∈ Top ⟼ j qTop x ∈ ⋃ j ⟼ y ∈ j | x ∈ y
9 ovex ⊢ J qTop x ∈ ⋃ J ⟼ y ∈ J | x ∈ y ∈ V
10 7 8 9 fvmpt ⊢ J ∈ Top → KQ ⁡ J = J qTop x ∈ ⋃ J ⟼ y ∈ J | x ∈ y
11 2 10 syl ⊢ J ∈ TopOn ⁡ X → KQ ⁡ J = J qTop x ∈ ⋃ J ⟼ y ∈ J | x ∈ y
12 toponuni ⊢ J ∈ TopOn ⁡ X → X = ⋃ J
13 12 mpteq1d ⊢ J ∈ TopOn ⁡ X → x ∈ X ⟼ y ∈ J | x ∈ y = x ∈ ⋃ J ⟼ y ∈ J | x ∈ y
14 1 13 syl5eq ⊢ J ∈ TopOn ⁡ X → F = x ∈ ⋃ J ⟼ y ∈ J | x ∈ y
15 14 oveq2d ⊢ J ∈ TopOn ⁡ X → J qTop F = J qTop x ∈ ⋃ J ⟼ y ∈ J | x ∈ y
16 11 15 eqtr4d ⊢ J ∈ TopOn ⁡ X → KQ ⁡ J = J qTop F