Metamath Proof Explorer

Theorem kqtopon

Description: The Kolmogorov quotient is a topology on the quotient set. (Contributed by Mario Carneiro, 25-Aug-2015)

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

Proof

Step Hyp Ref Expression
1 kqval.2 ⊢ F = x ∈ X ⟼ y ∈ J | x ∈ y
2 1 kqval ⊢ J ∈ TopOn ⁡ X → KQ ⁡ J = J qTop F
3 1 kqffn ⊢ J ∈ TopOn ⁡ X → F Fn X
4 dffn4 ⊢ F Fn X ↔ F : X ⟶ onto ran ⁡ F
5 3 4 sylib ⊢ J ∈ TopOn ⁡ X → F : X ⟶ onto ran ⁡ F
6 qtoptopon ⊢ J ∈ TopOn ⁡ X ∧ F : X ⟶ onto ran ⁡ F → J qTop F ∈ TopOn ⁡ ran ⁡ F
7 5 6 mpdan ⊢ J ∈ TopOn ⁡ X → J qTop F ∈ TopOn ⁡ ran ⁡ F
8 2 7 eqeltrd ⊢ J ∈ TopOn ⁡ X → KQ ⁡ J ∈ TopOn ⁡ ran ⁡ F