metuel2

Description: Elementhood in the uniform structure generated by a metric D (Contributed by Thierry Arnoux, 24-Jan-2018) (Revised by Thierry Arnoux, 11-Feb-2018)

		Ref	Expression
	Hypothesis	metuel2.u	$⊢ U = metUnif (D)$
	Assertion	metuel2	$⊢ (X \neq \emptyset \land D \in PsMet (X)) \to (V \in U \leftrightarrow (V \subseteq X \times X \land \exists d \in ℝ^{+} \forall x \in X \forall y \in X (x D y < d \to x V y)))$

Proof

Step	Hyp	Ref	Expression
1		metuel2.u	$⊢ U = metUnif (D)$
2	1	eleq2i	$⊢ V \in U \leftrightarrow V \in metUnif (D)$
3	2	a1i	$⊢ (X \neq \emptyset \land D \in PsMet (X)) \to (V \in U \leftrightarrow V \in metUnif (D))$
4		metuel	$⊢ (X \neq \emptyset \land D \in PsMet (X)) \to (V \in metUnif (D) \leftrightarrow (V \subseteq X \times X \land \exists w \in ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)]) w \subseteq V))$
5		oveq2	$⊢ a = d \to [0, a) = [0, d)$
6	5	imaeq2d	$⊢ a = d \to D^{-1} [[0, a)] = D^{-1} [[0, d)]$
7	6	cbvmptv	$⊢ (a \in ℝ^{+} ⟼ D^{-1} [[0, a)]) = (d \in ℝ^{+} ⟼ D^{-1} [[0, d)])$
8	7	elrnmpt	$⊢ w \in V \to (w \in ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)]) \leftrightarrow \exists d \in ℝ^{+} w = D^{-1} [[0, d)])$
9	8	elv	$⊢ w \in ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)]) \leftrightarrow \exists d \in ℝ^{+} w = D^{-1} [[0, d)]$
10	9	anbi1i	$⊢ (w \in ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)]) \land w \subseteq V) \leftrightarrow (\exists d \in ℝ^{+} w = D^{-1} [[0, d)] \land w \subseteq V)$
11		r19.41v	$⊢ \exists d \in ℝ^{+} (w = D^{-1} [[0, d)] \land w \subseteq V) \leftrightarrow (\exists d \in ℝ^{+} w = D^{-1} [[0, d)] \land w \subseteq V)$
12	10 11	bitr4i	$⊢ (w \in ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)]) \land w \subseteq V) \leftrightarrow \exists d \in ℝ^{+} (w = D^{-1} [[0, d)] \land w \subseteq V)$
13	12	exbii	$⊢ \exists w (w \in ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)]) \land w \subseteq V) \leftrightarrow \exists w \exists d \in ℝ^{+} (w = D^{-1} [[0, d)] \land w \subseteq V)$
14		df-rex	$⊢ \exists w \in ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)]) w \subseteq V \leftrightarrow \exists w (w \in ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)]) \land w \subseteq V)$
15		rexcom4	$⊢ \exists d \in ℝ^{+} \exists w (w = D^{-1} [[0, d)] \land w \subseteq V) \leftrightarrow \exists w \exists d \in ℝ^{+} (w = D^{-1} [[0, d)] \land w \subseteq V)$
16	13 14 15	3bitr4i	$⊢ \exists w \in ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)]) w \subseteq V \leftrightarrow \exists d \in ℝ^{+} \exists w (w = D^{-1} [[0, d)] \land w \subseteq V)$
17		cnvexg	$⊢ D \in PsMet (X) \to D^{-1} \in V$
18		imaexg	$⊢ D^{-1} \in V \to D^{-1} [[0, d)] \in V$
19		sseq1	$⊢ w = D^{-1} [[0, d)] \to (w \subseteq V \leftrightarrow D^{-1} [[0, d)] \subseteq V)$
20	19	ceqsexgv	$⊢ D^{-1} [[0, d)] \in V \to (\exists w (w = D^{-1} [[0, d)] \land w \subseteq V) \leftrightarrow D^{-1} [[0, d)] \subseteq V)$
21	17 18 20	3syl	$⊢ D \in PsMet (X) \to (\exists w (w = D^{-1} [[0, d)] \land w \subseteq V) \leftrightarrow D^{-1} [[0, d)] \subseteq V)$
22	21	rexbidv	$⊢ D \in PsMet (X) \to (\exists d \in ℝ^{+} \exists w (w = D^{-1} [[0, d)] \land w \subseteq V) \leftrightarrow \exists d \in ℝ^{+} D^{-1} [[0, d)] \subseteq V)$
23	22	adantr	$⊢ (D \in PsMet (X) \land V \subseteq X \times X) \to (\exists d \in ℝ^{+} \exists w (w = D^{-1} [[0, d)] \land w \subseteq V) \leftrightarrow \exists d \in ℝ^{+} D^{-1} [[0, d)] \subseteq V)$
24	16 23	syl5bb	$⊢ (D \in PsMet (X) \land V \subseteq X \times X) \to (\exists w \in ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)]) w \subseteq V \leftrightarrow \exists d \in ℝ^{+} D^{-1} [[0, d)] \subseteq V)$
25		cnvimass	$⊢ D^{-1} [[0, d)] \subseteq dom D$
26		simpll	$⊢ ((D \in PsMet (X) \land V \subseteq X \times X) \land d \in ℝ^{+}) \to D \in PsMet (X)$
27		psmetf	$⊢ D \in PsMet (X) \to D : X \times X ⟶ ℝ^{*}$
28		fdm	$⊢ D : X \times X ⟶ ℝ^{*} \to dom D = X \times X$
29	26 27 28	3syl	$⊢ ((D \in PsMet (X) \land V \subseteq X \times X) \land d \in ℝ^{+}) \to dom D = X \times X$
30	25 29	sseqtrid	$⊢ ((D \in PsMet (X) \land V \subseteq X \times X) \land d \in ℝ^{+}) \to D^{-1} [[0, d)] \subseteq X \times X$
31		ssrel2	$⊢ D^{-1} [[0, d)] \subseteq X \times X \to (D^{-1} [[0, d)] \subseteq V \leftrightarrow \forall x \in X \forall y \in X (⟨x, y⟩ \in D^{-1} [[0, d)] \to ⟨x, y⟩ \in V))$
32	30 31	syl	$⊢ ((D \in PsMet (X) \land V \subseteq X \times X) \land d \in ℝ^{+}) \to (D^{-1} [[0, d)] \subseteq V \leftrightarrow \forall x \in X \forall y \in X (⟨x, y⟩ \in D^{-1} [[0, d)] \to ⟨x, y⟩ \in V))$
33		simplr	$⊢ ((((D \in PsMet (X) \land V \subseteq X \times X) \land d \in ℝ^{+}) \land x \in X) \land y \in X) \to x \in X$
34		simpr	$⊢ ((((D \in PsMet (X) \land V \subseteq X \times X) \land d \in ℝ^{+}) \land x \in X) \land y \in X) \to y \in X$
35	33 34	opelxpd	$⊢ ((((D \in PsMet (X) \land V \subseteq X \times X) \land d \in ℝ^{+}) \land x \in X) \land y \in X) \to ⟨x, y⟩ \in (X \times X)$
36	35	biantrurd	$⊢ ((((D \in PsMet (X) \land V \subseteq X \times X) \land d \in ℝ^{+}) \land x \in X) \land y \in X) \to (D (⟨x, y⟩) \in [0, d) \leftrightarrow (⟨x, y⟩ \in (X \times X) \land D (⟨x, y⟩) \in [0, d)))$
37		psmetcl	$⊢ (D \in PsMet (X) \land x \in X \land y \in X) \to x D y \in ℝ^{*}$
38	37	ad5ant145	$⊢ ((((D \in PsMet (X) \land V \subseteq X \times X) \land d \in ℝ^{+}) \land x \in X) \land y \in X) \to x D y \in ℝ^{*}$
39	38	3biant1d	$⊢ ((((D \in PsMet (X) \land V \subseteq X \times X) \land d \in ℝ^{+}) \land x \in X) \land y \in X) \to ((0 \leq x D y \land x D y < d) \leftrightarrow (x D y \in ℝ^{*} \land 0 \leq x D y \land x D y < d))$
40		psmetge0	$⊢ (D \in PsMet (X) \land x \in X \land y \in X) \to 0 \leq x D y$
41	40	biantrurd	$⊢ (D \in PsMet (X) \land x \in X \land y \in X) \to (x D y < d \leftrightarrow (0 \leq x D y \land x D y < d))$
42	41	ad5ant145	$⊢ ((((D \in PsMet (X) \land V \subseteq X \times X) \land d \in ℝ^{+}) \land x \in X) \land y \in X) \to (x D y < d \leftrightarrow (0 \leq x D y \land x D y < d))$
43		0xr	$⊢ 0 \in ℝ^{*}$
44		simpllr	$⊢ ((((D \in PsMet (X) \land V \subseteq X \times X) \land d \in ℝ^{+}) \land x \in X) \land y \in X) \to d \in ℝ^{+}$
45	44	rpxrd	$⊢ ((((D \in PsMet (X) \land V \subseteq X \times X) \land d \in ℝ^{+}) \land x \in X) \land y \in X) \to d \in ℝ^{*}$
46		elico1	$⊢ (0 \in ℝ^{} \land d \in ℝ^{}) \to (x D y \in [0, d) \leftrightarrow (x D y \in ℝ^{*} \land 0 \leq x D y \land x D y < d))$
47	43 45 46	sylancr	$⊢ ((((D \in PsMet (X) \land V \subseteq X \times X) \land d \in ℝ^{+}) \land x \in X) \land y \in X) \to (x D y \in [0, d) \leftrightarrow (x D y \in ℝ^{*} \land 0 \leq x D y \land x D y < d))$
48	39 42 47	3bitr4d	$⊢ ((((D \in PsMet (X) \land V \subseteq X \times X) \land d \in ℝ^{+}) \land x \in X) \land y \in X) \to (x D y < d \leftrightarrow x D y \in [0, d))$
49		df-ov	$⊢ x D y = D (⟨x, y⟩)$
50	49	eleq1i	$⊢ x D y \in [0, d) \leftrightarrow D (⟨x, y⟩) \in [0, d)$
51	48 50	syl6bb	$⊢ ((((D \in PsMet (X) \land V \subseteq X \times X) \land d \in ℝ^{+}) \land x \in X) \land y \in X) \to (x D y < d \leftrightarrow D (⟨x, y⟩) \in [0, d))$
52		simp-4l	$⊢ ((((D \in PsMet (X) \land V \subseteq X \times X) \land d \in ℝ^{+}) \land x \in X) \land y \in X) \to D \in PsMet (X)$
53		ffn	$⊢ D : X \times X ⟶ ℝ^{*} \to D Fn (X \times X)$
54		elpreima	$⊢ D Fn (X \times X) \to (⟨x, y⟩ \in D^{-1} [[0, d)] \leftrightarrow (⟨x, y⟩ \in (X \times X) \land D (⟨x, y⟩) \in [0, d)))$
55	52 27 53 54	4syl	$⊢ ((((D \in PsMet (X) \land V \subseteq X \times X) \land d \in ℝ^{+}) \land x \in X) \land y \in X) \to (⟨x, y⟩ \in D^{-1} [[0, d)] \leftrightarrow (⟨x, y⟩ \in (X \times X) \land D (⟨x, y⟩) \in [0, d)))$
56	36 51 55	3bitr4d	$⊢ ((((D \in PsMet (X) \land V \subseteq X \times X) \land d \in ℝ^{+}) \land x \in X) \land y \in X) \to (x D y < d \leftrightarrow ⟨x, y⟩ \in D^{-1} [[0, d)])$
57	56	anasss	$⊢ (((D \in PsMet (X) \land V \subseteq X \times X) \land d \in ℝ^{+}) \land (x \in X \land y \in X)) \to (x D y < d \leftrightarrow ⟨x, y⟩ \in D^{-1} [[0, d)])$
58		df-br	$⊢ x V y \leftrightarrow ⟨x, y⟩ \in V$
59	58	a1i	$⊢ (((D \in PsMet (X) \land V \subseteq X \times X) \land d \in ℝ^{+}) \land (x \in X \land y \in X)) \to (x V y \leftrightarrow ⟨x, y⟩ \in V)$
60	57 59	imbi12d	$⊢ (((D \in PsMet (X) \land V \subseteq X \times X) \land d \in ℝ^{+}) \land (x \in X \land y \in X)) \to ((x D y < d \to x V y) \leftrightarrow (⟨x, y⟩ \in D^{-1} [[0, d)] \to ⟨x, y⟩ \in V))$
61	60	2ralbidva	$⊢ ((D \in PsMet (X) \land V \subseteq X \times X) \land d \in ℝ^{+}) \to (\forall x \in X \forall y \in X (x D y < d \to x V y) \leftrightarrow \forall x \in X \forall y \in X (⟨x, y⟩ \in D^{-1} [[0, d)] \to ⟨x, y⟩ \in V))$
62	32 61	bitr4d	$⊢ ((D \in PsMet (X) \land V \subseteq X \times X) \land d \in ℝ^{+}) \to (D^{-1} [[0, d)] \subseteq V \leftrightarrow \forall x \in X \forall y \in X (x D y < d \to x V y))$
63	62	rexbidva	$⊢ (D \in PsMet (X) \land V \subseteq X \times X) \to (\exists d \in ℝ^{+} D^{-1} [[0, d)] \subseteq V \leftrightarrow \exists d \in ℝ^{+} \forall x \in X \forall y \in X (x D y < d \to x V y))$
64	24 63	bitrd	$⊢ (D \in PsMet (X) \land V \subseteq X \times X) \to (\exists w \in ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)]) w \subseteq V \leftrightarrow \exists d \in ℝ^{+} \forall x \in X \forall y \in X (x D y < d \to x V y))$
65	64	pm5.32da	$⊢ D \in PsMet (X) \to ((V \subseteq X \times X \land \exists w \in ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)]) w \subseteq V) \leftrightarrow (V \subseteq X \times X \land \exists d \in ℝ^{+} \forall x \in X \forall y \in X (x D y < d \to x V y)))$
66	65	adantl	$⊢ (X \neq \emptyset \land D \in PsMet (X)) \to ((V \subseteq X \times X \land \exists w \in ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)]) w \subseteq V) \leftrightarrow (V \subseteq X \times X \land \exists d \in ℝ^{+} \forall x \in X \forall y \in X (x D y < d \to x V y)))$
67	3 4 66	3bitrd	$⊢ (X \neq \emptyset \land D \in PsMet (X)) \to (V \in U \leftrightarrow (V \subseteq X \times X \land \exists d \in ℝ^{+} \forall x \in X \forall y \in X (x D y < d \to x V y)))$

Metamath Proof Explorer

Theorem metuel2

Proof