metust

Description: The uniform structure generated by a metric D . (Contributed by Thierry Arnoux, 26-Nov-2017) (Revised by Thierry Arnoux, 11-Feb-2018)

		Ref	Expression
	Hypothesis	metust.1	$⊢ F = ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)])$
	Assertion	metust	$⊢ (X \neq \emptyset \land D \in PsMet (X)) \to (X \times X) filGen F \in UnifOn (X)$

Proof

Step	Hyp	Ref	Expression
1		metust.1	$⊢ F = ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)])$
2	1	metustfbas	$⊢ (X \neq \emptyset \land D \in PsMet (X)) \to F \in fBas (X \times X)$
3		fgcl	$⊢ F \in fBas (X \times X) \to (X \times X) filGen F \in Fil (X \times X)$
4		filsspw	$⊢ (X \times X) filGen F \in Fil (X \times X) \to (X \times X) filGen F \subseteq 𝒫 (X \times X)$
5	2 3 4	3syl	$⊢ (X \neq \emptyset \land D \in PsMet (X)) \to (X \times X) filGen F \subseteq 𝒫 (X \times X)$
6		filtop	$⊢ (X \times X) filGen F \in Fil (X \times X) \to X \times X \in ((X \times X) filGen F)$
7	2 3 6	3syl	$⊢ (X \neq \emptyset \land D \in PsMet (X)) \to X \times X \in ((X \times X) filGen F)$
8	2 3	syl	$⊢ (X \neq \emptyset \land D \in PsMet (X)) \to (X \times X) filGen F \in Fil (X \times X)$
9	8	ad3antrrr	$⊢ ((((X \neq \emptyset \land D \in PsMet (X)) \land v \in ((X \times X) filGen F)) \land w \in 𝒫 (X \times X)) \land v \subseteq w) \to (X \times X) filGen F \in Fil (X \times X)$
10		simpllr	$⊢ ((((X \neq \emptyset \land D \in PsMet (X)) \land v \in ((X \times X) filGen F)) \land w \in 𝒫 (X \times X)) \land v \subseteq w) \to v \in ((X \times X) filGen F)$
11		simplr	$⊢ ((((X \neq \emptyset \land D \in PsMet (X)) \land v \in ((X \times X) filGen F)) \land w \in 𝒫 (X \times X)) \land v \subseteq w) \to w \in 𝒫 (X \times X)$
12	11	elpwid	$⊢ ((((X \neq \emptyset \land D \in PsMet (X)) \land v \in ((X \times X) filGen F)) \land w \in 𝒫 (X \times X)) \land v \subseteq w) \to w \subseteq X \times X$
13		simpr	$⊢ ((((X \neq \emptyset \land D \in PsMet (X)) \land v \in ((X \times X) filGen F)) \land w \in 𝒫 (X \times X)) \land v \subseteq w) \to v \subseteq w$
14		filss	$⊢ ((X \times X) filGen F \in Fil (X \times X) \land (v \in ((X \times X) filGen F) \land w \subseteq X \times X \land v \subseteq w)) \to w \in ((X \times X) filGen F)$
15	9 10 12 13 14	syl13anc	$⊢ ((((X \neq \emptyset \land D \in PsMet (X)) \land v \in ((X \times X) filGen F)) \land w \in 𝒫 (X \times X)) \land v \subseteq w) \to w \in ((X \times X) filGen F)$
16	15	ex	$⊢ (((X \neq \emptyset \land D \in PsMet (X)) \land v \in ((X \times X) filGen F)) \land w \in 𝒫 (X \times X)) \to (v \subseteq w \to w \in ((X \times X) filGen F))$
17	16	ralrimiva	$⊢ ((X \neq \emptyset \land D \in PsMet (X)) \land v \in ((X \times X) filGen F)) \to \forall w \in 𝒫 (X \times X) (v \subseteq w \to w \in ((X \times X) filGen F))$
18	8	ad2antrr	$⊢ (((X \neq \emptyset \land D \in PsMet (X)) \land v \in ((X \times X) filGen F)) \land w \in ((X \times X) filGen F)) \to (X \times X) filGen F \in Fil (X \times X)$
19		simplr	$⊢ (((X \neq \emptyset \land D \in PsMet (X)) \land v \in ((X \times X) filGen F)) \land w \in ((X \times X) filGen F)) \to v \in ((X \times X) filGen F)$
20		simpr	$⊢ (((X \neq \emptyset \land D \in PsMet (X)) \land v \in ((X \times X) filGen F)) \land w \in ((X \times X) filGen F)) \to w \in ((X \times X) filGen F)$
21		filin	$⊢ ((X \times X) filGen F \in Fil (X \times X) \land v \in ((X \times X) filGen F) \land w \in ((X \times X) filGen F)) \to v \cap w \in ((X \times X) filGen F)$
22	18 19 20 21	syl3anc	$⊢ (((X \neq \emptyset \land D \in PsMet (X)) \land v \in ((X \times X) filGen F)) \land w \in ((X \times X) filGen F)) \to v \cap w \in ((X \times X) filGen F)$
23	22	ralrimiva	$⊢ ((X \neq \emptyset \land D \in PsMet (X)) \land v \in ((X \times X) filGen F)) \to \forall w \in ((X \times X) filGen F) v \cap w \in ((X \times X) filGen F)$
24	1	metustid	$⊢ (D \in PsMet (X) \land u \in F) \to {I ↾}_{X} \subseteq u$
25	24	ad5ant24	$⊢ ((((X \neq \emptyset \land D \in PsMet (X)) \land v \in ((X \times X) filGen F)) \land u \in F) \land u \subseteq v) \to {I ↾}_{X} \subseteq u$
26		simpr	$⊢ ((((X \neq \emptyset \land D \in PsMet (X)) \land v \in ((X \times X) filGen F)) \land u \in F) \land u \subseteq v) \to u \subseteq v$
27	25 26	sstrd	$⊢ ((((X \neq \emptyset \land D \in PsMet (X)) \land v \in ((X \times X) filGen F)) \land u \in F) \land u \subseteq v) \to {I ↾}_{X} \subseteq v$
28		elfg	$⊢ F \in fBas (X \times X) \to (v \in ((X \times X) filGen F) \leftrightarrow (v \subseteq X \times X \land \exists u \in F u \subseteq v))$
29	28	biimpa	$⊢ (F \in fBas (X \times X) \land v \in ((X \times X) filGen F)) \to (v \subseteq X \times X \land \exists u \in F u \subseteq v)$
30	29	simprd	$⊢ (F \in fBas (X \times X) \land v \in ((X \times X) filGen F)) \to \exists u \in F u \subseteq v$
31	2 30	sylan	$⊢ ((X \neq \emptyset \land D \in PsMet (X)) \land v \in ((X \times X) filGen F)) \to \exists u \in F u \subseteq v$
32	27 31	r19.29a	$⊢ ((X \neq \emptyset \land D \in PsMet (X)) \land v \in ((X \times X) filGen F)) \to {I ↾}_{X} \subseteq v$
33	8	ad3antrrr	$⊢ ((((X \neq \emptyset \land D \in PsMet (X)) \land v \in ((X \times X) filGen F)) \land u \in F) \land u \subseteq v) \to (X \times X) filGen F \in Fil (X \times X)$
34	2	adantr	$⊢ ((X \neq \emptyset \land D \in PsMet (X)) \land v \in ((X \times X) filGen F)) \to F \in fBas (X \times X)$
35		ssfg	$⊢ F \in fBas (X \times X) \to F \subseteq (X \times X) filGen F$
36	34 35	syl	$⊢ ((X \neq \emptyset \land D \in PsMet (X)) \land v \in ((X \times X) filGen F)) \to F \subseteq (X \times X) filGen F$
37	36	ad2antrr	$⊢ ((((X \neq \emptyset \land D \in PsMet (X)) \land v \in ((X \times X) filGen F)) \land u \in F) \land u \subseteq v) \to F \subseteq (X \times X) filGen F$
38		simplr	$⊢ ((((X \neq \emptyset \land D \in PsMet (X)) \land v \in ((X \times X) filGen F)) \land u \in F) \land u \subseteq v) \to u \in F$
39	37 38	sseldd	$⊢ ((((X \neq \emptyset \land D \in PsMet (X)) \land v \in ((X \times X) filGen F)) \land u \in F) \land u \subseteq v) \to u \in ((X \times X) filGen F)$
40	29	simpld	$⊢ (F \in fBas (X \times X) \land v \in ((X \times X) filGen F)) \to v \subseteq X \times X$
41	2 40	sylan	$⊢ ((X \neq \emptyset \land D \in PsMet (X)) \land v \in ((X \times X) filGen F)) \to v \subseteq X \times X$
42	41	ad2antrr	$⊢ ((((X \neq \emptyset \land D \in PsMet (X)) \land v \in ((X \times X) filGen F)) \land u \in F) \land u \subseteq v) \to v \subseteq X \times X$
43		cnvss	$⊢ v \subseteq X \times X \to v^{-1} \subseteq {(X \times X)}^{-1}$
44		cnvxp	$⊢ {(X \times X)}^{-1} = X \times X$
45	43 44	sseqtrdi	$⊢ v \subseteq X \times X \to v^{-1} \subseteq X \times X$
46	42 45	syl	$⊢ ((((X \neq \emptyset \land D \in PsMet (X)) \land v \in ((X \times X) filGen F)) \land u \in F) \land u \subseteq v) \to v^{-1} \subseteq X \times X$
47	1	metustsym	$⊢ (D \in PsMet (X) \land u \in F) \to u^{-1} = u$
48	47	ad5ant24	$⊢ ((((X \neq \emptyset \land D \in PsMet (X)) \land v \in ((X \times X) filGen F)) \land u \in F) \land u \subseteq v) \to u^{-1} = u$
49		cnvss	$⊢ u \subseteq v \to u^{-1} \subseteq v^{-1}$
50	49	adantl	$⊢ ((((X \neq \emptyset \land D \in PsMet (X)) \land v \in ((X \times X) filGen F)) \land u \in F) \land u \subseteq v) \to u^{-1} \subseteq v^{-1}$
51	48 50	eqsstrrd	$⊢ ((((X \neq \emptyset \land D \in PsMet (X)) \land v \in ((X \times X) filGen F)) \land u \in F) \land u \subseteq v) \to u \subseteq v^{-1}$
52		filss	$⊢ ((X \times X) filGen F \in Fil (X \times X) \land (u \in ((X \times X) filGen F) \land v^{-1} \subseteq X \times X \land u \subseteq v^{-1})) \to v^{-1} \in ((X \times X) filGen F)$
53	33 39 46 51 52	syl13anc	$⊢ ((((X \neq \emptyset \land D \in PsMet (X)) \land v \in ((X \times X) filGen F)) \land u \in F) \land u \subseteq v) \to v^{-1} \in ((X \times X) filGen F)$
54	53 31	r19.29a	$⊢ ((X \neq \emptyset \land D \in PsMet (X)) \land v \in ((X \times X) filGen F)) \to v^{-1} \in ((X \times X) filGen F)$
55	1	metustexhalf	$⊢ ((X \neq \emptyset \land D \in PsMet (X)) \land u \in F) \to \exists w \in F w \circ w \subseteq u$
56	55	ad4ant13	$⊢ ((((X \neq \emptyset \land D \in PsMet (X)) \land v \in ((X \times X) filGen F)) \land u \in F) \land u \subseteq v) \to \exists w \in F w \circ w \subseteq u$
57		r19.41v	$⊢ \exists w \in F (w \circ w \subseteq u \land u \subseteq v) \leftrightarrow (\exists w \in F w \circ w \subseteq u \land u \subseteq v)$
58		sstr	$⊢ (w \circ w \subseteq u \land u \subseteq v) \to w \circ w \subseteq v$
59	58	reximi	$⊢ \exists w \in F (w \circ w \subseteq u \land u \subseteq v) \to \exists w \in F w \circ w \subseteq v$
60	57 59	sylbir	$⊢ (\exists w \in F w \circ w \subseteq u \land u \subseteq v) \to \exists w \in F w \circ w \subseteq v$
61	56 60	sylancom	$⊢ ((((X \neq \emptyset \land D \in PsMet (X)) \land v \in ((X \times X) filGen F)) \land u \in F) \land u \subseteq v) \to \exists w \in F w \circ w \subseteq v$
62	61 31	r19.29a	$⊢ ((X \neq \emptyset \land D \in PsMet (X)) \land v \in ((X \times X) filGen F)) \to \exists w \in F w \circ w \subseteq v$
63		ssrexv	$⊢ F \subseteq (X \times X) filGen F \to (\exists w \in F w \circ w \subseteq v \to \exists w \in ((X \times X) filGen F) w \circ w \subseteq v)$
64	36 62 63	sylc	$⊢ ((X \neq \emptyset \land D \in PsMet (X)) \land v \in ((X \times X) filGen F)) \to \exists w \in ((X \times X) filGen F) w \circ w \subseteq v$
65	32 54 64	3jca	$⊢ ((X \neq \emptyset \land D \in PsMet (X)) \land v \in ((X \times X) filGen F)) \to ({I ↾}_{X} \subseteq v \land v^{-1} \in ((X \times X) filGen F) \land \exists w \in ((X \times X) filGen F) w \circ w \subseteq v)$
66	17 23 65	3jca	$⊢ ((X \neq \emptyset \land D \in PsMet (X)) \land v \in ((X \times X) filGen F)) \to (\forall w \in 𝒫 (X \times X) (v \subseteq w \to w \in ((X \times X) filGen F)) \land \forall w \in ((X \times X) filGen F) v \cap w \in ((X \times X) filGen F) \land ({I ↾}_{X} \subseteq v \land v^{-1} \in ((X \times X) filGen F) \land \exists w \in ((X \times X) filGen F) w \circ w \subseteq v))$
67	66	ralrimiva	$⊢ (X \neq \emptyset \land D \in PsMet (X)) \to \forall v \in ((X \times X) filGen F) (\forall w \in 𝒫 (X \times X) (v \subseteq w \to w \in ((X \times X) filGen F)) \land \forall w \in ((X \times X) filGen F) v \cap w \in ((X \times X) filGen F) \land ({I ↾}_{X} \subseteq v \land v^{-1} \in ((X \times X) filGen F) \land \exists w \in ((X \times X) filGen F) w \circ w \subseteq v))$
68		elfvex	$⊢ D \in PsMet (X) \to X \in V$
69	68	adantl	$⊢ (X \neq \emptyset \land D \in PsMet (X)) \to X \in V$
70		isust	$⊢ X \in V \to ((X \times X) filGen F \in UnifOn (X) \leftrightarrow ((X \times X) filGen F \subseteq 𝒫 (X \times X) \land X \times X \in ((X \times X) filGen F) \land \forall v \in ((X \times X) filGen F) (\forall w \in 𝒫 (X \times X) (v \subseteq w \to w \in ((X \times X) filGen F)) \land \forall w \in ((X \times X) filGen F) v \cap w \in ((X \times X) filGen F) \land ({I ↾}_{X} \subseteq v \land v^{-1} \in ((X \times X) filGen F) \land \exists w \in ((X \times X) filGen F) w \circ w \subseteq v))))$
71	69 70	syl	$⊢ (X \neq \emptyset \land D \in PsMet (X)) \to ((X \times X) filGen F \in UnifOn (X) \leftrightarrow ((X \times X) filGen F \subseteq 𝒫 (X \times X) \land X \times X \in ((X \times X) filGen F) \land \forall v \in ((X \times X) filGen F) (\forall w \in 𝒫 (X \times X) (v \subseteq w \to w \in ((X \times X) filGen F)) \land \forall w \in ((X \times X) filGen F) v \cap w \in ((X \times X) filGen F) \land ({I ↾}_{X} \subseteq v \land v^{-1} \in ((X \times X) filGen F) \land \exists w \in ((X \times X) filGen F) w \circ w \subseteq v))))$
72	5 7 67 71	mpbir3and	$⊢ (X \neq \emptyset \land D \in PsMet (X)) \to (X \times X) filGen F \in UnifOn (X)$

Metamath Proof Explorer

Theorem metust

Proof