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

Metamath Proof Explorer

Theorem kqnrm

Description: The Kolmogorov quotient of a normal space is normal. (Contributed by Mario Carneiro, 25-Aug-2015)

Ref Expression
Assertion kqnrm ( 𝐽 ∈ Nrm ↔ ( KQ ‘ 𝐽 ) ∈ Nrm )

Proof

Step Hyp Ref Expression
1 nrmtop ⊢ ( 𝐽 ∈ Nrm → 𝐽 ∈ Top )
2 toptopon2 ⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) )
3 1 2 sylib ⊢ ( 𝐽 ∈ Nrm → 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) )
4 eqid ⊢ ( 𝑥 ∈ ∪ 𝐽 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } ) = ( 𝑥 ∈ ∪ 𝐽 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } )
5 4 kqnrmlem1 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) ∧ 𝐽 ∈ Nrm ) → ( KQ ‘ 𝐽 ) ∈ Nrm )
6 3 5 mpancom ⊢ ( 𝐽 ∈ Nrm → ( KQ ‘ 𝐽 ) ∈ Nrm )
7 nrmtop ⊢ ( ( KQ ‘ 𝐽 ) ∈ Nrm → ( KQ ‘ 𝐽 ) ∈ Top )
8 kqtop ⊢ ( 𝐽 ∈ Top ↔ ( KQ ‘ 𝐽 ) ∈ Top )
9 7 8 sylibr ⊢ ( ( KQ ‘ 𝐽 ) ∈ Nrm → 𝐽 ∈ Top )
10 9 2 sylib ⊢ ( ( KQ ‘ 𝐽 ) ∈ Nrm → 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) )
11 4 kqnrmlem2 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) → 𝐽 ∈ Nrm )
12 10 11 mpancom ⊢ ( ( KQ ‘ 𝐽 ) ∈ Nrm → 𝐽 ∈ Nrm )
13 6 12 impbii ⊢ ( 𝐽 ∈ Nrm ↔ ( KQ ‘ 𝐽 ) ∈ Nrm )