regr1lem2

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

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

Proof

Step	Hyp	Ref	Expression
1		kqval.2	$⊢ F = (x \in X ⟼ \{y \in J \| x \in y\})$
2		simplll	$⊢ (((J \in TopOn (X) \land J \in Reg) \land (z \in X \land w \in X)) \land (a \in J \land \neg \exists m \in KQ (J) \exists n \in KQ (J) (F (z) \in m \land F (w) \in n \land m \cap n = \emptyset))) \to J \in TopOn (X)$
3		simpllr	$⊢ (((J \in TopOn (X) \land J \in Reg) \land (z \in X \land w \in X)) \land (a \in J \land \neg \exists m \in KQ (J) \exists n \in KQ (J) (F (z) \in m \land F (w) \in n \land m \cap n = \emptyset))) \to J \in Reg$
4		simplrl	$⊢ (((J \in TopOn (X) \land J \in Reg) \land (z \in X \land w \in X)) \land (a \in J \land \neg \exists m \in KQ (J) \exists n \in KQ (J) (F (z) \in m \land F (w) \in n \land m \cap n = \emptyset))) \to z \in X$
5		simplrr	$⊢ (((J \in TopOn (X) \land J \in Reg) \land (z \in X \land w \in X)) \land (a \in J \land \neg \exists m \in KQ (J) \exists n \in KQ (J) (F (z) \in m \land F (w) \in n \land m \cap n = \emptyset))) \to w \in X$
6		simprl	$⊢ (((J \in TopOn (X) \land J \in Reg) \land (z \in X \land w \in X)) \land (a \in J \land \neg \exists m \in KQ (J) \exists n \in KQ (J) (F (z) \in m \land F (w) \in n \land m \cap n = \emptyset))) \to a \in J$
7		simprr	$⊢ (((J \in TopOn (X) \land J \in Reg) \land (z \in X \land w \in X)) \land (a \in J \land \neg \exists m \in KQ (J) \exists n \in KQ (J) (F (z) \in m \land F (w) \in n \land m \cap n = \emptyset))) \to \neg \exists m \in KQ (J) \exists n \in KQ (J) (F (z) \in m \land F (w) \in n \land m \cap n = \emptyset)$
8	1 2 3 4 5 6 7	regr1lem	$⊢ (((J \in TopOn (X) \land J \in Reg) \land (z \in X \land w \in X)) \land (a \in J \land \neg \exists m \in KQ (J) \exists n \in KQ (J) (F (z) \in m \land F (w) \in n \land m \cap n = \emptyset))) \to (z \in a \to w \in a)$
9		3ancoma	$⊢ (F (z) \in m \land F (w) \in n \land m \cap n = \emptyset) \leftrightarrow (F (w) \in n \land F (z) \in m \land m \cap n = \emptyset)$
10		incom	$⊢ m \cap n = n \cap m$
11	10	eqeq1i	$⊢ m \cap n = \emptyset \leftrightarrow n \cap m = \emptyset$
12	11	3anbi3i	$⊢ (F (w) \in n \land F (z) \in m \land m \cap n = \emptyset) \leftrightarrow (F (w) \in n \land F (z) \in m \land n \cap m = \emptyset)$
13	9 12	bitri	$⊢ (F (z) \in m \land F (w) \in n \land m \cap n = \emptyset) \leftrightarrow (F (w) \in n \land F (z) \in m \land n \cap m = \emptyset)$
14	13	2rexbii	$⊢ \exists m \in KQ (J) \exists n \in KQ (J) (F (z) \in m \land F (w) \in n \land m \cap n = \emptyset) \leftrightarrow \exists m \in KQ (J) \exists n \in KQ (J) (F (w) \in n \land F (z) \in m \land n \cap m = \emptyset)$
15		rexcom	$⊢ \exists m \in KQ (J) \exists n \in KQ (J) (F (w) \in n \land F (z) \in m \land n \cap m = \emptyset) \leftrightarrow \exists n \in KQ (J) \exists m \in KQ (J) (F (w) \in n \land F (z) \in m \land n \cap m = \emptyset)$
16	14 15	bitri	$⊢ \exists m \in KQ (J) \exists n \in KQ (J) (F (z) \in m \land F (w) \in n \land m \cap n = \emptyset) \leftrightarrow \exists n \in KQ (J) \exists m \in KQ (J) (F (w) \in n \land F (z) \in m \land n \cap m = \emptyset)$
17	7 16	sylnib	$⊢ (((J \in TopOn (X) \land J \in Reg) \land (z \in X \land w \in X)) \land (a \in J \land \neg \exists m \in KQ (J) \exists n \in KQ (J) (F (z) \in m \land F (w) \in n \land m \cap n = \emptyset))) \to \neg \exists n \in KQ (J) \exists m \in KQ (J) (F (w) \in n \land F (z) \in m \land n \cap m = \emptyset)$
18	1 2 3 5 4 6 17	regr1lem	$⊢ (((J \in TopOn (X) \land J \in Reg) \land (z \in X \land w \in X)) \land (a \in J \land \neg \exists m \in KQ (J) \exists n \in KQ (J) (F (z) \in m \land F (w) \in n \land m \cap n = \emptyset))) \to (w \in a \to z \in a)$
19	8 18	impbid	$⊢ (((J \in TopOn (X) \land J \in Reg) \land (z \in X \land w \in X)) \land (a \in J \land \neg \exists m \in KQ (J) \exists n \in KQ (J) (F (z) \in m \land F (w) \in n \land m \cap n = \emptyset))) \to (z \in a \leftrightarrow w \in a)$
20	19	expr	$⊢ (((J \in TopOn (X) \land J \in Reg) \land (z \in X \land w \in X)) \land a \in J) \to (\neg \exists m \in KQ (J) \exists n \in KQ (J) (F (z) \in m \land F (w) \in n \land m \cap n = \emptyset) \to (z \in a \leftrightarrow w \in a))$
21	20	ralrimdva	$⊢ ((J \in TopOn (X) \land J \in Reg) \land (z \in X \land w \in X)) \to (\neg \exists m \in KQ (J) \exists n \in KQ (J) (F (z) \in m \land F (w) \in n \land m \cap n = \emptyset) \to \forall a \in J (z \in a \leftrightarrow w \in a))$
22	1	kqfeq	$⊢ (J \in TopOn (X) \land z \in X \land w \in X) \to (F (z) = F (w) \leftrightarrow \forall y \in J (z \in y \leftrightarrow w \in y))$
23		elequ2	$⊢ y = a \to (z \in y \leftrightarrow z \in a)$
24		elequ2	$⊢ y = a \to (w \in y \leftrightarrow w \in a)$
25	23 24	bibi12d	$⊢ y = a \to ((z \in y \leftrightarrow w \in y) \leftrightarrow (z \in a \leftrightarrow w \in a))$
26	25	cbvralvw	$⊢ \forall y \in J (z \in y \leftrightarrow w \in y) \leftrightarrow \forall a \in J (z \in a \leftrightarrow w \in a)$
27	22 26	bitrdi	$⊢ (J \in TopOn (X) \land z \in X \land w \in X) \to (F (z) = F (w) \leftrightarrow \forall a \in J (z \in a \leftrightarrow w \in a))$
28	27	3expb	$⊢ (J \in TopOn (X) \land (z \in X \land w \in X)) \to (F (z) = F (w) \leftrightarrow \forall a \in J (z \in a \leftrightarrow w \in a))$
29	28	adantlr	$⊢ ((J \in TopOn (X) \land J \in Reg) \land (z \in X \land w \in X)) \to (F (z) = F (w) \leftrightarrow \forall a \in J (z \in a \leftrightarrow w \in a))$
30	21 29	sylibrd	$⊢ ((J \in TopOn (X) \land J \in Reg) \land (z \in X \land w \in X)) \to (\neg \exists m \in KQ (J) \exists n \in KQ (J) (F (z) \in m \land F (w) \in n \land m \cap n = \emptyset) \to F (z) = F (w))$
31	30	necon1ad	$⊢ ((J \in TopOn (X) \land J \in Reg) \land (z \in X \land w \in X)) \to (F (z) \neq F (w) \to \exists m \in KQ (J) \exists n \in KQ (J) (F (z) \in m \land F (w) \in n \land m \cap n = \emptyset))$
32	31	ralrimivva	$⊢ (J \in TopOn (X) \land J \in Reg) \to \forall z \in X \forall w \in X (F (z) \neq F (w) \to \exists m \in KQ (J) \exists n \in KQ (J) (F (z) \in m \land F (w) \in n \land m \cap n = \emptyset))$
33	1	kqffn	$⊢ J \in TopOn (X) \to F Fn X$
34	33	adantr	$⊢ (J \in TopOn (X) \land J \in Reg) \to F Fn X$
35		neeq1	$⊢ a = F (z) \to (a \neq b \leftrightarrow F (z) \neq b)$
36		eleq1	$⊢ a = F (z) \to (a \in m \leftrightarrow F (z) \in m)$
37	36	3anbi1d	$⊢ a = F (z) \to ((a \in m \land b \in n \land m \cap n = \emptyset) \leftrightarrow (F (z) \in m \land b \in n \land m \cap n = \emptyset))$
38	37	2rexbidv	$⊢ a = F (z) \to (\exists m \in KQ (J) \exists n \in KQ (J) (a \in m \land b \in n \land m \cap n = \emptyset) \leftrightarrow \exists m \in KQ (J) \exists n \in KQ (J) (F (z) \in m \land b \in n \land m \cap n = \emptyset))$
39	35 38	imbi12d	$⊢ a = F (z) \to ((a \neq b \to \exists m \in KQ (J) \exists n \in KQ (J) (a \in m \land b \in n \land m \cap n = \emptyset)) \leftrightarrow (F (z) \neq b \to \exists m \in KQ (J) \exists n \in KQ (J) (F (z) \in m \land b \in n \land m \cap n = \emptyset)))$
40	39	ralbidv	$⊢ a = F (z) \to (\forall b \in ran F (a \neq b \to \exists m \in KQ (J) \exists n \in KQ (J) (a \in m \land b \in n \land m \cap n = \emptyset)) \leftrightarrow \forall b \in ran F (F (z) \neq b \to \exists m \in KQ (J) \exists n \in KQ (J) (F (z) \in m \land b \in n \land m \cap n = \emptyset)))$
41	40	ralrn	$⊢ F Fn X \to (\forall a \in ran F \forall b \in ran F (a \neq b \to \exists m \in KQ (J) \exists n \in KQ (J) (a \in m \land b \in n \land m \cap n = \emptyset)) \leftrightarrow \forall z \in X \forall b \in ran F (F (z) \neq b \to \exists m \in KQ (J) \exists n \in KQ (J) (F (z) \in m \land b \in n \land m \cap n = \emptyset)))$
42		neeq2	$⊢ b = F (w) \to (F (z) \neq b \leftrightarrow F (z) \neq F (w))$
43		eleq1	$⊢ b = F (w) \to (b \in n \leftrightarrow F (w) \in n)$
44	43	3anbi2d	$⊢ b = F (w) \to ((F (z) \in m \land b \in n \land m \cap n = \emptyset) \leftrightarrow (F (z) \in m \land F (w) \in n \land m \cap n = \emptyset))$
45	44	2rexbidv	$⊢ b = F (w) \to (\exists m \in KQ (J) \exists n \in KQ (J) (F (z) \in m \land b \in n \land m \cap n = \emptyset) \leftrightarrow \exists m \in KQ (J) \exists n \in KQ (J) (F (z) \in m \land F (w) \in n \land m \cap n = \emptyset))$
46	42 45	imbi12d	$⊢ b = F (w) \to ((F (z) \neq b \to \exists m \in KQ (J) \exists n \in KQ (J) (F (z) \in m \land b \in n \land m \cap n = \emptyset)) \leftrightarrow (F (z) \neq F (w) \to \exists m \in KQ (J) \exists n \in KQ (J) (F (z) \in m \land F (w) \in n \land m \cap n = \emptyset)))$
47	46	ralrn	$⊢ F Fn X \to (\forall b \in ran F (F (z) \neq b \to \exists m \in KQ (J) \exists n \in KQ (J) (F (z) \in m \land b \in n \land m \cap n = \emptyset)) \leftrightarrow \forall w \in X (F (z) \neq F (w) \to \exists m \in KQ (J) \exists n \in KQ (J) (F (z) \in m \land F (w) \in n \land m \cap n = \emptyset)))$
48	47	ralbidv	$⊢ F Fn X \to (\forall z \in X \forall b \in ran F (F (z) \neq b \to \exists m \in KQ (J) \exists n \in KQ (J) (F (z) \in m \land b \in n \land m \cap n = \emptyset)) \leftrightarrow \forall z \in X \forall w \in X (F (z) \neq F (w) \to \exists m \in KQ (J) \exists n \in KQ (J) (F (z) \in m \land F (w) \in n \land m \cap n = \emptyset)))$
49	41 48	bitrd	$⊢ F Fn X \to (\forall a \in ran F \forall b \in ran F (a \neq b \to \exists m \in KQ (J) \exists n \in KQ (J) (a \in m \land b \in n \land m \cap n = \emptyset)) \leftrightarrow \forall z \in X \forall w \in X (F (z) \neq F (w) \to \exists m \in KQ (J) \exists n \in KQ (J) (F (z) \in m \land F (w) \in n \land m \cap n = \emptyset)))$
50	34 49	syl	$⊢ (J \in TopOn (X) \land J \in Reg) \to (\forall a \in ran F \forall b \in ran F (a \neq b \to \exists m \in KQ (J) \exists n \in KQ (J) (a \in m \land b \in n \land m \cap n = \emptyset)) \leftrightarrow \forall z \in X \forall w \in X (F (z) \neq F (w) \to \exists m \in KQ (J) \exists n \in KQ (J) (F (z) \in m \land F (w) \in n \land m \cap n = \emptyset)))$
51	32 50	mpbird	$⊢ (J \in TopOn (X) \land J \in Reg) \to \forall a \in ran F \forall b \in ran F (a \neq b \to \exists m \in KQ (J) \exists n \in KQ (J) (a \in m \land b \in n \land m \cap n = \emptyset))$
52	1	kqtopon	$⊢ J \in TopOn (X) \to KQ (J) \in TopOn (ran F)$
53	52	adantr	$⊢ (J \in TopOn (X) \land J \in Reg) \to KQ (J) \in TopOn (ran F)$
54		ishaus2	$⊢ KQ (J) \in TopOn (ran F) \to (KQ (J) \in Haus \leftrightarrow \forall a \in ran F \forall b \in ran F (a \neq b \to \exists m \in KQ (J) \exists n \in KQ (J) (a \in m \land b \in n \land m \cap n = \emptyset)))$
55	53 54	syl	$⊢ (J \in TopOn (X) \land J \in Reg) \to (KQ (J) \in Haus \leftrightarrow \forall a \in ran F \forall b \in ran F (a \neq b \to \exists m \in KQ (J) \exists n \in KQ (J) (a \in m \land b \in n \land m \cap n = \emptyset)))$
56	51 55	mpbird	$⊢ (J \in TopOn (X) \land J \in Reg) \to KQ (J) \in Haus$

Metamath Proof Explorer

Theorem regr1lem2

Proof