kqnrmlem2

Description: If the Kolmogorov quotient of a space is normal then so is the original space. (Contributed by Mario Carneiro, 25-Aug-2015)

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

Proof

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

Metamath Proof Explorer

Theorem kqnrmlem2

Proof