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 )