kqnrm

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

		Ref	Expression
	Assertion	kqnrm	$⊢ J \in Nrm \leftrightarrow KQ (J) \in Nrm$

Step	Hyp	Ref	Expression
1		nrmtop	$⊢ J \in Nrm \to J \in Top$
2		toptopon2	$⊢ J \in Top \leftrightarrow J \in TopOn (⋃ J)$
3	1 2	sylib	$⊢ J \in Nrm \to J \in TopOn (⋃ J)$
4		eqid	$⊢ (x \in ⋃ J ⟼ \{y \in J \| x \in y\}) = (x \in ⋃ J ⟼ \{y \in J \| x \in y\})$
5	4	kqnrmlem1	$⊢ (J \in TopOn (⋃ J) \land J \in Nrm) \to KQ (J) \in Nrm$
6	3 5	mpancom	$⊢ J \in Nrm \to KQ (J) \in Nrm$
7		nrmtop	$⊢ KQ (J) \in Nrm \to KQ (J) \in Top$
8		kqtop	$⊢ J \in Top \leftrightarrow KQ (J) \in Top$
9	7 8	sylibr	$⊢ KQ (J) \in Nrm \to J \in Top$
10	9 2	sylib	$⊢ KQ (J) \in Nrm \to J \in TopOn (⋃ J)$
11	4	kqnrmlem2	$⊢ (J \in TopOn (⋃ J) \land KQ (J) \in Nrm) \to J \in Nrm$
12	10 11	mpancom	$⊢ KQ (J) \in Nrm \to J \in Nrm$
13	6 12	impbii	$⊢ J \in Nrm \leftrightarrow KQ (J) \in Nrm$

Metamath Proof Explorer