kqreglem2

Description: If the Kolmogorov quotient of a space is regular 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	kqreglem2	$⊢ (J \in TopOn (X) \land KQ (J) \in Reg) \to J \in Reg$

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 Reg) \to J \in Top$
4		simplr	$⊢ ((J \in TopOn (X) \land KQ (J) \in Reg) \land (z \in J \land w \in z)) \to KQ (J) \in Reg$
5		simpll	$⊢ ((J \in TopOn (X) \land KQ (J) \in Reg) \land (z \in J \land w \in z)) \to J \in TopOn (X)$
6		simprl	$⊢ ((J \in TopOn (X) \land KQ (J) \in Reg) \land (z \in J \land w \in 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 Reg) \land (z \in J \land w \in z)) \to F [z] \in KQ (J)$
9		simprr	$⊢ ((J \in TopOn (X) \land KQ (J) \in Reg) \land (z \in J \land w \in z)) \to w \in z$
10		toponss	$⊢ (J \in TopOn (X) \land z \in J) \to z \subseteq X$
11	5 6 10	syl2anc	$⊢ ((J \in TopOn (X) \land KQ (J) \in Reg) \land (z \in J \land w \in z)) \to z \subseteq X$
12	11 9	sseldd	$⊢ ((J \in TopOn (X) \land KQ (J) \in Reg) \land (z \in J \land w \in z)) \to w \in X$
13	1	kqfvima	$⊢ (J \in TopOn (X) \land z \in J \land w \in X) \to (w \in z \leftrightarrow F (w) \in F [z])$
14	5 6 12 13	syl3anc	$⊢ ((J \in TopOn (X) \land KQ (J) \in Reg) \land (z \in J \land w \in z)) \to (w \in z \leftrightarrow F (w) \in F [z])$
15	9 14	mpbid	$⊢ ((J \in TopOn (X) \land KQ (J) \in Reg) \land (z \in J \land w \in z)) \to F (w) \in F [z]$
16		regsep	$⊢ (KQ (J) \in Reg \land F [z] \in KQ (J) \land F (w) \in F [z]) \to \exists n \in KQ (J) (F (w) \in n \land cls (KQ (J)) (n) \subseteq F [z])$
17	4 8 15 16	syl3anc	$⊢ ((J \in TopOn (X) \land KQ (J) \in Reg) \land (z \in J \land w \in z)) \to \exists n \in KQ (J) (F (w) \in n \land cls (KQ (J)) (n) \subseteq F [z])$
18	5	adantr	$⊢ (((J \in TopOn (X) \land KQ (J) \in Reg) \land (z \in J \land w \in z)) \land (n \in KQ (J) \land (F (w) \in n \land cls (KQ (J)) (n) \subseteq F [z]))) \to J \in TopOn (X)$
19	1	kqid	$⊢ J \in TopOn (X) \to F \in (J Cn KQ (J))$
20	18 19	syl	$⊢ (((J \in TopOn (X) \land KQ (J) \in Reg) \land (z \in J \land w \in z)) \land (n \in KQ (J) \land (F (w) \in n \land cls (KQ (J)) (n) \subseteq F [z]))) \to F \in (J Cn KQ (J))$
21		simprl	$⊢ (((J \in TopOn (X) \land KQ (J) \in Reg) \land (z \in J \land w \in z)) \land (n \in KQ (J) \land (F (w) \in n \land cls (KQ (J)) (n) \subseteq F [z]))) \to n \in KQ (J)$
22		cnima	$⊢ (F \in (J Cn KQ (J)) \land n \in KQ (J)) \to F^{-1} [n] \in J$
23	20 21 22	syl2anc	$⊢ (((J \in TopOn (X) \land KQ (J) \in Reg) \land (z \in J \land w \in z)) \land (n \in KQ (J) \land (F (w) \in n \land cls (KQ (J)) (n) \subseteq F [z]))) \to F^{-1} [n] \in J$
24	12	adantr	$⊢ (((J \in TopOn (X) \land KQ (J) \in Reg) \land (z \in J \land w \in z)) \land (n \in KQ (J) \land (F (w) \in n \land cls (KQ (J)) (n) \subseteq F [z]))) \to w \in X$
25		simprrl	$⊢ (((J \in TopOn (X) \land KQ (J) \in Reg) \land (z \in J \land w \in z)) \land (n \in KQ (J) \land (F (w) \in n \land cls (KQ (J)) (n) \subseteq F [z]))) \to F (w) \in n$
26	1	kqffn	$⊢ J \in TopOn (X) \to F Fn X$
27		elpreima	$⊢ F Fn X \to (w \in F^{-1} [n] \leftrightarrow (w \in X \land F (w) \in n))$
28	18 26 27	3syl	$⊢ (((J \in TopOn (X) \land KQ (J) \in Reg) \land (z \in J \land w \in z)) \land (n \in KQ (J) \land (F (w) \in n \land cls (KQ (J)) (n) \subseteq F [z]))) \to (w \in F^{-1} [n] \leftrightarrow (w \in X \land F (w) \in n))$
29	24 25 28	mpbir2and	$⊢ (((J \in TopOn (X) \land KQ (J) \in Reg) \land (z \in J \land w \in z)) \land (n \in KQ (J) \land (F (w) \in n \land cls (KQ (J)) (n) \subseteq F [z]))) \to w \in F^{-1} [n]$
30	1	kqtopon	$⊢ J \in TopOn (X) \to KQ (J) \in TopOn (ran F)$
31		topontop	$⊢ KQ (J) \in TopOn (ran F) \to KQ (J) \in Top$
32	18 30 31	3syl	$⊢ (((J \in TopOn (X) \land KQ (J) \in Reg) \land (z \in J \land w \in z)) \land (n \in KQ (J) \land (F (w) \in n \land cls (KQ (J)) (n) \subseteq F [z]))) \to KQ (J) \in Top$
33		elssuni	$⊢ n \in KQ (J) \to n \subseteq ⋃ KQ (J)$
34	33	ad2antrl	$⊢ (((J \in TopOn (X) \land KQ (J) \in Reg) \land (z \in J \land w \in z)) \land (n \in KQ (J) \land (F (w) \in n \land cls (KQ (J)) (n) \subseteq F [z]))) \to n \subseteq ⋃ KQ (J)$
35		eqid	$⊢ ⋃ KQ (J) = ⋃ KQ (J)$
36	35	clscld	$⊢ (KQ (J) \in Top \land n \subseteq ⋃ KQ (J)) \to cls (KQ (J)) (n) \in Clsd (KQ (J))$
37	32 34 36	syl2anc	$⊢ (((J \in TopOn (X) \land KQ (J) \in Reg) \land (z \in J \land w \in z)) \land (n \in KQ (J) \land (F (w) \in n \land cls (KQ (J)) (n) \subseteq F [z]))) \to cls (KQ (J)) (n) \in Clsd (KQ (J))$
38		cnclima	$⊢ (F \in (J Cn KQ (J)) \land cls (KQ (J)) (n) \in Clsd (KQ (J))) \to F^{-1} [cls (KQ (J)) (n)] \in Clsd (J)$
39	20 37 38	syl2anc	$⊢ (((J \in TopOn (X) \land KQ (J) \in Reg) \land (z \in J \land w \in z)) \land (n \in KQ (J) \land (F (w) \in n \land cls (KQ (J)) (n) \subseteq F [z]))) \to F^{-1} [cls (KQ (J)) (n)] \in Clsd (J)$
40	35	sscls	$⊢ (KQ (J) \in Top \land n \subseteq ⋃ KQ (J)) \to n \subseteq cls (KQ (J)) (n)$
41	32 34 40	syl2anc	$⊢ (((J \in TopOn (X) \land KQ (J) \in Reg) \land (z \in J \land w \in z)) \land (n \in KQ (J) \land (F (w) \in n \land cls (KQ (J)) (n) \subseteq F [z]))) \to n \subseteq cls (KQ (J)) (n)$
42		imass2	$⊢ n \subseteq cls (KQ (J)) (n) \to F^{-1} [n] \subseteq F^{-1} [cls (KQ (J)) (n)]$
43	41 42	syl	$⊢ (((J \in TopOn (X) \land KQ (J) \in Reg) \land (z \in J \land w \in z)) \land (n \in KQ (J) \land (F (w) \in n \land cls (KQ (J)) (n) \subseteq F [z]))) \to F^{-1} [n] \subseteq F^{-1} [cls (KQ (J)) (n)]$
44		eqid	$⊢ ⋃ J = ⋃ J$
45	44	clsss2	$⊢ (F^{-1} [cls (KQ (J)) (n)] \in Clsd (J) \land F^{-1} [n] \subseteq F^{-1} [cls (KQ (J)) (n)]) \to cls (J) (F^{-1} [n]) \subseteq F^{-1} [cls (KQ (J)) (n)]$
46	39 43 45	syl2anc	$⊢ (((J \in TopOn (X) \land KQ (J) \in Reg) \land (z \in J \land w \in z)) \land (n \in KQ (J) \land (F (w) \in n \land cls (KQ (J)) (n) \subseteq F [z]))) \to cls (J) (F^{-1} [n]) \subseteq F^{-1} [cls (KQ (J)) (n)]$
47		simprrr	$⊢ (((J \in TopOn (X) \land KQ (J) \in Reg) \land (z \in J \land w \in z)) \land (n \in KQ (J) \land (F (w) \in n \land cls (KQ (J)) (n) \subseteq F [z]))) \to cls (KQ (J)) (n) \subseteq F [z]$
48		imass2	$⊢ cls (KQ (J)) (n) \subseteq F [z] \to F^{-1} [cls (KQ (J)) (n)] \subseteq F^{-1} [F [z]]$
49	47 48	syl	$⊢ (((J \in TopOn (X) \land KQ (J) \in Reg) \land (z \in J \land w \in z)) \land (n \in KQ (J) \land (F (w) \in n \land cls (KQ (J)) (n) \subseteq F [z]))) \to F^{-1} [cls (KQ (J)) (n)] \subseteq F^{-1} [F [z]]$
50	6	adantr	$⊢ (((J \in TopOn (X) \land KQ (J) \in Reg) \land (z \in J \land w \in z)) \land (n \in KQ (J) \land (F (w) \in n \land cls (KQ (J)) (n) \subseteq F [z]))) \to z \in J$
51	1	kqsat	$⊢ (J \in TopOn (X) \land z \in J) \to F^{-1} [F [z]] = z$
52	18 50 51	syl2anc	$⊢ (((J \in TopOn (X) \land KQ (J) \in Reg) \land (z \in J \land w \in z)) \land (n \in KQ (J) \land (F (w) \in n \land cls (KQ (J)) (n) \subseteq F [z]))) \to F^{-1} [F [z]] = z$
53	49 52	sseqtrd	$⊢ (((J \in TopOn (X) \land KQ (J) \in Reg) \land (z \in J \land w \in z)) \land (n \in KQ (J) \land (F (w) \in n \land cls (KQ (J)) (n) \subseteq F [z]))) \to F^{-1} [cls (KQ (J)) (n)] \subseteq z$
54	46 53	sstrd	$⊢ (((J \in TopOn (X) \land KQ (J) \in Reg) \land (z \in J \land w \in z)) \land (n \in KQ (J) \land (F (w) \in n \land cls (KQ (J)) (n) \subseteq F [z]))) \to cls (J) (F^{-1} [n]) \subseteq z$
55		eleq2	$⊢ m = F^{-1} [n] \to (w \in m \leftrightarrow w \in F^{-1} [n])$
56		fveq2	$⊢ m = F^{-1} [n] \to cls (J) (m) = cls (J) (F^{-1} [n])$
57	56	sseq1d	$⊢ m = F^{-1} [n] \to (cls (J) (m) \subseteq z \leftrightarrow cls (J) (F^{-1} [n]) \subseteq z)$
58	55 57	anbi12d	$⊢ m = F^{-1} [n] \to ((w \in m \land cls (J) (m) \subseteq z) \leftrightarrow (w \in F^{-1} [n] \land cls (J) (F^{-1} [n]) \subseteq z))$
59	58	rspcev	$⊢ (F^{-1} [n] \in J \land (w \in F^{-1} [n] \land cls (J) (F^{-1} [n]) \subseteq z)) \to \exists m \in J (w \in m \land cls (J) (m) \subseteq z)$
60	23 29 54 59	syl12anc	$⊢ (((J \in TopOn (X) \land KQ (J) \in Reg) \land (z \in J \land w \in z)) \land (n \in KQ (J) \land (F (w) \in n \land cls (KQ (J)) (n) \subseteq F [z]))) \to \exists m \in J (w \in m \land cls (J) (m) \subseteq z)$
61	17 60	rexlimddv	$⊢ ((J \in TopOn (X) \land KQ (J) \in Reg) \land (z \in J \land w \in z)) \to \exists m \in J (w \in m \land cls (J) (m) \subseteq z)$
62	61	ralrimivva	$⊢ (J \in TopOn (X) \land KQ (J) \in Reg) \to \forall z \in J \forall w \in z \exists m \in J (w \in m \land cls (J) (m) \subseteq z)$
63		isreg	$⊢ J \in Reg \leftrightarrow (J \in Top \land \forall z \in J \forall w \in z \exists m \in J (w \in m \land cls (J) (m) \subseteq z))$
64	3 62 63	sylanbrc	$⊢ (J \in TopOn (X) \land KQ (J) \in Reg) \to J \in Reg$

Metamath Proof Explorer

Theorem kqreglem2

Proof