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

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 ( 𝐽 ∈ Top ↔ ( KQ ‘ 𝐽 ) ∈ Top )

Proof

Step Hyp Ref Expression
1 toptopon2 ⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) )
2 eqid ⊢ ( 𝑥 ∈ ∪ 𝐽 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } ) = ( 𝑥 ∈ ∪ 𝐽 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } )
3 2 kqtopon ⊢ ( 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) → ( KQ ‘ 𝐽 ) ∈ ( TopOn ‘ ran ( 𝑥 ∈ ∪ 𝐽 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } ) ) )
4 1 3 sylbi ⊢ ( 𝐽 ∈ Top → ( KQ ‘ 𝐽 ) ∈ ( TopOn ‘ ran ( 𝑥 ∈ ∪ 𝐽 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } ) ) )
5 topontop ⊢ ( ( KQ ‘ 𝐽 ) ∈ ( TopOn ‘ ran ( 𝑥 ∈ ∪ 𝐽 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } ) ) → ( KQ ‘ 𝐽 ) ∈ Top )
6 4 5 syl ⊢ ( 𝐽 ∈ Top → ( KQ ‘ 𝐽 ) ∈ Top )
7 0opn ⊢ ( ( KQ ‘ 𝐽 ) ∈ Top → ∅ ∈ ( KQ ‘ 𝐽 ) )
8 elfvdm ⊢ ( ∅ ∈ ( KQ ‘ 𝐽 ) → 𝐽 ∈ dom KQ )
9 7 8 syl ⊢ ( ( KQ ‘ 𝐽 ) ∈ Top → 𝐽 ∈ dom KQ )
10 ovex ⊢ ( 𝑗 qTop ( 𝑥 ∈ ∪ 𝑗 ↦ { 𝑦 ∈ 𝑗 ∣ 𝑥 ∈ 𝑦 } ) ) ∈ V
11 df-kq ⊢ KQ = ( 𝑗 ∈ Top ↦ ( 𝑗 qTop ( 𝑥 ∈ ∪ 𝑗 ↦ { 𝑦 ∈ 𝑗 ∣ 𝑥 ∈ 𝑦 } ) ) )
12 10 11 dmmpti ⊢ dom KQ = Top
13 9 12 eleqtrdi ⊢ ( ( KQ ‘ 𝐽 ) ∈ Top → 𝐽 ∈ Top )
14 6 13 impbii ⊢ ( 𝐽 ∈ Top ↔ ( KQ ‘ 𝐽 ) ∈ Top )