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 )