psmetutop

Description: The topology induced by a uniform structure generated by a metric D is generated by that metric's open balls. (Contributed by Thierry Arnoux, 6-Dec-2017) (Revised by Thierry Arnoux, 11-Mar-2018)

		Ref	Expression
	Assertion	psmetutop	$⊢ (X \neq \emptyset \land D \in PsMet (X)) \to unifTop (metUnif (D)) = topGen (ran ball (D))$

Proof

Step	Hyp	Ref	Expression
1		metuust	$⊢ (X \neq \emptyset \land D \in PsMet (X)) \to metUnif (D) \in UnifOn (X)$
2		utopval	$⊢ metUnif (D) \in UnifOn (X) \to unifTop (metUnif (D)) = \{a \in 𝒫 X \| \forall x \in a \exists v \in metUnif (D) v [\{x\}] \subseteq a\}$
3	1 2	syl	$⊢ (X \neq \emptyset \land D \in PsMet (X)) \to unifTop (metUnif (D)) = \{a \in 𝒫 X \| \forall x \in a \exists v \in metUnif (D) v [\{x\}] \subseteq a\}$
4	3	eleq2d	$⊢ (X \neq \emptyset \land D \in PsMet (X)) \to (a \in unifTop (metUnif (D)) \leftrightarrow a \in \{a \in 𝒫 X \| \forall x \in a \exists v \in metUnif (D) v [\{x\}] \subseteq a\})$
5		rabid	$⊢ a \in \{a \in 𝒫 X \| \forall x \in a \exists v \in metUnif (D) v [\{x\}] \subseteq a\} \leftrightarrow (a \in 𝒫 X \land \forall x \in a \exists v \in metUnif (D) v [\{x\}] \subseteq a)$
6	4 5	bitrdi	$⊢ (X \neq \emptyset \land D \in PsMet (X)) \to (a \in unifTop (metUnif (D)) \leftrightarrow (a \in 𝒫 X \land \forall x \in a \exists v \in metUnif (D) v [\{x\}] \subseteq a))$
7	6	biimpa	$⊢ ((X \neq \emptyset \land D \in PsMet (X)) \land a \in unifTop (metUnif (D))) \to (a \in 𝒫 X \land \forall x \in a \exists v \in metUnif (D) v [\{x\}] \subseteq a)$
8	7	simpld	$⊢ ((X \neq \emptyset \land D \in PsMet (X)) \land a \in unifTop (metUnif (D))) \to a \in 𝒫 X$
9	8	elpwid	$⊢ ((X \neq \emptyset \land D \in PsMet (X)) \land a \in unifTop (metUnif (D))) \to a \subseteq X$
10		unirnblps	$⊢ D \in PsMet (X) \to ⋃ ran ball (D) = X$
11	10	ad2antlr	$⊢ ((X \neq \emptyset \land D \in PsMet (X)) \land a \in unifTop (metUnif (D))) \to ⋃ ran ball (D) = X$
12	9 11	sseqtrrd	$⊢ ((X \neq \emptyset \land D \in PsMet (X)) \land a \in unifTop (metUnif (D))) \to a \subseteq ⋃ ran ball (D)$
13		simpr	$⊢ (((((X \neq \emptyset \land D \in PsMet (X)) \land a \in unifTop (metUnif (D))) \land x \in a) \land v \in metUnif (D)) \land v [\{x\}] \subseteq a) \to v [\{x\}] \subseteq a$
14		simp-5r	$⊢ (((((X \neq \emptyset \land D \in PsMet (X)) \land a \in unifTop (metUnif (D))) \land x \in a) \land v \in metUnif (D)) \land v [\{x\}] \subseteq a) \to D \in PsMet (X)$
15		simplr	$⊢ (((((X \neq \emptyset \land D \in PsMet (X)) \land a \in unifTop (metUnif (D))) \land x \in a) \land v \in metUnif (D)) \land v [\{x\}] \subseteq a) \to v \in metUnif (D)$
16	9	ad3antrrr	$⊢ (((((X \neq \emptyset \land D \in PsMet (X)) \land a \in unifTop (metUnif (D))) \land x \in a) \land v \in metUnif (D)) \land v [\{x\}] \subseteq a) \to a \subseteq X$
17		simpllr	$⊢ (((((X \neq \emptyset \land D \in PsMet (X)) \land a \in unifTop (metUnif (D))) \land x \in a) \land v \in metUnif (D)) \land v [\{x\}] \subseteq a) \to x \in a$
18	16 17	sseldd	$⊢ (((((X \neq \emptyset \land D \in PsMet (X)) \land a \in unifTop (metUnif (D))) \land x \in a) \land v \in metUnif (D)) \land v [\{x\}] \subseteq a) \to x \in X$
19		metustbl	$⊢ (D \in PsMet (X) \land v \in metUnif (D) \land x \in X) \to \exists b \in ran ball (D) (x \in b \land b \subseteq v [\{x\}])$
20	14 15 18 19	syl3anc	$⊢ (((((X \neq \emptyset \land D \in PsMet (X)) \land a \in unifTop (metUnif (D))) \land x \in a) \land v \in metUnif (D)) \land v [\{x\}] \subseteq a) \to \exists b \in ran ball (D) (x \in b \land b \subseteq v [\{x\}])$
21		sstr	$⊢ (b \subseteq v [\{x\}] \land v [\{x\}] \subseteq a) \to b \subseteq a$
22	21	expcom	$⊢ v [\{x\}] \subseteq a \to (b \subseteq v [\{x\}] \to b \subseteq a)$
23	22	anim2d	$⊢ v [\{x\}] \subseteq a \to ((x \in b \land b \subseteq v [\{x\}]) \to (x \in b \land b \subseteq a))$
24	23	reximdv	$⊢ v [\{x\}] \subseteq a \to (\exists b \in ran ball (D) (x \in b \land b \subseteq v [\{x\}]) \to \exists b \in ran ball (D) (x \in b \land b \subseteq a))$
25	13 20 24	sylc	$⊢ (((((X \neq \emptyset \land D \in PsMet (X)) \land a \in unifTop (metUnif (D))) \land x \in a) \land v \in metUnif (D)) \land v [\{x\}] \subseteq a) \to \exists b \in ran ball (D) (x \in b \land b \subseteq a)$
26	7	simprd	$⊢ ((X \neq \emptyset \land D \in PsMet (X)) \land a \in unifTop (metUnif (D))) \to \forall x \in a \exists v \in metUnif (D) v [\{x\}] \subseteq a$
27	26	r19.21bi	$⊢ (((X \neq \emptyset \land D \in PsMet (X)) \land a \in unifTop (metUnif (D))) \land x \in a) \to \exists v \in metUnif (D) v [\{x\}] \subseteq a$
28	25 27	r19.29a	$⊢ (((X \neq \emptyset \land D \in PsMet (X)) \land a \in unifTop (metUnif (D))) \land x \in a) \to \exists b \in ran ball (D) (x \in b \land b \subseteq a)$
29	28	ralrimiva	$⊢ ((X \neq \emptyset \land D \in PsMet (X)) \land a \in unifTop (metUnif (D))) \to \forall x \in a \exists b \in ran ball (D) (x \in b \land b \subseteq a)$
30	12 29	jca	$⊢ ((X \neq \emptyset \land D \in PsMet (X)) \land a \in unifTop (metUnif (D))) \to (a \subseteq ⋃ ran ball (D) \land \forall x \in a \exists b \in ran ball (D) (x \in b \land b \subseteq a))$
31		fvex	$⊢ ball (D) \in V$
32	31	rnex	$⊢ ran ball (D) \in V$
33		eltg2	$⊢ ran ball (D) \in V \to (a \in topGen (ran ball (D)) \leftrightarrow (a \subseteq ⋃ ran ball (D) \land \forall x \in a \exists b \in ran ball (D) (x \in b \land b \subseteq a)))$
34	32 33	mp1i	$⊢ ((X \neq \emptyset \land D \in PsMet (X)) \land a \in unifTop (metUnif (D))) \to (a \in topGen (ran ball (D)) \leftrightarrow (a \subseteq ⋃ ran ball (D) \land \forall x \in a \exists b \in ran ball (D) (x \in b \land b \subseteq a)))$
35	30 34	mpbird	$⊢ ((X \neq \emptyset \land D \in PsMet (X)) \land a \in unifTop (metUnif (D))) \to a \in topGen (ran ball (D))$
36	32 33	mp1i	$⊢ (X \neq \emptyset \land D \in PsMet (X)) \to (a \in topGen (ran ball (D)) \leftrightarrow (a \subseteq ⋃ ran ball (D) \land \forall x \in a \exists b \in ran ball (D) (x \in b \land b \subseteq a)))$
37	36	biimpa	$⊢ ((X \neq \emptyset \land D \in PsMet (X)) \land a \in topGen (ran ball (D))) \to (a \subseteq ⋃ ran ball (D) \land \forall x \in a \exists b \in ran ball (D) (x \in b \land b \subseteq a))$
38	37	simpld	$⊢ ((X \neq \emptyset \land D \in PsMet (X)) \land a \in topGen (ran ball (D))) \to a \subseteq ⋃ ran ball (D)$
39	10	ad2antlr	$⊢ ((X \neq \emptyset \land D \in PsMet (X)) \land a \in topGen (ran ball (D))) \to ⋃ ran ball (D) = X$
40	38 39	sseqtrd	$⊢ ((X \neq \emptyset \land D \in PsMet (X)) \land a \in topGen (ran ball (D))) \to a \subseteq X$
41		elpwg	$⊢ a \in topGen (ran ball (D)) \to (a \in 𝒫 X \leftrightarrow a \subseteq X)$
42	41	adantl	$⊢ ((X \neq \emptyset \land D \in PsMet (X)) \land a \in topGen (ran ball (D))) \to (a \in 𝒫 X \leftrightarrow a \subseteq X)$
43	40 42	mpbird	$⊢ ((X \neq \emptyset \land D \in PsMet (X)) \land a \in topGen (ran ball (D))) \to a \in 𝒫 X$
44		simpllr	$⊢ (((X \neq \emptyset \land D \in PsMet (X)) \land a \in topGen (ran ball (D))) \land x \in a) \to D \in PsMet (X)$
45	40	sselda	$⊢ (((X \neq \emptyset \land D \in PsMet (X)) \land a \in topGen (ran ball (D))) \land x \in a) \to x \in X$
46	37	simprd	$⊢ ((X \neq \emptyset \land D \in PsMet (X)) \land a \in topGen (ran ball (D))) \to \forall x \in a \exists b \in ran ball (D) (x \in b \land b \subseteq a)$
47	46	r19.21bi	$⊢ (((X \neq \emptyset \land D \in PsMet (X)) \land a \in topGen (ran ball (D))) \land x \in a) \to \exists b \in ran ball (D) (x \in b \land b \subseteq a)$
48		blssexps	$⊢ (D \in PsMet (X) \land x \in X) \to (\exists b \in ran ball (D) (x \in b \land b \subseteq a) \leftrightarrow \exists d \in ℝ^{+} x ball (D) d \subseteq a)$
49	44 45 48	syl2anc	$⊢ (((X \neq \emptyset \land D \in PsMet (X)) \land a \in topGen (ran ball (D))) \land x \in a) \to (\exists b \in ran ball (D) (x \in b \land b \subseteq a) \leftrightarrow \exists d \in ℝ^{+} x ball (D) d \subseteq a)$
50	47 49	mpbid	$⊢ (((X \neq \emptyset \land D \in PsMet (X)) \land a \in topGen (ran ball (D))) \land x \in a) \to \exists d \in ℝ^{+} x ball (D) d \subseteq a$
51		blval2	$⊢ (D \in PsMet (X) \land x \in X \land d \in ℝ^{+}) \to x ball (D) d = D^{-1} [[0, d)] [\{x\}]$
52	51	3expa	$⊢ ((D \in PsMet (X) \land x \in X) \land d \in ℝ^{+}) \to x ball (D) d = D^{-1} [[0, d)] [\{x\}]$
53	52	sseq1d	$⊢ ((D \in PsMet (X) \land x \in X) \land d \in ℝ^{+}) \to (x ball (D) d \subseteq a \leftrightarrow D^{-1} [[0, d)] [\{x\}] \subseteq a)$
54	53	rexbidva	$⊢ (D \in PsMet (X) \land x \in X) \to (\exists d \in ℝ^{+} x ball (D) d \subseteq a \leftrightarrow \exists d \in ℝ^{+} D^{-1} [[0, d)] [\{x\}] \subseteq a)$
55	54	biimpa	$⊢ ((D \in PsMet (X) \land x \in X) \land \exists d \in ℝ^{+} x ball (D) d \subseteq a) \to \exists d \in ℝ^{+} D^{-1} [[0, d)] [\{x\}] \subseteq a$
56	44 45 50 55	syl21anc	$⊢ (((X \neq \emptyset \land D \in PsMet (X)) \land a \in topGen (ran ball (D))) \land x \in a) \to \exists d \in ℝ^{+} D^{-1} [[0, d)] [\{x\}] \subseteq a$
57		cnvexg	$⊢ D \in PsMet (X) \to D^{-1} \in V$
58		imaexg	$⊢ D^{-1} \in V \to D^{-1} [[0, d)] \in V$
59	57 58	syl	$⊢ D \in PsMet (X) \to D^{-1} [[0, d)] \in V$
60	59	ralrimivw	$⊢ D \in PsMet (X) \to \forall d \in ℝ^{+} D^{-1} [[0, d)] \in V$
61		eqid	$⊢ (d \in ℝ^{+} ⟼ D^{-1} [[0, d)]) = (d \in ℝ^{+} ⟼ D^{-1} [[0, d)])$
62		imaeq1	$⊢ v = D^{-1} [[0, d)] \to v [\{x\}] = D^{-1} [[0, d)] [\{x\}]$
63	62	sseq1d	$⊢ v = D^{-1} [[0, d)] \to (v [\{x\}] \subseteq a \leftrightarrow D^{-1} [[0, d)] [\{x\}] \subseteq a)$
64	61 63	rexrnmptw	$⊢ \forall d \in ℝ^{+} D^{-1} [[0, d)] \in V \to (\exists v \in ran (d \in ℝ^{+} ⟼ D^{-1} [[0, d)]) v [\{x\}] \subseteq a \leftrightarrow \exists d \in ℝ^{+} D^{-1} [[0, d)] [\{x\}] \subseteq a)$
65	44 60 64	3syl	$⊢ (((X \neq \emptyset \land D \in PsMet (X)) \land a \in topGen (ran ball (D))) \land x \in a) \to (\exists v \in ran (d \in ℝ^{+} ⟼ D^{-1} [[0, d)]) v [\{x\}] \subseteq a \leftrightarrow \exists d \in ℝ^{+} D^{-1} [[0, d)] [\{x\}] \subseteq a)$
66	56 65	mpbird	$⊢ (((X \neq \emptyset \land D \in PsMet (X)) \land a \in topGen (ran ball (D))) \land x \in a) \to \exists v \in ran (d \in ℝ^{+} ⟼ D^{-1} [[0, d)]) v [\{x\}] \subseteq a$
67		oveq2	$⊢ d = e \to [0, d) = [0, e)$
68	67	imaeq2d	$⊢ d = e \to D^{-1} [[0, d)] = D^{-1} [[0, e)]$
69	68	cbvmptv	$⊢ (d \in ℝ^{+} ⟼ D^{-1} [[0, d)]) = (e \in ℝ^{+} ⟼ D^{-1} [[0, e)])$
70	69	rneqi	$⊢ ran (d \in ℝ^{+} ⟼ D^{-1} [[0, d)]) = ran (e \in ℝ^{+} ⟼ D^{-1} [[0, e)])$
71	70	metustfbas	$⊢ (X \neq \emptyset \land D \in PsMet (X)) \to ran (d \in ℝ^{+} ⟼ D^{-1} [[0, d)]) \in fBas (X \times X)$
72		ssfg	$⊢ ran (d \in ℝ^{+} ⟼ D^{-1} [[0, d)]) \in fBas (X \times X) \to ran (d \in ℝ^{+} ⟼ D^{-1} [[0, d)]) \subseteq (X \times X) filGen ran (d \in ℝ^{+} ⟼ D^{-1} [[0, d)])$
73	71 72	syl	$⊢ (X \neq \emptyset \land D \in PsMet (X)) \to ran (d \in ℝ^{+} ⟼ D^{-1} [[0, d)]) \subseteq (X \times X) filGen ran (d \in ℝ^{+} ⟼ D^{-1} [[0, d)])$
74		metuval	$⊢ D \in PsMet (X) \to metUnif (D) = (X \times X) filGen ran (d \in ℝ^{+} ⟼ D^{-1} [[0, d)])$
75	74	adantl	$⊢ (X \neq \emptyset \land D \in PsMet (X)) \to metUnif (D) = (X \times X) filGen ran (d \in ℝ^{+} ⟼ D^{-1} [[0, d)])$
76	73 75	sseqtrrd	$⊢ (X \neq \emptyset \land D \in PsMet (X)) \to ran (d \in ℝ^{+} ⟼ D^{-1} [[0, d)]) \subseteq metUnif (D)$
77		ssrexv	$⊢ ran (d \in ℝ^{+} ⟼ D^{-1} [[0, d)]) \subseteq metUnif (D) \to (\exists v \in ran (d \in ℝ^{+} ⟼ D^{-1} [[0, d)]) v [\{x\}] \subseteq a \to \exists v \in metUnif (D) v [\{x\}] \subseteq a)$
78	76 77	syl	$⊢ (X \neq \emptyset \land D \in PsMet (X)) \to (\exists v \in ran (d \in ℝ^{+} ⟼ D^{-1} [[0, d)]) v [\{x\}] \subseteq a \to \exists v \in metUnif (D) v [\{x\}] \subseteq a)$
79	78	ad2antrr	$⊢ (((X \neq \emptyset \land D \in PsMet (X)) \land a \in topGen (ran ball (D))) \land x \in a) \to (\exists v \in ran (d \in ℝ^{+} ⟼ D^{-1} [[0, d)]) v [\{x\}] \subseteq a \to \exists v \in metUnif (D) v [\{x\}] \subseteq a)$
80	66 79	mpd	$⊢ (((X \neq \emptyset \land D \in PsMet (X)) \land a \in topGen (ran ball (D))) \land x \in a) \to \exists v \in metUnif (D) v [\{x\}] \subseteq a$
81	80	ralrimiva	$⊢ ((X \neq \emptyset \land D \in PsMet (X)) \land a \in topGen (ran ball (D))) \to \forall x \in a \exists v \in metUnif (D) v [\{x\}] \subseteq a$
82	43 81	jca	$⊢ ((X \neq \emptyset \land D \in PsMet (X)) \land a \in topGen (ran ball (D))) \to (a \in 𝒫 X \land \forall x \in a \exists v \in metUnif (D) v [\{x\}] \subseteq a)$
83	6	biimpar	$⊢ ((X \neq \emptyset \land D \in PsMet (X)) \land (a \in 𝒫 X \land \forall x \in a \exists v \in metUnif (D) v [\{x\}] \subseteq a)) \to a \in unifTop (metUnif (D))$
84	82 83	syldan	$⊢ ((X \neq \emptyset \land D \in PsMet (X)) \land a \in topGen (ran ball (D))) \to a \in unifTop (metUnif (D))$
85	35 84	impbida	$⊢ (X \neq \emptyset \land D \in PsMet (X)) \to (a \in unifTop (metUnif (D)) \leftrightarrow a \in topGen (ran ball (D)))$
86	85	eqrdv	$⊢ (X \neq \emptyset \land D \in PsMet (X)) \to unifTop (metUnif (D)) = topGen (ran ball (D))$

Metamath Proof Explorer

Theorem psmetutop

Proof