kqreglem1

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

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

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 Reg) \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 Reg) \to KQ (J) \in Top$
6		toponss	$⊢ (KQ (J) \in TopOn (ran F) \land a \in KQ (J)) \to a \subseteq ran F$
7	3 6	sylan	$⊢ ((J \in TopOn (X) \land J \in Reg) \land a \in KQ (J)) \to a \subseteq ran F$
8	7	sselda	$⊢ (((J \in TopOn (X) \land J \in Reg) \land a \in KQ (J)) \land b \in a) \to b \in ran F$
9	1	kqffn	$⊢ J \in TopOn (X) \to F Fn X$
10	9	ad3antrrr	$⊢ (((J \in TopOn (X) \land J \in Reg) \land a \in KQ (J)) \land b \in a) \to F Fn X$
11		fvelrnb	$⊢ F Fn X \to (b \in ran F \leftrightarrow \exists z \in X F (z) = b)$
12	10 11	syl	$⊢ (((J \in TopOn (X) \land J \in Reg) \land a \in KQ (J)) \land b \in a) \to (b \in ran F \leftrightarrow \exists z \in X F (z) = b)$
13	8 12	mpbid	$⊢ (((J \in TopOn (X) \land J \in Reg) \land a \in KQ (J)) \land b \in a) \to \exists z \in X F (z) = b$
14		simpllr	$⊢ (((J \in TopOn (X) \land J \in Reg) \land a \in KQ (J)) \land (z \in X \land F (z) \in a)) \to J \in Reg$
15	1	kqid	$⊢ J \in TopOn (X) \to F \in (J Cn KQ (J))$
16	15	ad3antrrr	$⊢ (((J \in TopOn (X) \land J \in Reg) \land a \in KQ (J)) \land (z \in X \land F (z) \in a)) \to F \in (J Cn KQ (J))$
17		simplr	$⊢ (((J \in TopOn (X) \land J \in Reg) \land a \in KQ (J)) \land (z \in X \land F (z) \in a)) \to a \in KQ (J)$
18		cnima	$⊢ (F \in (J Cn KQ (J)) \land a \in KQ (J)) \to F^{-1} [a] \in J$
19	16 17 18	syl2anc	$⊢ (((J \in TopOn (X) \land J \in Reg) \land a \in KQ (J)) \land (z \in X \land F (z) \in a)) \to F^{-1} [a] \in J$
20	9	adantr	$⊢ (J \in TopOn (X) \land J \in Reg) \to F Fn X$
21	20	adantr	$⊢ ((J \in TopOn (X) \land J \in Reg) \land a \in KQ (J)) \to F Fn X$
22		elpreima	$⊢ F Fn X \to (z \in F^{-1} [a] \leftrightarrow (z \in X \land F (z) \in a))$
23	21 22	syl	$⊢ ((J \in TopOn (X) \land J \in Reg) \land a \in KQ (J)) \to (z \in F^{-1} [a] \leftrightarrow (z \in X \land F (z) \in a))$
24	23	biimpar	$⊢ (((J \in TopOn (X) \land J \in Reg) \land a \in KQ (J)) \land (z \in X \land F (z) \in a)) \to z \in F^{-1} [a]$
25		regsep	$⊢ (J \in Reg \land F^{-1} [a] \in J \land z \in F^{-1} [a]) \to \exists w \in J (z \in w \land cls (J) (w) \subseteq F^{-1} [a])$
26	14 19 24 25	syl3anc	$⊢ (((J \in TopOn (X) \land J \in Reg) \land a \in KQ (J)) \land (z \in X \land F (z) \in a)) \to \exists w \in J (z \in w \land cls (J) (w) \subseteq F^{-1} [a])$
27		simp-4l	$⊢ ((((J \in TopOn (X) \land J \in Reg) \land a \in KQ (J)) \land (z \in X \land F (z) \in a)) \land (w \in J \land (z \in w \land cls (J) (w) \subseteq F^{-1} [a]))) \to J \in TopOn (X)$
28		simprl	$⊢ ((((J \in TopOn (X) \land J \in Reg) \land a \in KQ (J)) \land (z \in X \land F (z) \in a)) \land (w \in J \land (z \in w \land cls (J) (w) \subseteq F^{-1} [a]))) \to w \in J$
29	1	kqopn	$⊢ (J \in TopOn (X) \land w \in J) \to F [w] \in KQ (J)$
30	27 28 29	syl2anc	$⊢ ((((J \in TopOn (X) \land J \in Reg) \land a \in KQ (J)) \land (z \in X \land F (z) \in a)) \land (w \in J \land (z \in w \land cls (J) (w) \subseteq F^{-1} [a]))) \to F [w] \in KQ (J)$
31		simprrl	$⊢ ((((J \in TopOn (X) \land J \in Reg) \land a \in KQ (J)) \land (z \in X \land F (z) \in a)) \land (w \in J \land (z \in w \land cls (J) (w) \subseteq F^{-1} [a]))) \to z \in w$
32		simplrl	$⊢ ((((J \in TopOn (X) \land J \in Reg) \land a \in KQ (J)) \land (z \in X \land F (z) \in a)) \land (w \in J \land (z \in w \land cls (J) (w) \subseteq F^{-1} [a]))) \to z \in X$
33	1	kqfvima	$⊢ (J \in TopOn (X) \land w \in J \land z \in X) \to (z \in w \leftrightarrow F (z) \in F [w])$
34	27 28 32 33	syl3anc	$⊢ ((((J \in TopOn (X) \land J \in Reg) \land a \in KQ (J)) \land (z \in X \land F (z) \in a)) \land (w \in J \land (z \in w \land cls (J) (w) \subseteq F^{-1} [a]))) \to (z \in w \leftrightarrow F (z) \in F [w])$
35	31 34	mpbid	$⊢ ((((J \in TopOn (X) \land J \in Reg) \land a \in KQ (J)) \land (z \in X \land F (z) \in a)) \land (w \in J \land (z \in w \land cls (J) (w) \subseteq F^{-1} [a]))) \to F (z) \in F [w]$
36		topontop	$⊢ J \in TopOn (X) \to J \in Top$
37	27 36	syl	$⊢ ((((J \in TopOn (X) \land J \in Reg) \land a \in KQ (J)) \land (z \in X \land F (z) \in a)) \land (w \in J \land (z \in w \land cls (J) (w) \subseteq F^{-1} [a]))) \to J \in Top$
38		elssuni	$⊢ w \in J \to w \subseteq ⋃ J$
39	38	ad2antrl	$⊢ ((((J \in TopOn (X) \land J \in Reg) \land a \in KQ (J)) \land (z \in X \land F (z) \in a)) \land (w \in J \land (z \in w \land cls (J) (w) \subseteq F^{-1} [a]))) \to w \subseteq ⋃ J$
40		eqid	$⊢ ⋃ J = ⋃ J$
41	40	clscld	$⊢ (J \in Top \land w \subseteq ⋃ J) \to cls (J) (w) \in Clsd (J)$
42	37 39 41	syl2anc	$⊢ ((((J \in TopOn (X) \land J \in Reg) \land a \in KQ (J)) \land (z \in X \land F (z) \in a)) \land (w \in J \land (z \in w \land cls (J) (w) \subseteq F^{-1} [a]))) \to cls (J) (w) \in Clsd (J)$
43	1	kqcld	$⊢ (J \in TopOn (X) \land cls (J) (w) \in Clsd (J)) \to F [cls (J) (w)] \in Clsd (KQ (J))$
44	27 42 43	syl2anc	$⊢ ((((J \in TopOn (X) \land J \in Reg) \land a \in KQ (J)) \land (z \in X \land F (z) \in a)) \land (w \in J \land (z \in w \land cls (J) (w) \subseteq F^{-1} [a]))) \to F [cls (J) (w)] \in Clsd (KQ (J))$
45	40	sscls	$⊢ (J \in Top \land w \subseteq ⋃ J) \to w \subseteq cls (J) (w)$
46	37 39 45	syl2anc	$⊢ ((((J \in TopOn (X) \land J \in Reg) \land a \in KQ (J)) \land (z \in X \land F (z) \in a)) \land (w \in J \land (z \in w \land cls (J) (w) \subseteq F^{-1} [a]))) \to w \subseteq cls (J) (w)$
47		imass2	$⊢ w \subseteq cls (J) (w) \to F [w] \subseteq F [cls (J) (w)]$
48	46 47	syl	$⊢ ((((J \in TopOn (X) \land J \in Reg) \land a \in KQ (J)) \land (z \in X \land F (z) \in a)) \land (w \in J \land (z \in w \land cls (J) (w) \subseteq F^{-1} [a]))) \to F [w] \subseteq F [cls (J) (w)]$
49		eqid	$⊢ ⋃ KQ (J) = ⋃ KQ (J)$
50	49	clsss2	$⊢ (F [cls (J) (w)] \in Clsd (KQ (J)) \land F [w] \subseteq F [cls (J) (w)]) \to cls (KQ (J)) (F [w]) \subseteq F [cls (J) (w)]$
51	44 48 50	syl2anc	$⊢ ((((J \in TopOn (X) \land J \in Reg) \land a \in KQ (J)) \land (z \in X \land F (z) \in a)) \land (w \in J \land (z \in w \land cls (J) (w) \subseteq F^{-1} [a]))) \to cls (KQ (J)) (F [w]) \subseteq F [cls (J) (w)]$
52	20	ad3antrrr	$⊢ ((((J \in TopOn (X) \land J \in Reg) \land a \in KQ (J)) \land (z \in X \land F (z) \in a)) \land (w \in J \land (z \in w \land cls (J) (w) \subseteq F^{-1} [a]))) \to F Fn X$
53		fnfun	$⊢ F Fn X \to Fun F$
54	52 53	syl	$⊢ ((((J \in TopOn (X) \land J \in Reg) \land a \in KQ (J)) \land (z \in X \land F (z) \in a)) \land (w \in J \land (z \in w \land cls (J) (w) \subseteq F^{-1} [a]))) \to Fun F$
55		simprrr	$⊢ ((((J \in TopOn (X) \land J \in Reg) \land a \in KQ (J)) \land (z \in X \land F (z) \in a)) \land (w \in J \land (z \in w \land cls (J) (w) \subseteq F^{-1} [a]))) \to cls (J) (w) \subseteq F^{-1} [a]$
56		funimass2	$⊢ (Fun F \land cls (J) (w) \subseteq F^{-1} [a]) \to F [cls (J) (w)] \subseteq a$
57	54 55 56	syl2anc	$⊢ ((((J \in TopOn (X) \land J \in Reg) \land a \in KQ (J)) \land (z \in X \land F (z) \in a)) \land (w \in J \land (z \in w \land cls (J) (w) \subseteq F^{-1} [a]))) \to F [cls (J) (w)] \subseteq a$
58	51 57	sstrd	$⊢ ((((J \in TopOn (X) \land J \in Reg) \land a \in KQ (J)) \land (z \in X \land F (z) \in a)) \land (w \in J \land (z \in w \land cls (J) (w) \subseteq F^{-1} [a]))) \to cls (KQ (J)) (F [w]) \subseteq a$
59		eleq2	$⊢ m = F [w] \to (F (z) \in m \leftrightarrow F (z) \in F [w])$
60		fveq2	$⊢ m = F [w] \to cls (KQ (J)) (m) = cls (KQ (J)) (F [w])$
61	60	sseq1d	$⊢ m = F [w] \to (cls (KQ (J)) (m) \subseteq a \leftrightarrow cls (KQ (J)) (F [w]) \subseteq a)$
62	59 61	anbi12d	$⊢ m = F [w] \to ((F (z) \in m \land cls (KQ (J)) (m) \subseteq a) \leftrightarrow (F (z) \in F [w] \land cls (KQ (J)) (F [w]) \subseteq a))$
63	62	rspcev	$⊢ (F [w] \in KQ (J) \land (F (z) \in F [w] \land cls (KQ (J)) (F [w]) \subseteq a)) \to \exists m \in KQ (J) (F (z) \in m \land cls (KQ (J)) (m) \subseteq a)$
64	30 35 58 63	syl12anc	$⊢ ((((J \in TopOn (X) \land J \in Reg) \land a \in KQ (J)) \land (z \in X \land F (z) \in a)) \land (w \in J \land (z \in w \land cls (J) (w) \subseteq F^{-1} [a]))) \to \exists m \in KQ (J) (F (z) \in m \land cls (KQ (J)) (m) \subseteq a)$
65	26 64	rexlimddv	$⊢ (((J \in TopOn (X) \land J \in Reg) \land a \in KQ (J)) \land (z \in X \land F (z) \in a)) \to \exists m \in KQ (J) (F (z) \in m \land cls (KQ (J)) (m) \subseteq a)$
66	65	expr	$⊢ (((J \in TopOn (X) \land J \in Reg) \land a \in KQ (J)) \land z \in X) \to (F (z) \in a \to \exists m \in KQ (J) (F (z) \in m \land cls (KQ (J)) (m) \subseteq a))$
67		eleq1	$⊢ F (z) = b \to (F (z) \in a \leftrightarrow b \in a)$
68		eleq1	$⊢ F (z) = b \to (F (z) \in m \leftrightarrow b \in m)$
69	68	anbi1d	$⊢ F (z) = b \to ((F (z) \in m \land cls (KQ (J)) (m) \subseteq a) \leftrightarrow (b \in m \land cls (KQ (J)) (m) \subseteq a))$
70	69	rexbidv	$⊢ F (z) = b \to (\exists m \in KQ (J) (F (z) \in m \land cls (KQ (J)) (m) \subseteq a) \leftrightarrow \exists m \in KQ (J) (b \in m \land cls (KQ (J)) (m) \subseteq a))$
71	67 70	imbi12d	$⊢ F (z) = b \to ((F (z) \in a \to \exists m \in KQ (J) (F (z) \in m \land cls (KQ (J)) (m) \subseteq a)) \leftrightarrow (b \in a \to \exists m \in KQ (J) (b \in m \land cls (KQ (J)) (m) \subseteq a)))$
72	66 71	syl5ibcom	$⊢ (((J \in TopOn (X) \land J \in Reg) \land a \in KQ (J)) \land z \in X) \to (F (z) = b \to (b \in a \to \exists m \in KQ (J) (b \in m \land cls (KQ (J)) (m) \subseteq a)))$
73	72	com23	$⊢ (((J \in TopOn (X) \land J \in Reg) \land a \in KQ (J)) \land z \in X) \to (b \in a \to (F (z) = b \to \exists m \in KQ (J) (b \in m \land cls (KQ (J)) (m) \subseteq a)))$
74	73	imp	$⊢ ((((J \in TopOn (X) \land J \in Reg) \land a \in KQ (J)) \land z \in X) \land b \in a) \to (F (z) = b \to \exists m \in KQ (J) (b \in m \land cls (KQ (J)) (m) \subseteq a))$
75	74	an32s	$⊢ ((((J \in TopOn (X) \land J \in Reg) \land a \in KQ (J)) \land b \in a) \land z \in X) \to (F (z) = b \to \exists m \in KQ (J) (b \in m \land cls (KQ (J)) (m) \subseteq a))$
76	75	rexlimdva	$⊢ (((J \in TopOn (X) \land J \in Reg) \land a \in KQ (J)) \land b \in a) \to (\exists z \in X F (z) = b \to \exists m \in KQ (J) (b \in m \land cls (KQ (J)) (m) \subseteq a))$
77	13 76	mpd	$⊢ (((J \in TopOn (X) \land J \in Reg) \land a \in KQ (J)) \land b \in a) \to \exists m \in KQ (J) (b \in m \land cls (KQ (J)) (m) \subseteq a)$
78	77	anasss	$⊢ ((J \in TopOn (X) \land J \in Reg) \land (a \in KQ (J) \land b \in a)) \to \exists m \in KQ (J) (b \in m \land cls (KQ (J)) (m) \subseteq a)$
79	78	ralrimivva	$⊢ (J \in TopOn (X) \land J \in Reg) \to \forall a \in KQ (J) \forall b \in a \exists m \in KQ (J) (b \in m \land cls (KQ (J)) (m) \subseteq a)$
80		isreg	$⊢ KQ (J) \in Reg \leftrightarrow (KQ (J) \in Top \land \forall a \in KQ (J) \forall b \in a \exists m \in KQ (J) (b \in m \land cls (KQ (J)) (m) \subseteq a))$
81	5 79 80	sylanbrc	$⊢ (J \in TopOn (X) \land J \in Reg) \to KQ (J) \in Reg$

Metamath Proof Explorer

Theorem kqreglem1

Proof