kqnrmlem1

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

		Ref	Expression
	Hypothesis	kqval.2	$⊢ F = (x \in X ⟼ \{y \in J \| x \in y\})$
	Assertion	kqnrmlem1	$⊢ (J \in TopOn (X) \land J \in Nrm) \to KQ (J) \in Nrm$

Proof

Step	Hyp	Ref	Expression
1		kqval.2	$⊢ F = (x \in X ⟼ \{y \in J \| x \in y\})$
2	1	kqtopon	$⊢ J \in TopOn (X) \to KQ (J) \in TopOn (ran F)$
3	2	adantr	$⊢ (J \in TopOn (X) \land J \in Nrm) \to KQ (J) \in TopOn (ran F)$
4		topontop	$⊢ KQ (J) \in TopOn (ran F) \to KQ (J) \in Top$
5	3 4	syl	$⊢ (J \in TopOn (X) \land J \in Nrm) \to KQ (J) \in Top$
6		simplr	$⊢ ((J \in TopOn (X) \land J \in Nrm) \land (z \in KQ (J) \land w \in (Clsd (KQ (J)) \cap 𝒫 z))) \to J \in Nrm$
7	1	kqid	$⊢ J \in TopOn (X) \to F \in (J Cn KQ (J))$
8	7	ad2antrr	$⊢ ((J \in TopOn (X) \land J \in Nrm) \land (z \in KQ (J) \land w \in (Clsd (KQ (J)) \cap 𝒫 z))) \to F \in (J Cn KQ (J))$
9		simprl	$⊢ ((J \in TopOn (X) \land J \in Nrm) \land (z \in KQ (J) \land w \in (Clsd (KQ (J)) \cap 𝒫 z))) \to z \in KQ (J)$
10		cnima	$⊢ (F \in (J Cn KQ (J)) \land z \in KQ (J)) \to F^{-1} [z] \in J$
11	8 9 10	syl2anc	$⊢ ((J \in TopOn (X) \land J \in Nrm) \land (z \in KQ (J) \land w \in (Clsd (KQ (J)) \cap 𝒫 z))) \to F^{-1} [z] \in J$
12		simprr	$⊢ ((J \in TopOn (X) \land J \in Nrm) \land (z \in KQ (J) \land w \in (Clsd (KQ (J)) \cap 𝒫 z))) \to w \in (Clsd (KQ (J)) \cap 𝒫 z)$
13	12	elin1d	$⊢ ((J \in TopOn (X) \land J \in Nrm) \land (z \in KQ (J) \land w \in (Clsd (KQ (J)) \cap 𝒫 z))) \to w \in Clsd (KQ (J))$
14		cnclima	$⊢ (F \in (J Cn KQ (J)) \land w \in Clsd (KQ (J))) \to F^{-1} [w] \in Clsd (J)$
15	8 13 14	syl2anc	$⊢ ((J \in TopOn (X) \land J \in Nrm) \land (z \in KQ (J) \land w \in (Clsd (KQ (J)) \cap 𝒫 z))) \to F^{-1} [w] \in Clsd (J)$
16	12	elin2d	$⊢ ((J \in TopOn (X) \land J \in Nrm) \land (z \in KQ (J) \land w \in (Clsd (KQ (J)) \cap 𝒫 z))) \to w \in 𝒫 z$
17		elpwi	$⊢ w \in 𝒫 z \to w \subseteq z$
18		imass2	$⊢ w \subseteq z \to F^{-1} [w] \subseteq F^{-1} [z]$
19	16 17 18	3syl	$⊢ ((J \in TopOn (X) \land J \in Nrm) \land (z \in KQ (J) \land w \in (Clsd (KQ (J)) \cap 𝒫 z))) \to F^{-1} [w] \subseteq F^{-1} [z]$
20		nrmsep3	$⊢ (J \in Nrm \land (F^{-1} [z] \in J \land F^{-1} [w] \in Clsd (J) \land F^{-1} [w] \subseteq F^{-1} [z])) \to \exists u \in J (F^{-1} [w] \subseteq u \land cls (J) (u) \subseteq F^{-1} [z])$
21	6 11 15 19 20	syl13anc	$⊢ ((J \in TopOn (X) \land J \in Nrm) \land (z \in KQ (J) \land w \in (Clsd (KQ (J)) \cap 𝒫 z))) \to \exists u \in J (F^{-1} [w] \subseteq u \land cls (J) (u) \subseteq F^{-1} [z])$
22		simplll	$⊢ (((J \in TopOn (X) \land J \in Nrm) \land (z \in KQ (J) \land w \in (Clsd (KQ (J)) \cap 𝒫 z))) \land (u \in J \land (F^{-1} [w] \subseteq u \land cls (J) (u) \subseteq F^{-1} [z]))) \to J \in TopOn (X)$
23		simprl	$⊢ (((J \in TopOn (X) \land J \in Nrm) \land (z \in KQ (J) \land w \in (Clsd (KQ (J)) \cap 𝒫 z))) \land (u \in J \land (F^{-1} [w] \subseteq u \land cls (J) (u) \subseteq F^{-1} [z]))) \to u \in J$
24	1	kqopn	$⊢ (J \in TopOn (X) \land u \in J) \to F [u] \in KQ (J)$
25	22 23 24	syl2anc	$⊢ (((J \in TopOn (X) \land J \in Nrm) \land (z \in KQ (J) \land w \in (Clsd (KQ (J)) \cap 𝒫 z))) \land (u \in J \land (F^{-1} [w] \subseteq u \land cls (J) (u) \subseteq F^{-1} [z]))) \to F [u] \in KQ (J)$
26		simprrl	$⊢ (((J \in TopOn (X) \land J \in Nrm) \land (z \in KQ (J) \land w \in (Clsd (KQ (J)) \cap 𝒫 z))) \land (u \in J \land (F^{-1} [w] \subseteq u \land cls (J) (u) \subseteq F^{-1} [z]))) \to F^{-1} [w] \subseteq u$
27	1	kqffn	$⊢ J \in TopOn (X) \to F Fn X$
28		fnfun	$⊢ F Fn X \to Fun F$
29	22 27 28	3syl	$⊢ (((J \in TopOn (X) \land J \in Nrm) \land (z \in KQ (J) \land w \in (Clsd (KQ (J)) \cap 𝒫 z))) \land (u \in J \land (F^{-1} [w] \subseteq u \land cls (J) (u) \subseteq F^{-1} [z]))) \to Fun F$
30	13	adantr	$⊢ (((J \in TopOn (X) \land J \in Nrm) \land (z \in KQ (J) \land w \in (Clsd (KQ (J)) \cap 𝒫 z))) \land (u \in J \land (F^{-1} [w] \subseteq u \land cls (J) (u) \subseteq F^{-1} [z]))) \to w \in Clsd (KQ (J))$
31		eqid	$⊢ ⋃ KQ (J) = ⋃ KQ (J)$
32	31	cldss	$⊢ w \in Clsd (KQ (J)) \to w \subseteq ⋃ KQ (J)$
33	30 32	syl	$⊢ (((J \in TopOn (X) \land J \in Nrm) \land (z \in KQ (J) \land w \in (Clsd (KQ (J)) \cap 𝒫 z))) \land (u \in J \land (F^{-1} [w] \subseteq u \land cls (J) (u) \subseteq F^{-1} [z]))) \to w \subseteq ⋃ KQ (J)$
34		toponuni	$⊢ KQ (J) \in TopOn (ran F) \to ran F = ⋃ KQ (J)$
35	22 2 34	3syl	$⊢ (((J \in TopOn (X) \land J \in Nrm) \land (z \in KQ (J) \land w \in (Clsd (KQ (J)) \cap 𝒫 z))) \land (u \in J \land (F^{-1} [w] \subseteq u \land cls (J) (u) \subseteq F^{-1} [z]))) \to ran F = ⋃ KQ (J)$
36	33 35	sseqtrrd	$⊢ (((J \in TopOn (X) \land J \in Nrm) \land (z \in KQ (J) \land w \in (Clsd (KQ (J)) \cap 𝒫 z))) \land (u \in J \land (F^{-1} [w] \subseteq u \land cls (J) (u) \subseteq F^{-1} [z]))) \to w \subseteq ran F$
37		funimass1	$⊢ (Fun F \land w \subseteq ran F) \to (F^{-1} [w] \subseteq u \to w \subseteq F [u])$
38	29 36 37	syl2anc	$⊢ (((J \in TopOn (X) \land J \in Nrm) \land (z \in KQ (J) \land w \in (Clsd (KQ (J)) \cap 𝒫 z))) \land (u \in J \land (F^{-1} [w] \subseteq u \land cls (J) (u) \subseteq F^{-1} [z]))) \to (F^{-1} [w] \subseteq u \to w \subseteq F [u])$
39	26 38	mpd	$⊢ (((J \in TopOn (X) \land J \in Nrm) \land (z \in KQ (J) \land w \in (Clsd (KQ (J)) \cap 𝒫 z))) \land (u \in J \land (F^{-1} [w] \subseteq u \land cls (J) (u) \subseteq F^{-1} [z]))) \to w \subseteq F [u]$
40		topontop	$⊢ J \in TopOn (X) \to J \in Top$
41	22 40	syl	$⊢ (((J \in TopOn (X) \land J \in Nrm) \land (z \in KQ (J) \land w \in (Clsd (KQ (J)) \cap 𝒫 z))) \land (u \in J \land (F^{-1} [w] \subseteq u \land cls (J) (u) \subseteq F^{-1} [z]))) \to J \in Top$
42		elssuni	$⊢ u \in J \to u \subseteq ⋃ J$
43	42	ad2antrl	$⊢ (((J \in TopOn (X) \land J \in Nrm) \land (z \in KQ (J) \land w \in (Clsd (KQ (J)) \cap 𝒫 z))) \land (u \in J \land (F^{-1} [w] \subseteq u \land cls (J) (u) \subseteq F^{-1} [z]))) \to u \subseteq ⋃ J$
44		eqid	$⊢ ⋃ J = ⋃ J$
45	44	clscld	$⊢ (J \in Top \land u \subseteq ⋃ J) \to cls (J) (u) \in Clsd (J)$
46	41 43 45	syl2anc	$⊢ (((J \in TopOn (X) \land J \in Nrm) \land (z \in KQ (J) \land w \in (Clsd (KQ (J)) \cap 𝒫 z))) \land (u \in J \land (F^{-1} [w] \subseteq u \land cls (J) (u) \subseteq F^{-1} [z]))) \to cls (J) (u) \in Clsd (J)$
47	1	kqcld	$⊢ (J \in TopOn (X) \land cls (J) (u) \in Clsd (J)) \to F [cls (J) (u)] \in Clsd (KQ (J))$
48	22 46 47	syl2anc	$⊢ (((J \in TopOn (X) \land J \in Nrm) \land (z \in KQ (J) \land w \in (Clsd (KQ (J)) \cap 𝒫 z))) \land (u \in J \land (F^{-1} [w] \subseteq u \land cls (J) (u) \subseteq F^{-1} [z]))) \to F [cls (J) (u)] \in Clsd (KQ (J))$
49	44	sscls	$⊢ (J \in Top \land u \subseteq ⋃ J) \to u \subseteq cls (J) (u)$
50	41 43 49	syl2anc	$⊢ (((J \in TopOn (X) \land J \in Nrm) \land (z \in KQ (J) \land w \in (Clsd (KQ (J)) \cap 𝒫 z))) \land (u \in J \land (F^{-1} [w] \subseteq u \land cls (J) (u) \subseteq F^{-1} [z]))) \to u \subseteq cls (J) (u)$
51		imass2	$⊢ u \subseteq cls (J) (u) \to F [u] \subseteq F [cls (J) (u)]$
52	50 51	syl	$⊢ (((J \in TopOn (X) \land J \in Nrm) \land (z \in KQ (J) \land w \in (Clsd (KQ (J)) \cap 𝒫 z))) \land (u \in J \land (F^{-1} [w] \subseteq u \land cls (J) (u) \subseteq F^{-1} [z]))) \to F [u] \subseteq F [cls (J) (u)]$
53	31	clsss2	$⊢ (F [cls (J) (u)] \in Clsd (KQ (J)) \land F [u] \subseteq F [cls (J) (u)]) \to cls (KQ (J)) (F [u]) \subseteq F [cls (J) (u)]$
54	48 52 53	syl2anc	$⊢ (((J \in TopOn (X) \land J \in Nrm) \land (z \in KQ (J) \land w \in (Clsd (KQ (J)) \cap 𝒫 z))) \land (u \in J \land (F^{-1} [w] \subseteq u \land cls (J) (u) \subseteq F^{-1} [z]))) \to cls (KQ (J)) (F [u]) \subseteq F [cls (J) (u)]$
55		simprrr	$⊢ (((J \in TopOn (X) \land J \in Nrm) \land (z \in KQ (J) \land w \in (Clsd (KQ (J)) \cap 𝒫 z))) \land (u \in J \land (F^{-1} [w] \subseteq u \land cls (J) (u) \subseteq F^{-1} [z]))) \to cls (J) (u) \subseteq F^{-1} [z]$
56	44	clsss3	$⊢ (J \in Top \land u \subseteq ⋃ J) \to cls (J) (u) \subseteq ⋃ J$
57	41 43 56	syl2anc	$⊢ (((J \in TopOn (X) \land J \in Nrm) \land (z \in KQ (J) \land w \in (Clsd (KQ (J)) \cap 𝒫 z))) \land (u \in J \land (F^{-1} [w] \subseteq u \land cls (J) (u) \subseteq F^{-1} [z]))) \to cls (J) (u) \subseteq ⋃ J$
58		fndm	$⊢ F Fn X \to dom F = X$
59	22 27 58	3syl	$⊢ (((J \in TopOn (X) \land J \in Nrm) \land (z \in KQ (J) \land w \in (Clsd (KQ (J)) \cap 𝒫 z))) \land (u \in J \land (F^{-1} [w] \subseteq u \land cls (J) (u) \subseteq F^{-1} [z]))) \to dom F = X$
60		toponuni	$⊢ J \in TopOn (X) \to X = ⋃ J$
61	22 60	syl	$⊢ (((J \in TopOn (X) \land J \in Nrm) \land (z \in KQ (J) \land w \in (Clsd (KQ (J)) \cap 𝒫 z))) \land (u \in J \land (F^{-1} [w] \subseteq u \land cls (J) (u) \subseteq F^{-1} [z]))) \to X = ⋃ J$
62	59 61	eqtrd	$⊢ (((J \in TopOn (X) \land J \in Nrm) \land (z \in KQ (J) \land w \in (Clsd (KQ (J)) \cap 𝒫 z))) \land (u \in J \land (F^{-1} [w] \subseteq u \land cls (J) (u) \subseteq F^{-1} [z]))) \to dom F = ⋃ J$
63	57 62	sseqtrrd	$⊢ (((J \in TopOn (X) \land J \in Nrm) \land (z \in KQ (J) \land w \in (Clsd (KQ (J)) \cap 𝒫 z))) \land (u \in J \land (F^{-1} [w] \subseteq u \land cls (J) (u) \subseteq F^{-1} [z]))) \to cls (J) (u) \subseteq dom F$
64		funimass3	$⊢ (Fun F \land cls (J) (u) \subseteq dom F) \to (F [cls (J) (u)] \subseteq z \leftrightarrow cls (J) (u) \subseteq F^{-1} [z])$
65	29 63 64	syl2anc	$⊢ (((J \in TopOn (X) \land J \in Nrm) \land (z \in KQ (J) \land w \in (Clsd (KQ (J)) \cap 𝒫 z))) \land (u \in J \land (F^{-1} [w] \subseteq u \land cls (J) (u) \subseteq F^{-1} [z]))) \to (F [cls (J) (u)] \subseteq z \leftrightarrow cls (J) (u) \subseteq F^{-1} [z])$
66	55 65	mpbird	$⊢ (((J \in TopOn (X) \land J \in Nrm) \land (z \in KQ (J) \land w \in (Clsd (KQ (J)) \cap 𝒫 z))) \land (u \in J \land (F^{-1} [w] \subseteq u \land cls (J) (u) \subseteq F^{-1} [z]))) \to F [cls (J) (u)] \subseteq z$
67	54 66	sstrd	$⊢ (((J \in TopOn (X) \land J \in Nrm) \land (z \in KQ (J) \land w \in (Clsd (KQ (J)) \cap 𝒫 z))) \land (u \in J \land (F^{-1} [w] \subseteq u \land cls (J) (u) \subseteq F^{-1} [z]))) \to cls (KQ (J)) (F [u]) \subseteq z$
68		sseq2	$⊢ m = F [u] \to (w \subseteq m \leftrightarrow w \subseteq F [u])$
69		fveq2	$⊢ m = F [u] \to cls (KQ (J)) (m) = cls (KQ (J)) (F [u])$
70	69	sseq1d	$⊢ m = F [u] \to (cls (KQ (J)) (m) \subseteq z \leftrightarrow cls (KQ (J)) (F [u]) \subseteq z)$
71	68 70	anbi12d	$⊢ m = F [u] \to ((w \subseteq m \land cls (KQ (J)) (m) \subseteq z) \leftrightarrow (w \subseteq F [u] \land cls (KQ (J)) (F [u]) \subseteq z))$
72	71	rspcev	$⊢ (F [u] \in KQ (J) \land (w \subseteq F [u] \land cls (KQ (J)) (F [u]) \subseteq z)) \to \exists m \in KQ (J) (w \subseteq m \land cls (KQ (J)) (m) \subseteq z)$
73	25 39 67 72	syl12anc	$⊢ (((J \in TopOn (X) \land J \in Nrm) \land (z \in KQ (J) \land w \in (Clsd (KQ (J)) \cap 𝒫 z))) \land (u \in J \land (F^{-1} [w] \subseteq u \land cls (J) (u) \subseteq F^{-1} [z]))) \to \exists m \in KQ (J) (w \subseteq m \land cls (KQ (J)) (m) \subseteq z)$
74	21 73	rexlimddv	$⊢ ((J \in TopOn (X) \land J \in Nrm) \land (z \in KQ (J) \land w \in (Clsd (KQ (J)) \cap 𝒫 z))) \to \exists m \in KQ (J) (w \subseteq m \land cls (KQ (J)) (m) \subseteq z)$
75	74	ralrimivva	$⊢ (J \in TopOn (X) \land J \in Nrm) \to \forall z \in KQ (J) \forall w \in (Clsd (KQ (J)) \cap 𝒫 z) \exists m \in KQ (J) (w \subseteq m \land cls (KQ (J)) (m) \subseteq z)$
76		isnrm	$⊢ KQ (J) \in Nrm \leftrightarrow (KQ (J) \in Top \land \forall z \in KQ (J) \forall w \in (Clsd (KQ (J)) \cap 𝒫 z) \exists m \in KQ (J) (w \subseteq m \land cls (KQ (J)) (m) \subseteq z))$
77	5 75 76	sylanbrc	$⊢ (J \in TopOn (X) \land J \in Nrm) \to KQ (J) \in Nrm$

Metamath Proof Explorer

Theorem kqnrmlem1

Proof