Metamath Proof Explorer

Theorem kqtop

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

Ref Expression
Assertion kqtop ⊢ J ∈ Top ↔ KQ ⁡ J ∈ Top

Proof

Step Hyp Ref Expression
1 toptopon2 ⊢ J ∈ Top ↔ J ∈ TopOn ⁡ ⋃ J
2 eqid ⊢ x ∈ ⋃ J ⟼ y ∈ J | x ∈ y = x ∈ ⋃ J ⟼ y ∈ J | x ∈ y
3 2 kqtopon ⊢ J ∈ TopOn ⁡ ⋃ J → KQ ⁡ J ∈ TopOn ⁡ ran ⁡ x ∈ ⋃ J ⟼ y ∈ J | x ∈ y
4 1 3 sylbi ⊢ J ∈ Top → KQ ⁡ J ∈ TopOn ⁡ ran ⁡ x ∈ ⋃ J ⟼ y ∈ J | x ∈ y
5 topontop ⊢ KQ ⁡ J ∈ TopOn ⁡ ran ⁡ x ∈ ⋃ J ⟼ y ∈ J | x ∈ y → KQ ⁡ J ∈ Top
6 4 5 syl ⊢ J ∈ Top → KQ ⁡ J ∈ Top
7 0opn ⊢ KQ ⁡ J ∈ Top → ∅ ∈ KQ ⁡ J
8 elfvdm ⊢ ∅ ∈ KQ ⁡ J → J ∈ dom ⁡ KQ
9 7 8 syl ⊢ KQ ⁡ J ∈ Top → J ∈ dom ⁡ KQ
10 ovex ⊢ j qTop x ∈ ⋃ j ⟼ y ∈ j | x ∈ y ∈ V
11 df-kq ⊢ KQ = j ∈ Top ⟼ j qTop x ∈ ⋃ j ⟼ y ∈ j | x ∈ y
12 10 11 dmmpti ⊢ dom ⁡ KQ = Top
13 9 12 eleqtrdi ⊢ KQ ⁡ J ∈ Top → J ∈ Top
14 6 13 impbii ⊢ J ∈ Top ↔ KQ ⁡ J ∈ Top