cfilucfil

Description: Given a metric D and a uniform structure generated by that metric, Cauchy filter bases on that uniform structure are exactly the filter bases which contain balls of any pre-chosen size. See iscfil . (Contributed by Thierry Arnoux, 29-Nov-2017) (Revised by Thierry Arnoux, 11-Feb-2018)

		Ref	Expression
	Hypothesis	metust.1	$⊢ F = ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)])$
	Assertion	cfilucfil	$⊢ (X \neq \emptyset \land D \in PsMet (X)) \to (C \in CauFilU ((X \times X) filGen F) \leftrightarrow (C \in fBas (X) \land \forall x \in ℝ^{+} \exists y \in C D [y \times y] \subseteq [0, x)))$

Proof

Step	Hyp	Ref	Expression
1		metust.1	$⊢ F = ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)])$
2	1	metust	$⊢ (X \neq \emptyset \land D \in PsMet (X)) \to (X \times X) filGen F \in UnifOn (X)$
3		cfilufbas	$⊢ ((X \times X) filGen F \in UnifOn (X) \land C \in CauFilU ((X \times X) filGen F)) \to C \in fBas (X)$
4	2 3	sylan	$⊢ ((X \neq \emptyset \land D \in PsMet (X)) \land C \in CauFilU ((X \times X) filGen F)) \to C \in fBas (X)$
5		simpllr	$⊢ (((X \neq \emptyset \land D \in PsMet (X)) \land C \in CauFilU ((X \times X) filGen F)) \land x \in ℝ^{+}) \to D \in PsMet (X)$
6		psmetf	$⊢ D \in PsMet (X) \to D : X \times X ⟶ ℝ^{*}$
7		ffun	$⊢ D : X \times X ⟶ ℝ^{*} \to Fun D$
8	5 6 7	3syl	$⊢ (((X \neq \emptyset \land D \in PsMet (X)) \land C \in CauFilU ((X \times X) filGen F)) \land x \in ℝ^{+}) \to Fun D$
9	2	ad2antrr	$⊢ (((X \neq \emptyset \land D \in PsMet (X)) \land C \in CauFilU ((X \times X) filGen F)) \land x \in ℝ^{+}) \to (X \times X) filGen F \in UnifOn (X)$
10		simplr	$⊢ (((X \neq \emptyset \land D \in PsMet (X)) \land C \in CauFilU ((X \times X) filGen F)) \land x \in ℝ^{+}) \to C \in CauFilU ((X \times X) filGen F)$
11	1	metustfbas	$⊢ (X \neq \emptyset \land D \in PsMet (X)) \to F \in fBas (X \times X)$
12	11	ad2antrr	$⊢ (((X \neq \emptyset \land D \in PsMet (X)) \land C \in CauFilU ((X \times X) filGen F)) \land x \in ℝ^{+}) \to F \in fBas (X \times X)$
13		cnvimass	$⊢ D^{-1} [[0, x)] \subseteq dom D$
14		fdm	$⊢ D : X \times X ⟶ ℝ^{*} \to dom D = X \times X$
15	5 6 14	3syl	$⊢ (((X \neq \emptyset \land D \in PsMet (X)) \land C \in CauFilU ((X \times X) filGen F)) \land x \in ℝ^{+}) \to dom D = X \times X$
16	13 15	sseqtrid	$⊢ (((X \neq \emptyset \land D \in PsMet (X)) \land C \in CauFilU ((X \times X) filGen F)) \land x \in ℝ^{+}) \to D^{-1} [[0, x)] \subseteq X \times X$
17		simpr	$⊢ (((X \neq \emptyset \land D \in PsMet (X)) \land C \in CauFilU ((X \times X) filGen F)) \land x \in ℝ^{+}) \to x \in ℝ^{+}$
18	17	rphalfcld	$⊢ (((X \neq \emptyset \land D \in PsMet (X)) \land C \in CauFilU ((X \times X) filGen F)) \land x \in ℝ^{+}) \to \frac{x}{2} \in ℝ^{+}$
19		eqidd	$⊢ (((X \neq \emptyset \land D \in PsMet (X)) \land C \in CauFilU ((X \times X) filGen F)) \land x \in ℝ^{+}) \to D^{-1} [[0, \frac{x}{2})] = D^{-1} [[0, \frac{x}{2})]$
20		oveq2	$⊢ a = \frac{x}{2} \to [0, a) = [0, \frac{x}{2})$
21	20	imaeq2d	$⊢ a = \frac{x}{2} \to D^{-1} [[0, a)] = D^{-1} [[0, \frac{x}{2})]$
22	21	rspceeqv	$⊢ (\frac{x}{2} \in ℝ^{+} \land D^{-1} [[0, \frac{x}{2})] = D^{-1} [[0, \frac{x}{2})]) \to \exists a \in ℝ^{+} D^{-1} [[0, \frac{x}{2})] = D^{-1} [[0, a)]$
23	18 19 22	syl2anc	$⊢ (((X \neq \emptyset \land D \in PsMet (X)) \land C \in CauFilU ((X \times X) filGen F)) \land x \in ℝ^{+}) \to \exists a \in ℝ^{+} D^{-1} [[0, \frac{x}{2})] = D^{-1} [[0, a)]$
24	1	metustel	$⊢ D \in PsMet (X) \to (D^{-1} [[0, \frac{x}{2})] \in F \leftrightarrow \exists a \in ℝ^{+} D^{-1} [[0, \frac{x}{2})] = D^{-1} [[0, a)])$
25	24	biimpar	$⊢ (D \in PsMet (X) \land \exists a \in ℝ^{+} D^{-1} [[0, \frac{x}{2})] = D^{-1} [[0, a)]) \to D^{-1} [[0, \frac{x}{2})] \in F$
26	5 23 25	syl2anc	$⊢ (((X \neq \emptyset \land D \in PsMet (X)) \land C \in CauFilU ((X \times X) filGen F)) \land x \in ℝ^{+}) \to D^{-1} [[0, \frac{x}{2})] \in F$
27		0xr	$⊢ 0 \in ℝ^{*}$
28	27	a1i	$⊢ x \in ℝ^{+} \to 0 \in ℝ^{*}$
29		rpxr	$⊢ x \in ℝ^{+} \to x \in ℝ^{*}$
30		0le0	$⊢ 0 \leq 0$
31	30	a1i	$⊢ x \in ℝ^{+} \to 0 \leq 0$
32		rpre	$⊢ x \in ℝ^{+} \to x \in ℝ$
33	32	rehalfcld	$⊢ x \in ℝ^{+} \to \frac{x}{2} \in ℝ$
34		rphalflt	$⊢ x \in ℝ^{+} \to \frac{x}{2} < x$
35	33 32 34	ltled	$⊢ x \in ℝ^{+} \to \frac{x}{2} \leq x$
36		icossico	$⊢ ((0 \in ℝ^{} \land x \in ℝ^{}) \land (0 \leq 0 \land \frac{x}{2} \leq x)) \to [0, \frac{x}{2}) \subseteq [0, x)$
37	28 29 31 35 36	syl22anc	$⊢ x \in ℝ^{+} \to [0, \frac{x}{2}) \subseteq [0, x)$
38		imass2	$⊢ [0, \frac{x}{2}) \subseteq [0, x) \to D^{-1} [[0, \frac{x}{2})] \subseteq D^{-1} [[0, x)]$
39	17 37 38	3syl	$⊢ (((X \neq \emptyset \land D \in PsMet (X)) \land C \in CauFilU ((X \times X) filGen F)) \land x \in ℝ^{+}) \to D^{-1} [[0, \frac{x}{2})] \subseteq D^{-1} [[0, x)]$
40		sseq1	$⊢ w = D^{-1} [[0, \frac{x}{2})] \to (w \subseteq D^{-1} [[0, x)] \leftrightarrow D^{-1} [[0, \frac{x}{2})] \subseteq D^{-1} [[0, x)])$
41	40	rspcev	$⊢ (D^{-1} [[0, \frac{x}{2})] \in F \land D^{-1} [[0, \frac{x}{2})] \subseteq D^{-1} [[0, x)]) \to \exists w \in F w \subseteq D^{-1} [[0, x)]$
42	26 39 41	syl2anc	$⊢ (((X \neq \emptyset \land D \in PsMet (X)) \land C \in CauFilU ((X \times X) filGen F)) \land x \in ℝ^{+}) \to \exists w \in F w \subseteq D^{-1} [[0, x)]$
43		elfg	$⊢ F \in fBas (X \times X) \to (D^{-1} [[0, x)] \in ((X \times X) filGen F) \leftrightarrow (D^{-1} [[0, x)] \subseteq X \times X \land \exists w \in F w \subseteq D^{-1} [[0, x)]))$
44	43	biimpar	$⊢ (F \in fBas (X \times X) \land (D^{-1} [[0, x)] \subseteq X \times X \land \exists w \in F w \subseteq D^{-1} [[0, x)])) \to D^{-1} [[0, x)] \in ((X \times X) filGen F)$
45	12 16 42 44	syl12anc	$⊢ (((X \neq \emptyset \land D \in PsMet (X)) \land C \in CauFilU ((X \times X) filGen F)) \land x \in ℝ^{+}) \to D^{-1} [[0, x)] \in ((X \times X) filGen F)$
46		cfiluexsm	$⊢ ((X \times X) filGen F \in UnifOn (X) \land C \in CauFilU ((X \times X) filGen F) \land D^{-1} [[0, x)] \in ((X \times X) filGen F)) \to \exists y \in C y \times y \subseteq D^{-1} [[0, x)]$
47	9 10 45 46	syl3anc	$⊢ (((X \neq \emptyset \land D \in PsMet (X)) \land C \in CauFilU ((X \times X) filGen F)) \land x \in ℝ^{+}) \to \exists y \in C y \times y \subseteq D^{-1} [[0, x)]$
48		funimass2	$⊢ (Fun D \land y \times y \subseteq D^{-1} [[0, x)]) \to D [y \times y] \subseteq [0, x)$
49	48	ex	$⊢ Fun D \to (y \times y \subseteq D^{-1} [[0, x)] \to D [y \times y] \subseteq [0, x))$
50	49	reximdv	$⊢ Fun D \to (\exists y \in C y \times y \subseteq D^{-1} [[0, x)] \to \exists y \in C D [y \times y] \subseteq [0, x))$
51	8 47 50	sylc	$⊢ (((X \neq \emptyset \land D \in PsMet (X)) \land C \in CauFilU ((X \times X) filGen F)) \land x \in ℝ^{+}) \to \exists y \in C D [y \times y] \subseteq [0, x)$
52	51	ralrimiva	$⊢ ((X \neq \emptyset \land D \in PsMet (X)) \land C \in CauFilU ((X \times X) filGen F)) \to \forall x \in ℝ^{+} \exists y \in C D [y \times y] \subseteq [0, x)$
53	4 52	jca	$⊢ ((X \neq \emptyset \land D \in PsMet (X)) \land C \in CauFilU ((X \times X) filGen F)) \to (C \in fBas (X) \land \forall x \in ℝ^{+} \exists y \in C D [y \times y] \subseteq [0, x))$
54		simprl	$⊢ ((X \neq \emptyset \land D \in PsMet (X)) \land (C \in fBas (X) \land \forall x \in ℝ^{+} \exists y \in C D [y \times y] \subseteq [0, x))) \to C \in fBas (X)$
55		oveq2	$⊢ x = a \to [0, x) = [0, a)$
56	55	sseq2d	$⊢ x = a \to (D [y \times y] \subseteq [0, x) \leftrightarrow D [y \times y] \subseteq [0, a))$
57	56	rexbidv	$⊢ x = a \to (\exists y \in C D [y \times y] \subseteq [0, x) \leftrightarrow \exists y \in C D [y \times y] \subseteq [0, a))$
58		simp-4r	$⊢ (((((X \neq \emptyset \land D \in PsMet (X)) \land (C \in fBas (X) \land \forall x \in ℝ^{+} \exists y \in C D [y \times y] \subseteq [0, x))) \land v \in ((X \times X) filGen F)) \land a \in ℝ^{+}) \land D^{-1} [[0, a)] \subseteq v) \to (C \in fBas (X) \land \forall x \in ℝ^{+} \exists y \in C D [y \times y] \subseteq [0, x))$
59	58	simprd	$⊢ (((((X \neq \emptyset \land D \in PsMet (X)) \land (C \in fBas (X) \land \forall x \in ℝ^{+} \exists y \in C D [y \times y] \subseteq [0, x))) \land v \in ((X \times X) filGen F)) \land a \in ℝ^{+}) \land D^{-1} [[0, a)] \subseteq v) \to \forall x \in ℝ^{+} \exists y \in C D [y \times y] \subseteq [0, x)$
60		simplr	$⊢ (((((X \neq \emptyset \land D \in PsMet (X)) \land (C \in fBas (X) \land \forall x \in ℝ^{+} \exists y \in C D [y \times y] \subseteq [0, x))) \land v \in ((X \times X) filGen F)) \land a \in ℝ^{+}) \land D^{-1} [[0, a)] \subseteq v) \to a \in ℝ^{+}$
61	57 59 60	rspcdva	$⊢ (((((X \neq \emptyset \land D \in PsMet (X)) \land (C \in fBas (X) \land \forall x \in ℝ^{+} \exists y \in C D [y \times y] \subseteq [0, x))) \land v \in ((X \times X) filGen F)) \land a \in ℝ^{+}) \land D^{-1} [[0, a)] \subseteq v) \to \exists y \in C D [y \times y] \subseteq [0, a)$
62		nfv	$⊢ Ⅎ y (X \neq \emptyset \land D \in PsMet (X))$
63		nfv	$⊢ Ⅎ y C \in fBas (X)$
64		nfcv	$⊢ \underline{Ⅎ} y ℝ^{+}$
65		nfre1	$⊢ Ⅎ y \exists y \in C D [y \times y] \subseteq [0, x)$
66	64 65	nfralw	$⊢ Ⅎ y \forall x \in ℝ^{+} \exists y \in C D [y \times y] \subseteq [0, x)$
67	63 66	nfan	$⊢ Ⅎ y (C \in fBas (X) \land \forall x \in ℝ^{+} \exists y \in C D [y \times y] \subseteq [0, x))$
68	62 67	nfan	$⊢ Ⅎ y ((X \neq \emptyset \land D \in PsMet (X)) \land (C \in fBas (X) \land \forall x \in ℝ^{+} \exists y \in C D [y \times y] \subseteq [0, x)))$
69		nfv	$⊢ Ⅎ y v \in ((X \times X) filGen F)$
70	68 69	nfan	$⊢ Ⅎ y (((X \neq \emptyset \land D \in PsMet (X)) \land (C \in fBas (X) \land \forall x \in ℝ^{+} \exists y \in C D [y \times y] \subseteq [0, x))) \land v \in ((X \times X) filGen F))$
71		nfv	$⊢ Ⅎ y a \in ℝ^{+}$
72	70 71	nfan	$⊢ Ⅎ y ((((X \neq \emptyset \land D \in PsMet (X)) \land (C \in fBas (X) \land \forall x \in ℝ^{+} \exists y \in C D [y \times y] \subseteq [0, x))) \land v \in ((X \times X) filGen F)) \land a \in ℝ^{+})$
73		nfv	$⊢ Ⅎ y D^{-1} [[0, a)] \subseteq v$
74	72 73	nfan	$⊢ Ⅎ y (((((X \neq \emptyset \land D \in PsMet (X)) \land (C \in fBas (X) \land \forall x \in ℝ^{+} \exists y \in C D [y \times y] \subseteq [0, x))) \land v \in ((X \times X) filGen F)) \land a \in ℝ^{+}) \land D^{-1} [[0, a)] \subseteq v)$
75	54	ad4antr	$⊢ ((((((X \neq \emptyset \land D \in PsMet (X)) \land (C \in fBas (X) \land \forall x \in ℝ^{+} \exists y \in C D [y \times y] \subseteq [0, x))) \land v \in ((X \times X) filGen F)) \land a \in ℝ^{+}) \land D^{-1} [[0, a)] \subseteq v) \land y \in C) \to C \in fBas (X)$
76		fbelss	$⊢ (C \in fBas (X) \land y \in C) \to y \subseteq X$
77	75 76	sylancom	$⊢ ((((((X \neq \emptyset \land D \in PsMet (X)) \land (C \in fBas (X) \land \forall x \in ℝ^{+} \exists y \in C D [y \times y] \subseteq [0, x))) \land v \in ((X \times X) filGen F)) \land a \in ℝ^{+}) \land D^{-1} [[0, a)] \subseteq v) \land y \in C) \to y \subseteq X$
78		xpss12	$⊢ (y \subseteq X \land y \subseteq X) \to y \times y \subseteq X \times X$
79	77 77 78	syl2anc	$⊢ ((((((X \neq \emptyset \land D \in PsMet (X)) \land (C \in fBas (X) \land \forall x \in ℝ^{+} \exists y \in C D [y \times y] \subseteq [0, x))) \land v \in ((X \times X) filGen F)) \land a \in ℝ^{+}) \land D^{-1} [[0, a)] \subseteq v) \land y \in C) \to y \times y \subseteq X \times X$
80		simp-6r	$⊢ ((((((X \neq \emptyset \land D \in PsMet (X)) \land (C \in fBas (X) \land \forall x \in ℝ^{+} \exists y \in C D [y \times y] \subseteq [0, x))) \land v \in ((X \times X) filGen F)) \land a \in ℝ^{+}) \land D^{-1} [[0, a)] \subseteq v) \land y \in C) \to D \in PsMet (X)$
81	80 6 14	3syl	$⊢ ((((((X \neq \emptyset \land D \in PsMet (X)) \land (C \in fBas (X) \land \forall x \in ℝ^{+} \exists y \in C D [y \times y] \subseteq [0, x))) \land v \in ((X \times X) filGen F)) \land a \in ℝ^{+}) \land D^{-1} [[0, a)] \subseteq v) \land y \in C) \to dom D = X \times X$
82	79 81	sseqtrrd	$⊢ ((((((X \neq \emptyset \land D \in PsMet (X)) \land (C \in fBas (X) \land \forall x \in ℝ^{+} \exists y \in C D [y \times y] \subseteq [0, x))) \land v \in ((X \times X) filGen F)) \land a \in ℝ^{+}) \land D^{-1} [[0, a)] \subseteq v) \land y \in C) \to y \times y \subseteq dom D$
83	82	ex	$⊢ (((((X \neq \emptyset \land D \in PsMet (X)) \land (C \in fBas (X) \land \forall x \in ℝ^{+} \exists y \in C D [y \times y] \subseteq [0, x))) \land v \in ((X \times X) filGen F)) \land a \in ℝ^{+}) \land D^{-1} [[0, a)] \subseteq v) \to (y \in C \to y \times y \subseteq dom D)$
84	74 83	ralrimi	$⊢ (((((X \neq \emptyset \land D \in PsMet (X)) \land (C \in fBas (X) \land \forall x \in ℝ^{+} \exists y \in C D [y \times y] \subseteq [0, x))) \land v \in ((X \times X) filGen F)) \land a \in ℝ^{+}) \land D^{-1} [[0, a)] \subseteq v) \to \forall y \in C y \times y \subseteq dom D$
85		r19.29r	$⊢ (\exists y \in C D [y \times y] \subseteq [0, a) \land \forall y \in C y \times y \subseteq dom D) \to \exists y \in C (D [y \times y] \subseteq [0, a) \land y \times y \subseteq dom D)$
86		sseqin2	$⊢ y \times y \subseteq dom D \leftrightarrow dom D \cap (y \times y) = y \times y$
87	86	bilani	$⊢ (D [y \times y] \subseteq [0, a) \land y \times y \subseteq dom D) \to dom D \cap (y \times y) = y \times y$
88		dminss	$⊢ dom D \cap (y \times y) \subseteq D^{-1} [D [y \times y]]$
89	87 88	eqsstrrdi	$⊢ (D [y \times y] \subseteq [0, a) \land y \times y \subseteq dom D) \to y \times y \subseteq D^{-1} [D [y \times y]]$
90		imass2	$⊢ D [y \times y] \subseteq [0, a) \to D^{-1} [D [y \times y]] \subseteq D^{-1} [[0, a)]$
91	90	adantr	$⊢ (D [y \times y] \subseteq [0, a) \land y \times y \subseteq dom D) \to D^{-1} [D [y \times y]] \subseteq D^{-1} [[0, a)]$
92	89 91	sstrd	$⊢ (D [y \times y] \subseteq [0, a) \land y \times y \subseteq dom D) \to y \times y \subseteq D^{-1} [[0, a)]$
93	92	reximi	$⊢ \exists y \in C (D [y \times y] \subseteq [0, a) \land y \times y \subseteq dom D) \to \exists y \in C y \times y \subseteq D^{-1} [[0, a)]$
94	85 93	syl	$⊢ (\exists y \in C D [y \times y] \subseteq [0, a) \land \forall y \in C y \times y \subseteq dom D) \to \exists y \in C y \times y \subseteq D^{-1} [[0, a)]$
95	61 84 94	syl2anc	$⊢ (((((X \neq \emptyset \land D \in PsMet (X)) \land (C \in fBas (X) \land \forall x \in ℝ^{+} \exists y \in C D [y \times y] \subseteq [0, x))) \land v \in ((X \times X) filGen F)) \land a \in ℝ^{+}) \land D^{-1} [[0, a)] \subseteq v) \to \exists y \in C y \times y \subseteq D^{-1} [[0, a)]$
96		r19.41v	$⊢ \exists y \in C (y \times y \subseteq D^{-1} [[0, a)] \land D^{-1} [[0, a)] \subseteq v) \leftrightarrow (\exists y \in C y \times y \subseteq D^{-1} [[0, a)] \land D^{-1} [[0, a)] \subseteq v)$
97		sstr	$⊢ (y \times y \subseteq D^{-1} [[0, a)] \land D^{-1} [[0, a)] \subseteq v) \to y \times y \subseteq v$
98	97	reximi	$⊢ \exists y \in C (y \times y \subseteq D^{-1} [[0, a)] \land D^{-1} [[0, a)] \subseteq v) \to \exists y \in C y \times y \subseteq v$
99	96 98	sylbir	$⊢ (\exists y \in C y \times y \subseteq D^{-1} [[0, a)] \land D^{-1} [[0, a)] \subseteq v) \to \exists y \in C y \times y \subseteq v$
100	95 99	sylancom	$⊢ (((((X \neq \emptyset \land D \in PsMet (X)) \land (C \in fBas (X) \land \forall x \in ℝ^{+} \exists y \in C D [y \times y] \subseteq [0, x))) \land v \in ((X \times X) filGen F)) \land a \in ℝ^{+}) \land D^{-1} [[0, a)] \subseteq v) \to \exists y \in C y \times y \subseteq v$
101		simp-5r	$⊢ (((((X \neq \emptyset \land D \in PsMet (X)) \land (C \in fBas (X) \land \forall x \in ℝ^{+} \exists y \in C D [y \times y] \subseteq [0, x))) \land v \in ((X \times X) filGen F)) \land w \in F) \land w \subseteq v) \to D \in PsMet (X)$
102		simplr	$⊢ (((((X \neq \emptyset \land D \in PsMet (X)) \land (C \in fBas (X) \land \forall x \in ℝ^{+} \exists y \in C D [y \times y] \subseteq [0, x))) \land v \in ((X \times X) filGen F)) \land w \in F) \land w \subseteq v) \to w \in F$
103	1	metustel	$⊢ D \in PsMet (X) \to (w \in F \leftrightarrow \exists a \in ℝ^{+} w = D^{-1} [[0, a)])$
104	103	biimpa	$⊢ (D \in PsMet (X) \land w \in F) \to \exists a \in ℝ^{+} w = D^{-1} [[0, a)]$
105	101 102 104	syl2anc	$⊢ (((((X \neq \emptyset \land D \in PsMet (X)) \land (C \in fBas (X) \land \forall x \in ℝ^{+} \exists y \in C D [y \times y] \subseteq [0, x))) \land v \in ((X \times X) filGen F)) \land w \in F) \land w \subseteq v) \to \exists a \in ℝ^{+} w = D^{-1} [[0, a)]$
106		r19.41v	$⊢ \exists a \in ℝ^{+} (w = D^{-1} [[0, a)] \land w \subseteq v) \leftrightarrow (\exists a \in ℝ^{+} w = D^{-1} [[0, a)] \land w \subseteq v)$
107		sseq1	$⊢ w = D^{-1} [[0, a)] \to (w \subseteq v \leftrightarrow D^{-1} [[0, a)] \subseteq v)$
108	107	biimpa	$⊢ (w = D^{-1} [[0, a)] \land w \subseteq v) \to D^{-1} [[0, a)] \subseteq v$
109	108	reximi	$⊢ \exists a \in ℝ^{+} (w = D^{-1} [[0, a)] \land w \subseteq v) \to \exists a \in ℝ^{+} D^{-1} [[0, a)] \subseteq v$
110	106 109	sylbir	$⊢ (\exists a \in ℝ^{+} w = D^{-1} [[0, a)] \land w \subseteq v) \to \exists a \in ℝ^{+} D^{-1} [[0, a)] \subseteq v$
111	105 110	sylancom	$⊢ (((((X \neq \emptyset \land D \in PsMet (X)) \land (C \in fBas (X) \land \forall x \in ℝ^{+} \exists y \in C D [y \times y] \subseteq [0, x))) \land v \in ((X \times X) filGen F)) \land w \in F) \land w \subseteq v) \to \exists a \in ℝ^{+} D^{-1} [[0, a)] \subseteq v$
112	11	ad2antrr	$⊢ (((X \neq \emptyset \land D \in PsMet (X)) \land (C \in fBas (X) \land \forall x \in ℝ^{+} \exists y \in C D [y \times y] \subseteq [0, x))) \land v \in ((X \times X) filGen F)) \to F \in fBas (X \times X)$
113		elfg	$⊢ F \in fBas (X \times X) \to (v \in ((X \times X) filGen F) \leftrightarrow (v \subseteq X \times X \land \exists w \in F w \subseteq v))$
114	113	biimpa	$⊢ (F \in fBas (X \times X) \land v \in ((X \times X) filGen F)) \to (v \subseteq X \times X \land \exists w \in F w \subseteq v)$
115	112 114	sylancom	$⊢ (((X \neq \emptyset \land D \in PsMet (X)) \land (C \in fBas (X) \land \forall x \in ℝ^{+} \exists y \in C D [y \times y] \subseteq [0, x))) \land v \in ((X \times X) filGen F)) \to (v \subseteq X \times X \land \exists w \in F w \subseteq v)$
116	115	simprd	$⊢ (((X \neq \emptyset \land D \in PsMet (X)) \land (C \in fBas (X) \land \forall x \in ℝ^{+} \exists y \in C D [y \times y] \subseteq [0, x))) \land v \in ((X \times X) filGen F)) \to \exists w \in F w \subseteq v$
117	111 116	r19.29a	$⊢ (((X \neq \emptyset \land D \in PsMet (X)) \land (C \in fBas (X) \land \forall x \in ℝ^{+} \exists y \in C D [y \times y] \subseteq [0, x))) \land v \in ((X \times X) filGen F)) \to \exists a \in ℝ^{+} D^{-1} [[0, a)] \subseteq v$
118	100 117	r19.29a	$⊢ (((X \neq \emptyset \land D \in PsMet (X)) \land (C \in fBas (X) \land \forall x \in ℝ^{+} \exists y \in C D [y \times y] \subseteq [0, x))) \land v \in ((X \times X) filGen F)) \to \exists y \in C y \times y \subseteq v$
119	118	ralrimiva	$⊢ ((X \neq \emptyset \land D \in PsMet (X)) \land (C \in fBas (X) \land \forall x \in ℝ^{+} \exists y \in C D [y \times y] \subseteq [0, x))) \to \forall v \in ((X \times X) filGen F) \exists y \in C y \times y \subseteq v$
120	2	adantr	$⊢ ((X \neq \emptyset \land D \in PsMet (X)) \land (C \in fBas (X) \land \forall x \in ℝ^{+} \exists y \in C D [y \times y] \subseteq [0, x))) \to (X \times X) filGen F \in UnifOn (X)$
121		iscfilu	$⊢ (X \times X) filGen F \in UnifOn (X) \to (C \in CauFilU ((X \times X) filGen F) \leftrightarrow (C \in fBas (X) \land \forall v \in ((X \times X) filGen F) \exists y \in C y \times y \subseteq v))$
122	120 121	syl	$⊢ ((X \neq \emptyset \land D \in PsMet (X)) \land (C \in fBas (X) \land \forall x \in ℝ^{+} \exists y \in C D [y \times y] \subseteq [0, x))) \to (C \in CauFilU ((X \times X) filGen F) \leftrightarrow (C \in fBas (X) \land \forall v \in ((X \times X) filGen F) \exists y \in C y \times y \subseteq v))$
123	54 119 122	mpbir2and	$⊢ ((X \neq \emptyset \land D \in PsMet (X)) \land (C \in fBas (X) \land \forall x \in ℝ^{+} \exists y \in C D [y \times y] \subseteq [0, x))) \to C \in CauFilU ((X \times X) filGen F)$
124	53 123	impbida	$⊢ (X \neq \emptyset \land D \in PsMet (X)) \to (C \in CauFilU ((X \times X) filGen F) \leftrightarrow (C \in fBas (X) \land \forall x \in ℝ^{+} \exists y \in C D [y \times y] \subseteq [0, x)))$

Metamath Proof Explorer

Theorem cfilucfil

Proof