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	biimpi	$⊢ y \times y \subseteq dom D \to dom D \cap (y \times y) = y \times y$
88	87	adantl	$⊢ (D [y \times y] \subseteq [0, a) \land y \times y \subseteq dom D) \to dom D \cap (y \times y) = y \times y$
89		dminss	$⊢ dom D \cap (y \times y) \subseteq D^{-1} [D [y \times y]]$
90	88 89	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]]$
91		imass2	$⊢ D [y \times y] \subseteq [0, a) \to D^{-1} [D [y \times y]] \subseteq D^{-1} [[0, a)]$
92	91	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)]$
93	90 92	sstrd	$⊢ (D [y \times y] \subseteq [0, a) \land y \times y \subseteq dom D) \to y \times y \subseteq D^{-1} [[0, a)]$
94	93	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)]$
95	85 94	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)]$
96	61 84 95	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)]$
97		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)$
98		sstr	$⊢ (y \times y \subseteq D^{-1} [[0, a)] \land D^{-1} [[0, a)] \subseteq v) \to y \times y \subseteq v$
99	98	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$
100	97 99	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$
101	96 100	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$
102		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)$
103		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$
104	1	metustel	$⊢ D \in PsMet (X) \to (w \in F \leftrightarrow \exists a \in ℝ^{+} w = D^{-1} [[0, a)])$
105	104	biimpa	$⊢ (D \in PsMet (X) \land w \in F) \to \exists a \in ℝ^{+} w = D^{-1} [[0, a)]$
106	102 103 105	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)]$
107		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)$
108		sseq1	$⊢ w = D^{-1} [[0, a)] \to (w \subseteq v \leftrightarrow D^{-1} [[0, a)] \subseteq v)$
109	108	biimpa	$⊢ (w = D^{-1} [[0, a)] \land w \subseteq v) \to D^{-1} [[0, a)] \subseteq v$
110	109	reximi	$⊢ \exists a \in ℝ^{+} (w = D^{-1} [[0, a)] \land w \subseteq v) \to \exists a \in ℝ^{+} D^{-1} [[0, a)] \subseteq v$
111	107 110	sylbir	$⊢ (\exists a \in ℝ^{+} w = D^{-1} [[0, a)] \land w \subseteq v) \to \exists a \in ℝ^{+} D^{-1} [[0, a)] \subseteq v$
112	106 111	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$
113	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)$
114		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))$
115	114	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)$
116	113 115	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)$
117	116	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$
118	112 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 a \in ℝ^{+} D^{-1} [[0, a)] \subseteq v$
119	101 118	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$
120	119	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$
121	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)$
122		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))$
123	121 122	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))$
124	54 120 123	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)$
125	53 124	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