utopreg

Description: All Hausdorff uniform spaces are regular. Proposition 3 of BourbakiTop1 p. II.5. (Contributed by Thierry Arnoux, 16-Jan-2018)

		Ref	Expression
	Hypothesis	utopreg.1	$⊢ J = unifTop (U)$
	Assertion	utopreg	$⊢ (U \in UnifOn (X) \land J \in Haus) \to J \in Reg$

Proof

Step	Hyp	Ref	Expression
1		utopreg.1	$⊢ J = unifTop (U)$
2		utoptop	$⊢ U \in UnifOn (X) \to unifTop (U) \in Top$
3	2	adantr	$⊢ (U \in UnifOn (X) \land J \in Haus) \to unifTop (U) \in Top$
4	1 3	eqeltrid	$⊢ (U \in UnifOn (X) \land J \in Haus) \to J \in Top$
5		simp-4l	$⊢ (((((((U \in UnifOn (X) \land J \in Haus) \land a \in J) \land x \in a) \land v \in U) \land a = v [\{x\}]) \land w \in U) \land (w^{-1} = w \land w \circ (w \circ w) \subseteq v)) \to (((U \in UnifOn (X) \land J \in Haus) \land a \in J) \land x \in a)$
6	4	ad2antrr	$⊢ (((U \in UnifOn (X) \land J \in Haus) \land a \in J) \land x \in a) \to J \in Top$
7	5 6	syl	$⊢ (((((((U \in UnifOn (X) \land J \in Haus) \land a \in J) \land x \in a) \land v \in U) \land a = v [\{x\}]) \land w \in U) \land (w^{-1} = w \land w \circ (w \circ w) \subseteq v)) \to J \in Top$
8		simplr	$⊢ (((((((U \in UnifOn (X) \land J \in Haus) \land a \in J) \land x \in a) \land v \in U) \land a = v [\{x\}]) \land w \in U) \land (w^{-1} = w \land w \circ (w \circ w) \subseteq v)) \to w \in U$
9		simp-4l	$⊢ ((((U \in UnifOn (X) \land J \in Haus) \land a \in J) \land x \in a) \land w \in U) \to U \in UnifOn (X)$
10		simpr	$⊢ ((((U \in UnifOn (X) \land J \in Haus) \land a \in J) \land x \in a) \land w \in U) \to w \in U$
11	4	ad3antrrr	$⊢ ((((U \in UnifOn (X) \land J \in Haus) \land a \in J) \land x \in a) \land w \in U) \to J \in Top$
12		simpllr	$⊢ ((((U \in UnifOn (X) \land J \in Haus) \land a \in J) \land x \in a) \land w \in U) \to a \in J$
13		eqid	$⊢ ⋃ J = ⋃ J$
14	13	eltopss	$⊢ (J \in Top \land a \in J) \to a \subseteq ⋃ J$
15	11 12 14	syl2anc	$⊢ ((((U \in UnifOn (X) \land J \in Haus) \land a \in J) \land x \in a) \land w \in U) \to a \subseteq ⋃ J$
16		utopbas	$⊢ U \in UnifOn (X) \to X = ⋃ unifTop (U)$
17	1	unieqi	$⊢ ⋃ J = ⋃ unifTop (U)$
18	16 17	eqtr4di	$⊢ U \in UnifOn (X) \to X = ⋃ J$
19	9 18	syl	$⊢ ((((U \in UnifOn (X) \land J \in Haus) \land a \in J) \land x \in a) \land w \in U) \to X = ⋃ J$
20	15 19	sseqtrrd	$⊢ ((((U \in UnifOn (X) \land J \in Haus) \land a \in J) \land x \in a) \land w \in U) \to a \subseteq X$
21		simplr	$⊢ ((((U \in UnifOn (X) \land J \in Haus) \land a \in J) \land x \in a) \land w \in U) \to x \in a$
22	20 21	sseldd	$⊢ ((((U \in UnifOn (X) \land J \in Haus) \land a \in J) \land x \in a) \land w \in U) \to x \in X$
23	1	utopsnnei	$⊢ (U \in UnifOn (X) \land w \in U \land x \in X) \to w [\{x\}] \in nei (J) (\{x\})$
24	9 10 22 23	syl3anc	$⊢ ((((U \in UnifOn (X) \land J \in Haus) \land a \in J) \land x \in a) \land w \in U) \to w [\{x\}] \in nei (J) (\{x\})$
25	5 8 24	syl2anc	$⊢ (((((((U \in UnifOn (X) \land J \in Haus) \land a \in J) \land x \in a) \land v \in U) \land a = v [\{x\}]) \land w \in U) \land (w^{-1} = w \land w \circ (w \circ w) \subseteq v)) \to w [\{x\}] \in nei (J) (\{x\})$
26		neii2	$⊢ (J \in Top \land w [\{x\}] \in nei (J) (\{x\})) \to \exists b \in J (\{x\} \subseteq b \land b \subseteq w [\{x\}])$
27	7 25 26	syl2anc	$⊢ (((((((U \in UnifOn (X) \land J \in Haus) \land a \in J) \land x \in a) \land v \in U) \land a = v [\{x\}]) \land w \in U) \land (w^{-1} = w \land w \circ (w \circ w) \subseteq v)) \to \exists b \in J (\{x\} \subseteq b \land b \subseteq w [\{x\}])$
28		simprl	$⊢ (((((((((U \in UnifOn (X) \land J \in Haus) \land a \in J) \land x \in a) \land v \in U) \land a = v [\{x\}]) \land w \in U) \land (w^{-1} = w \land w \circ (w \circ w) \subseteq v)) \land b \in J) \land (\{x\} \subseteq b \land b \subseteq w [\{x\}])) \to \{x\} \subseteq b$
29		vex	$⊢ x \in V$
30	29	snss	$⊢ x \in b \leftrightarrow \{x\} \subseteq b$
31	28 30	sylibr	$⊢ (((((((((U \in UnifOn (X) \land J \in Haus) \land a \in J) \land x \in a) \land v \in U) \land a = v [\{x\}]) \land w \in U) \land (w^{-1} = w \land w \circ (w \circ w) \subseteq v)) \land b \in J) \land (\{x\} \subseteq b \land b \subseteq w [\{x\}])) \to x \in b$
32	7	ad2antrr	$⊢ (((((((((U \in UnifOn (X) \land J \in Haus) \land a \in J) \land x \in a) \land v \in U) \land a = v [\{x\}]) \land w \in U) \land (w^{-1} = w \land w \circ (w \circ w) \subseteq v)) \land b \in J) \land (\{x\} \subseteq b \land b \subseteq w [\{x\}])) \to J \in Top$
33		simplll	$⊢ (((U \in UnifOn (X) \land J \in Haus) \land a \in J) \land x \in a) \to U \in UnifOn (X)$
34	5 33	syl	$⊢ (((((((U \in UnifOn (X) \land J \in Haus) \land a \in J) \land x \in a) \land v \in U) \land a = v [\{x\}]) \land w \in U) \land (w^{-1} = w \land w \circ (w \circ w) \subseteq v)) \to U \in UnifOn (X)$
35	34	ad2antrr	$⊢ (((((((((U \in UnifOn (X) \land J \in Haus) \land a \in J) \land x \in a) \land v \in U) \land a = v [\{x\}]) \land w \in U) \land (w^{-1} = w \land w \circ (w \circ w) \subseteq v)) \land b \in J) \land (\{x\} \subseteq b \land b \subseteq w [\{x\}])) \to U \in UnifOn (X)$
36	8	ad2antrr	$⊢ (((((((((U \in UnifOn (X) \land J \in Haus) \land a \in J) \land x \in a) \land v \in U) \land a = v [\{x\}]) \land w \in U) \land (w^{-1} = w \land w \circ (w \circ w) \subseteq v)) \land b \in J) \land (\{x\} \subseteq b \land b \subseteq w [\{x\}])) \to w \in U$
37		simplr	$⊢ (((U \in UnifOn (X) \land J \in Haus) \land a \in J) \land x \in a) \to a \in J$
38	6 37 14	syl2anc	$⊢ (((U \in UnifOn (X) \land J \in Haus) \land a \in J) \land x \in a) \to a \subseteq ⋃ J$
39	33 18	syl	$⊢ (((U \in UnifOn (X) \land J \in Haus) \land a \in J) \land x \in a) \to X = ⋃ J$
40	38 39	sseqtrrd	$⊢ (((U \in UnifOn (X) \land J \in Haus) \land a \in J) \land x \in a) \to a \subseteq X$
41		simpr	$⊢ (((U \in UnifOn (X) \land J \in Haus) \land a \in J) \land x \in a) \to x \in a$
42	40 41	sseldd	$⊢ (((U \in UnifOn (X) \land J \in Haus) \land a \in J) \land x \in a) \to x \in X$
43	42	ad6antr	$⊢ (((((((((U \in UnifOn (X) \land J \in Haus) \land a \in J) \land x \in a) \land v \in U) \land a = v [\{x\}]) \land w \in U) \land (w^{-1} = w \land w \circ (w \circ w) \subseteq v)) \land b \in J) \land (\{x\} \subseteq b \land b \subseteq w [\{x\}])) \to x \in X$
44		ustimasn	$⊢ (U \in UnifOn (X) \land w \in U \land x \in X) \to w [\{x\}] \subseteq X$
45	35 36 43 44	syl3anc	$⊢ (((((((((U \in UnifOn (X) \land J \in Haus) \land a \in J) \land x \in a) \land v \in U) \land a = v [\{x\}]) \land w \in U) \land (w^{-1} = w \land w \circ (w \circ w) \subseteq v)) \land b \in J) \land (\{x\} \subseteq b \land b \subseteq w [\{x\}])) \to w [\{x\}] \subseteq X$
46	35 18	syl	$⊢ (((((((((U \in UnifOn (X) \land J \in Haus) \land a \in J) \land x \in a) \land v \in U) \land a = v [\{x\}]) \land w \in U) \land (w^{-1} = w \land w \circ (w \circ w) \subseteq v)) \land b \in J) \land (\{x\} \subseteq b \land b \subseteq w [\{x\}])) \to X = ⋃ J$
47	45 46	sseqtrd	$⊢ (((((((((U \in UnifOn (X) \land J \in Haus) \land a \in J) \land x \in a) \land v \in U) \land a = v [\{x\}]) \land w \in U) \land (w^{-1} = w \land w \circ (w \circ w) \subseteq v)) \land b \in J) \land (\{x\} \subseteq b \land b \subseteq w [\{x\}])) \to w [\{x\}] \subseteq ⋃ J$
48		simprr	$⊢ (((((((((U \in UnifOn (X) \land J \in Haus) \land a \in J) \land x \in a) \land v \in U) \land a = v [\{x\}]) \land w \in U) \land (w^{-1} = w \land w \circ (w \circ w) \subseteq v)) \land b \in J) \land (\{x\} \subseteq b \land b \subseteq w [\{x\}])) \to b \subseteq w [\{x\}]$
49	13	clsss	$⊢ (J \in Top \land w [\{x\}] \subseteq ⋃ J \land b \subseteq w [\{x\}]) \to cls (J) (b) \subseteq cls (J) (w [\{x\}])$
50	32 47 48 49	syl3anc	$⊢ (((((((((U \in UnifOn (X) \land J \in Haus) \land a \in J) \land x \in a) \land v \in U) \land a = v [\{x\}]) \land w \in U) \land (w^{-1} = w \land w \circ (w \circ w) \subseteq v)) \land b \in J) \land (\{x\} \subseteq b \land b \subseteq w [\{x\}])) \to cls (J) (b) \subseteq cls (J) (w [\{x\}])$
51		ustssxp	$⊢ (U \in UnifOn (X) \land w \in U) \to w \subseteq X \times X$
52	34 8 51	syl2anc	$⊢ (((((((U \in UnifOn (X) \land J \in Haus) \land a \in J) \land x \in a) \land v \in U) \land a = v [\{x\}]) \land w \in U) \land (w^{-1} = w \land w \circ (w \circ w) \subseteq v)) \to w \subseteq X \times X$
53	34 18	syl	$⊢ (((((((U \in UnifOn (X) \land J \in Haus) \land a \in J) \land x \in a) \land v \in U) \land a = v [\{x\}]) \land w \in U) \land (w^{-1} = w \land w \circ (w \circ w) \subseteq v)) \to X = ⋃ J$
54	53	sqxpeqd	$⊢ (((((((U \in UnifOn (X) \land J \in Haus) \land a \in J) \land x \in a) \land v \in U) \land a = v [\{x\}]) \land w \in U) \land (w^{-1} = w \land w \circ (w \circ w) \subseteq v)) \to X \times X = ⋃ J \times ⋃ J$
55	52 54	sseqtrd	$⊢ (((((((U \in UnifOn (X) \land J \in Haus) \land a \in J) \land x \in a) \land v \in U) \land a = v [\{x\}]) \land w \in U) \land (w^{-1} = w \land w \circ (w \circ w) \subseteq v)) \to w \subseteq ⋃ J \times ⋃ J$
56	5 38	syl	$⊢ (((((((U \in UnifOn (X) \land J \in Haus) \land a \in J) \land x \in a) \land v \in U) \land a = v [\{x\}]) \land w \in U) \land (w^{-1} = w \land w \circ (w \circ w) \subseteq v)) \to a \subseteq ⋃ J$
57		simp-5r	$⊢ (((((((U \in UnifOn (X) \land J \in Haus) \land a \in J) \land x \in a) \land v \in U) \land a = v [\{x\}]) \land w \in U) \land (w^{-1} = w \land w \circ (w \circ w) \subseteq v)) \to x \in a$
58	56 57	sseldd	$⊢ (((((((U \in UnifOn (X) \land J \in Haus) \land a \in J) \land x \in a) \land v \in U) \land a = v [\{x\}]) \land w \in U) \land (w^{-1} = w \land w \circ (w \circ w) \subseteq v)) \to x \in ⋃ J$
59	13 13	imasncls	$⊢ ((J \in Top \land J \in Top) \land (w \subseteq ⋃ J \times ⋃ J \land x \in ⋃ J)) \to cls (J) (w [\{x\}]) \subseteq cls (J \times_{t} J) (w) [\{x\}]$
60	7 7 55 58 59	syl22anc	$⊢ (((((((U \in UnifOn (X) \land J \in Haus) \land a \in J) \land x \in a) \land v \in U) \land a = v [\{x\}]) \land w \in U) \land (w^{-1} = w \land w \circ (w \circ w) \subseteq v)) \to cls (J) (w [\{x\}]) \subseteq cls (J \times_{t} J) (w) [\{x\}]$
61		simprl	$⊢ (((((((U \in UnifOn (X) \land J \in Haus) \land a \in J) \land x \in a) \land v \in U) \land a = v [\{x\}]) \land w \in U) \land (w^{-1} = w \land w \circ (w \circ w) \subseteq v)) \to w^{-1} = w$
62	1	utop3cls	$⊢ ((U \in UnifOn (X) \land w \subseteq X \times X) \land (w \in U \land w^{-1} = w)) \to cls (J \times_{t} J) (w) \subseteq w \circ (w \circ w)$
63	34 52 8 61 62	syl22anc	$⊢ (((((((U \in UnifOn (X) \land J \in Haus) \land a \in J) \land x \in a) \land v \in U) \land a = v [\{x\}]) \land w \in U) \land (w^{-1} = w \land w \circ (w \circ w) \subseteq v)) \to cls (J \times_{t} J) (w) \subseteq w \circ (w \circ w)$
64		simprr	$⊢ (((((((U \in UnifOn (X) \land J \in Haus) \land a \in J) \land x \in a) \land v \in U) \land a = v [\{x\}]) \land w \in U) \land (w^{-1} = w \land w \circ (w \circ w) \subseteq v)) \to w \circ (w \circ w) \subseteq v$
65	63 64	sstrd	$⊢ (((((((U \in UnifOn (X) \land J \in Haus) \land a \in J) \land x \in a) \land v \in U) \land a = v [\{x\}]) \land w \in U) \land (w^{-1} = w \land w \circ (w \circ w) \subseteq v)) \to cls (J \times_{t} J) (w) \subseteq v$
66		imass1	$⊢ cls (J \times_{t} J) (w) \subseteq v \to cls (J \times_{t} J) (w) [\{x\}] \subseteq v [\{x\}]$
67	65 66	syl	$⊢ (((((((U \in UnifOn (X) \land J \in Haus) \land a \in J) \land x \in a) \land v \in U) \land a = v [\{x\}]) \land w \in U) \land (w^{-1} = w \land w \circ (w \circ w) \subseteq v)) \to cls (J \times_{t} J) (w) [\{x\}] \subseteq v [\{x\}]$
68	60 67	sstrd	$⊢ (((((((U \in UnifOn (X) \land J \in Haus) \land a \in J) \land x \in a) \land v \in U) \land a = v [\{x\}]) \land w \in U) \land (w^{-1} = w \land w \circ (w \circ w) \subseteq v)) \to cls (J) (w [\{x\}]) \subseteq v [\{x\}]$
69	68	ad2antrr	$⊢ (((((((((U \in UnifOn (X) \land J \in Haus) \land a \in J) \land x \in a) \land v \in U) \land a = v [\{x\}]) \land w \in U) \land (w^{-1} = w \land w \circ (w \circ w) \subseteq v)) \land b \in J) \land (\{x\} \subseteq b \land b \subseteq w [\{x\}])) \to cls (J) (w [\{x\}]) \subseteq v [\{x\}]$
70	50 69	sstrd	$⊢ (((((((((U \in UnifOn (X) \land J \in Haus) \land a \in J) \land x \in a) \land v \in U) \land a = v [\{x\}]) \land w \in U) \land (w^{-1} = w \land w \circ (w \circ w) \subseteq v)) \land b \in J) \land (\{x\} \subseteq b \land b \subseteq w [\{x\}])) \to cls (J) (b) \subseteq v [\{x\}]$
71		simp-5r	$⊢ (((((((((U \in UnifOn (X) \land J \in Haus) \land a \in J) \land x \in a) \land v \in U) \land a = v [\{x\}]) \land w \in U) \land (w^{-1} = w \land w \circ (w \circ w) \subseteq v)) \land b \in J) \land (\{x\} \subseteq b \land b \subseteq w [\{x\}])) \to a = v [\{x\}]$
72	70 71	sseqtrrd	$⊢ (((((((((U \in UnifOn (X) \land J \in Haus) \land a \in J) \land x \in a) \land v \in U) \land a = v [\{x\}]) \land w \in U) \land (w^{-1} = w \land w \circ (w \circ w) \subseteq v)) \land b \in J) \land (\{x\} \subseteq b \land b \subseteq w [\{x\}])) \to cls (J) (b) \subseteq a$
73	31 72	jca	$⊢ (((((((((U \in UnifOn (X) \land J \in Haus) \land a \in J) \land x \in a) \land v \in U) \land a = v [\{x\}]) \land w \in U) \land (w^{-1} = w \land w \circ (w \circ w) \subseteq v)) \land b \in J) \land (\{x\} \subseteq b \land b \subseteq w [\{x\}])) \to (x \in b \land cls (J) (b) \subseteq a)$
74	73	ex	$⊢ ((((((((U \in UnifOn (X) \land J \in Haus) \land a \in J) \land x \in a) \land v \in U) \land a = v [\{x\}]) \land w \in U) \land (w^{-1} = w \land w \circ (w \circ w) \subseteq v)) \land b \in J) \to ((\{x\} \subseteq b \land b \subseteq w [\{x\}]) \to (x \in b \land cls (J) (b) \subseteq a))$
75	74	reximdva	$⊢ (((((((U \in UnifOn (X) \land J \in Haus) \land a \in J) \land x \in a) \land v \in U) \land a = v [\{x\}]) \land w \in U) \land (w^{-1} = w \land w \circ (w \circ w) \subseteq v)) \to (\exists b \in J (\{x\} \subseteq b \land b \subseteq w [\{x\}]) \to \exists b \in J (x \in b \land cls (J) (b) \subseteq a))$
76	27 75	mpd	$⊢ (((((((U \in UnifOn (X) \land J \in Haus) \land a \in J) \land x \in a) \land v \in U) \land a = v [\{x\}]) \land w \in U) \land (w^{-1} = w \land w \circ (w \circ w) \subseteq v)) \to \exists b \in J (x \in b \land cls (J) (b) \subseteq a)$
77		simp-5l	$⊢ (((((U \in UnifOn (X) \land J \in Haus) \land a \in J) \land x \in a) \land v \in U) \land a = v [\{x\}]) \to U \in UnifOn (X)$
78		simplr	$⊢ (((((U \in UnifOn (X) \land J \in Haus) \land a \in J) \land x \in a) \land v \in U) \land a = v [\{x\}]) \to v \in U$
79		ustex3sym	$⊢ (U \in UnifOn (X) \land v \in U) \to \exists w \in U (w^{-1} = w \land w \circ (w \circ w) \subseteq v)$
80	77 78 79	syl2anc	$⊢ (((((U \in UnifOn (X) \land J \in Haus) \land a \in J) \land x \in a) \land v \in U) \land a = v [\{x\}]) \to \exists w \in U (w^{-1} = w \land w \circ (w \circ w) \subseteq v)$
81	76 80	r19.29a	$⊢ (((((U \in UnifOn (X) \land J \in Haus) \land a \in J) \land x \in a) \land v \in U) \land a = v [\{x\}]) \to \exists b \in J (x \in b \land cls (J) (b) \subseteq a)$
82		opnneip	$⊢ (J \in Top \land a \in J \land x \in a) \to a \in nei (J) (\{x\})$
83	6 37 41 82	syl3anc	$⊢ (((U \in UnifOn (X) \land J \in Haus) \land a \in J) \land x \in a) \to a \in nei (J) (\{x\})$
84	1	utopsnneip	$⊢ (U \in UnifOn (X) \land x \in X) \to nei (J) (\{x\}) = ran (v \in U ⟼ v [\{x\}])$
85	33 42 84	syl2anc	$⊢ (((U \in UnifOn (X) \land J \in Haus) \land a \in J) \land x \in a) \to nei (J) (\{x\}) = ran (v \in U ⟼ v [\{x\}])$
86	83 85	eleqtrd	$⊢ (((U \in UnifOn (X) \land J \in Haus) \land a \in J) \land x \in a) \to a \in ran (v \in U ⟼ v [\{x\}])$
87		eqid	$⊢ (v \in U ⟼ v [\{x\}]) = (v \in U ⟼ v [\{x\}])$
88	87	elrnmpt	$⊢ a \in J \to (a \in ran (v \in U ⟼ v [\{x\}]) \leftrightarrow \exists v \in U a = v [\{x\}])$
89	37 88	syl	$⊢ (((U \in UnifOn (X) \land J \in Haus) \land a \in J) \land x \in a) \to (a \in ran (v \in U ⟼ v [\{x\}]) \leftrightarrow \exists v \in U a = v [\{x\}])$
90	86 89	mpbid	$⊢ (((U \in UnifOn (X) \land J \in Haus) \land a \in J) \land x \in a) \to \exists v \in U a = v [\{x\}]$
91	81 90	r19.29a	$⊢ (((U \in UnifOn (X) \land J \in Haus) \land a \in J) \land x \in a) \to \exists b \in J (x \in b \land cls (J) (b) \subseteq a)$
92	91	ralrimiva	$⊢ ((U \in UnifOn (X) \land J \in Haus) \land a \in J) \to \forall x \in a \exists b \in J (x \in b \land cls (J) (b) \subseteq a)$
93	92	ralrimiva	$⊢ (U \in UnifOn (X) \land J \in Haus) \to \forall a \in J \forall x \in a \exists b \in J (x \in b \land cls (J) (b) \subseteq a)$
94		isreg	$⊢ J \in Reg \leftrightarrow (J \in Top \land \forall a \in J \forall x \in a \exists b \in J (x \in b \land cls (J) (b) \subseteq a))$
95	4 93 94	sylanbrc	$⊢ (U \in UnifOn (X) \land J \in Haus) \to J \in Reg$

Metamath Proof Explorer

Theorem utopreg

Proof