metustexhalf

Description: For any element A of the filter base generated by the metric D , the half element (corresponding to half the distance) is also in this base. (Contributed by Thierry Arnoux, 28-Nov-2017) (Revised by Thierry Arnoux, 11-Feb-2018)

		Ref	Expression
	Hypothesis	metust.1	$⊢ F = ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)])$
	Assertion	metustexhalf	$⊢ ((X \neq \emptyset \land D \in PsMet (X)) \land A \in F) \to \exists v \in F v \circ v \subseteq A$

Proof

Step	Hyp	Ref	Expression
1		metust.1	$⊢ F = ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)])$
2		simp-4r	$⊢ ((((X \neq \emptyset \land D \in PsMet (X)) \land A \in F) \land a \in ℝ^{+}) \land A = D^{-1} [[0, a)]) \to D \in PsMet (X)$
3		simplr	$⊢ ((((X \neq \emptyset \land D \in PsMet (X)) \land A \in F) \land a \in ℝ^{+}) \land A = D^{-1} [[0, a)]) \to a \in ℝ^{+}$
4	3	rphalfcld	$⊢ ((((X \neq \emptyset \land D \in PsMet (X)) \land A \in F) \land a \in ℝ^{+}) \land A = D^{-1} [[0, a)]) \to \frac{a}{2} \in ℝ^{+}$
5		eqidd	$⊢ ((((X \neq \emptyset \land D \in PsMet (X)) \land A \in F) \land a \in ℝ^{+}) \land A = D^{-1} [[0, a)]) \to D^{-1} [[0, \frac{a}{2})] = D^{-1} [[0, \frac{a}{2})]$
6		oveq2	$⊢ b = \frac{a}{2} \to [0, b) = [0, \frac{a}{2})$
7	6	imaeq2d	$⊢ b = \frac{a}{2} \to D^{-1} [[0, b)] = D^{-1} [[0, \frac{a}{2})]$
8	7	rspceeqv	$⊢ (\frac{a}{2} \in ℝ^{+} \land D^{-1} [[0, \frac{a}{2})] = D^{-1} [[0, \frac{a}{2})]) \to \exists b \in ℝ^{+} D^{-1} [[0, \frac{a}{2})] = D^{-1} [[0, b)]$
9	4 5 8	syl2anc	$⊢ ((((X \neq \emptyset \land D \in PsMet (X)) \land A \in F) \land a \in ℝ^{+}) \land A = D^{-1} [[0, a)]) \to \exists b \in ℝ^{+} D^{-1} [[0, \frac{a}{2})] = D^{-1} [[0, b)]$
10		oveq2	$⊢ a = b \to [0, a) = [0, b)$
11	10	imaeq2d	$⊢ a = b \to D^{-1} [[0, a)] = D^{-1} [[0, b)]$
12	11	cbvmptv	$⊢ (a \in ℝ^{+} ⟼ D^{-1} [[0, a)]) = (b \in ℝ^{+} ⟼ D^{-1} [[0, b)])$
13	12	rneqi	$⊢ ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)]) = ran (b \in ℝ^{+} ⟼ D^{-1} [[0, b)])$
14	1 13	eqtri	$⊢ F = ran (b \in ℝ^{+} ⟼ D^{-1} [[0, b)])$
15	14	metustel	$⊢ D \in PsMet (X) \to (D^{-1} [[0, \frac{a}{2})] \in F \leftrightarrow \exists b \in ℝ^{+} D^{-1} [[0, \frac{a}{2})] = D^{-1} [[0, b)])$
16	15	biimpar	$⊢ (D \in PsMet (X) \land \exists b \in ℝ^{+} D^{-1} [[0, \frac{a}{2})] = D^{-1} [[0, b)]) \to D^{-1} [[0, \frac{a}{2})] \in F$
17	2 9 16	syl2anc	$⊢ ((((X \neq \emptyset \land D \in PsMet (X)) \land A \in F) \land a \in ℝ^{+}) \land A = D^{-1} [[0, a)]) \to D^{-1} [[0, \frac{a}{2})] \in F$
18		relco	$⊢ Rel (D^{-1} [[0, \frac{a}{2})] \circ D^{-1} [[0, \frac{a}{2})])$
19	18	a1i	$⊢ ((((X \neq \emptyset \land D \in PsMet (X)) \land A \in F) \land a \in ℝ^{+}) \land A = D^{-1} [[0, a)]) \to Rel (D^{-1} [[0, \frac{a}{2})] \circ D^{-1} [[0, \frac{a}{2})])$
20		cossxp	$⊢ D^{-1} [[0, \frac{a}{2})] \circ D^{-1} [[0, \frac{a}{2})] \subseteq dom D^{-1} [[0, \frac{a}{2})] \times ran D^{-1} [[0, \frac{a}{2})]$
21		cnvimass	$⊢ D^{-1} [[0, \frac{a}{2})] \subseteq dom D$
22		psmetf	$⊢ D \in PsMet (X) \to D : X \times X ⟶ ℝ^{*}$
23	21 22	fssdm	$⊢ D \in PsMet (X) \to D^{-1} [[0, \frac{a}{2})] \subseteq X \times X$
24		dmss	$⊢ D^{-1} [[0, \frac{a}{2})] \subseteq X \times X \to dom D^{-1} [[0, \frac{a}{2})] \subseteq dom (X \times X)$
25		rnss	$⊢ D^{-1} [[0, \frac{a}{2})] \subseteq X \times X \to ran D^{-1} [[0, \frac{a}{2})] \subseteq ran (X \times X)$
26		xpss12	$⊢ (dom D^{-1} [[0, \frac{a}{2})] \subseteq dom (X \times X) \land ran D^{-1} [[0, \frac{a}{2})] \subseteq ran (X \times X)) \to dom D^{-1} [[0, \frac{a}{2})] \times ran D^{-1} [[0, \frac{a}{2})] \subseteq dom (X \times X) \times ran (X \times X)$
27	24 25 26	syl2anc	$⊢ D^{-1} [[0, \frac{a}{2})] \subseteq X \times X \to dom D^{-1} [[0, \frac{a}{2})] \times ran D^{-1} [[0, \frac{a}{2})] \subseteq dom (X \times X) \times ran (X \times X)$
28	23 27	syl	$⊢ D \in PsMet (X) \to dom D^{-1} [[0, \frac{a}{2})] \times ran D^{-1} [[0, \frac{a}{2})] \subseteq dom (X \times X) \times ran (X \times X)$
29	28	adantl	$⊢ (X \neq \emptyset \land D \in PsMet (X)) \to dom D^{-1} [[0, \frac{a}{2})] \times ran D^{-1} [[0, \frac{a}{2})] \subseteq dom (X \times X) \times ran (X \times X)$
30		dmxp	$⊢ X \neq \emptyset \to dom (X \times X) = X$
31		rnxp	$⊢ X \neq \emptyset \to ran (X \times X) = X$
32	30 31	xpeq12d	$⊢ X \neq \emptyset \to dom (X \times X) \times ran (X \times X) = X \times X$
33	32	adantr	$⊢ (X \neq \emptyset \land D \in PsMet (X)) \to dom (X \times X) \times ran (X \times X) = X \times X$
34	29 33	sseqtrd	$⊢ (X \neq \emptyset \land D \in PsMet (X)) \to dom D^{-1} [[0, \frac{a}{2})] \times ran D^{-1} [[0, \frac{a}{2})] \subseteq X \times X$
35	20 34	sstrid	$⊢ (X \neq \emptyset \land D \in PsMet (X)) \to D^{-1} [[0, \frac{a}{2})] \circ D^{-1} [[0, \frac{a}{2})] \subseteq X \times X$
36	35	ad3antrrr	$⊢ ((((X \neq \emptyset \land D \in PsMet (X)) \land A \in F) \land a \in ℝ^{+}) \land A = D^{-1} [[0, a)]) \to D^{-1} [[0, \frac{a}{2})] \circ D^{-1} [[0, \frac{a}{2})] \subseteq X \times X$
37	36	sselda	$⊢ (((((X \neq \emptyset \land D \in PsMet (X)) \land A \in F) \land a \in ℝ^{+}) \land A = D^{-1} [[0, a)]) \land ⟨p, q⟩ \in (D^{-1} [[0, \frac{a}{2})] \circ D^{-1} [[0, \frac{a}{2})])) \to ⟨p, q⟩ \in (X \times X)$
38		opelxp	$⊢ ⟨p, q⟩ \in (X \times X) \leftrightarrow (p \in X \land q \in X)$
39	37 38	sylib	$⊢ (((((X \neq \emptyset \land D \in PsMet (X)) \land A \in F) \land a \in ℝ^{+}) \land A = D^{-1} [[0, a)]) \land ⟨p, q⟩ \in (D^{-1} [[0, \frac{a}{2})] \circ D^{-1} [[0, \frac{a}{2})])) \to (p \in X \land q \in X)$
40		simpll	$⊢ ((((((X \neq \emptyset \land D \in PsMet (X)) \land A \in F) \land a \in ℝ^{+}) \land A = D^{-1} [[0, a)]) \land ⟨p, q⟩ \in (D^{-1} [[0, \frac{a}{2})] \circ D^{-1} [[0, \frac{a}{2})])) \land (p \in X \land q \in X)) \to ((((X \neq \emptyset \land D \in PsMet (X)) \land A \in F) \land a \in ℝ^{+}) \land A = D^{-1} [[0, a)])$
41		simprl	$⊢ ((((((X \neq \emptyset \land D \in PsMet (X)) \land A \in F) \land a \in ℝ^{+}) \land A = D^{-1} [[0, a)]) \land ⟨p, q⟩ \in (D^{-1} [[0, \frac{a}{2})] \circ D^{-1} [[0, \frac{a}{2})])) \land (p \in X \land q \in X)) \to p \in X$
42		simprr	$⊢ ((((((X \neq \emptyset \land D \in PsMet (X)) \land A \in F) \land a \in ℝ^{+}) \land A = D^{-1} [[0, a)]) \land ⟨p, q⟩ \in (D^{-1} [[0, \frac{a}{2})] \circ D^{-1} [[0, \frac{a}{2})])) \land (p \in X \land q \in X)) \to q \in X$
43		simplr	$⊢ ((((((X \neq \emptyset \land D \in PsMet (X)) \land A \in F) \land a \in ℝ^{+}) \land A = D^{-1} [[0, a)]) \land ⟨p, q⟩ \in (D^{-1} [[0, \frac{a}{2})] \circ D^{-1} [[0, \frac{a}{2})])) \land (p \in X \land q \in X)) \to ⟨p, q⟩ \in (D^{-1} [[0, \frac{a}{2})] \circ D^{-1} [[0, \frac{a}{2})])$
44		simplll	$⊢ ((((((((X \neq \emptyset \land D \in PsMet (X)) \land A \in F) \land a \in ℝ^{+}) \land A = D^{-1} [[0, a)]) \land p \in X \land q \in X) \land ⟨p, q⟩ \in (D^{-1} [[0, \frac{a}{2})] \circ D^{-1} [[0, \frac{a}{2})])) \land r \in X) \land (p D^{-1} [[0, \frac{a}{2})] r \land r D^{-1} [[0, \frac{a}{2})] q)) \to (((((X \neq \emptyset \land D \in PsMet (X)) \land A \in F) \land a \in ℝ^{+}) \land A = D^{-1} [[0, a)]) \land p \in X \land q \in X)$
45	44	simp1d	$⊢ ((((((((X \neq \emptyset \land D \in PsMet (X)) \land A \in F) \land a \in ℝ^{+}) \land A = D^{-1} [[0, a)]) \land p \in X \land q \in X) \land ⟨p, q⟩ \in (D^{-1} [[0, \frac{a}{2})] \circ D^{-1} [[0, \frac{a}{2})])) \land r \in X) \land (p D^{-1} [[0, \frac{a}{2})] r \land r D^{-1} [[0, \frac{a}{2})] q)) \to ((((X \neq \emptyset \land D \in PsMet (X)) \land A \in F) \land a \in ℝ^{+}) \land A = D^{-1} [[0, a)])$
46	45 2	syl	$⊢ ((((((((X \neq \emptyset \land D \in PsMet (X)) \land A \in F) \land a \in ℝ^{+}) \land A = D^{-1} [[0, a)]) \land p \in X \land q \in X) \land ⟨p, q⟩ \in (D^{-1} [[0, \frac{a}{2})] \circ D^{-1} [[0, \frac{a}{2})])) \land r \in X) \land (p D^{-1} [[0, \frac{a}{2})] r \land r D^{-1} [[0, \frac{a}{2})] q)) \to D \in PsMet (X)$
47	45 3	syl	$⊢ ((((((((X \neq \emptyset \land D \in PsMet (X)) \land A \in F) \land a \in ℝ^{+}) \land A = D^{-1} [[0, a)]) \land p \in X \land q \in X) \land ⟨p, q⟩ \in (D^{-1} [[0, \frac{a}{2})] \circ D^{-1} [[0, \frac{a}{2})])) \land r \in X) \land (p D^{-1} [[0, \frac{a}{2})] r \land r D^{-1} [[0, \frac{a}{2})] q)) \to a \in ℝ^{+}$
48	46 47	jca	$⊢ ((((((((X \neq \emptyset \land D \in PsMet (X)) \land A \in F) \land a \in ℝ^{+}) \land A = D^{-1} [[0, a)]) \land p \in X \land q \in X) \land ⟨p, q⟩ \in (D^{-1} [[0, \frac{a}{2})] \circ D^{-1} [[0, \frac{a}{2})])) \land r \in X) \land (p D^{-1} [[0, \frac{a}{2})] r \land r D^{-1} [[0, \frac{a}{2})] q)) \to (D \in PsMet (X) \land a \in ℝ^{+})$
49	44	simp2d	$⊢ ((((((((X \neq \emptyset \land D \in PsMet (X)) \land A \in F) \land a \in ℝ^{+}) \land A = D^{-1} [[0, a)]) \land p \in X \land q \in X) \land ⟨p, q⟩ \in (D^{-1} [[0, \frac{a}{2})] \circ D^{-1} [[0, \frac{a}{2})])) \land r \in X) \land (p D^{-1} [[0, \frac{a}{2})] r \land r D^{-1} [[0, \frac{a}{2})] q)) \to p \in X$
50	44	simp3d	$⊢ ((((((((X \neq \emptyset \land D \in PsMet (X)) \land A \in F) \land a \in ℝ^{+}) \land A = D^{-1} [[0, a)]) \land p \in X \land q \in X) \land ⟨p, q⟩ \in (D^{-1} [[0, \frac{a}{2})] \circ D^{-1} [[0, \frac{a}{2})])) \land r \in X) \land (p D^{-1} [[0, \frac{a}{2})] r \land r D^{-1} [[0, \frac{a}{2})] q)) \to q \in X$
51	48 49 50	3jca	$⊢ ((((((((X \neq \emptyset \land D \in PsMet (X)) \land A \in F) \land a \in ℝ^{+}) \land A = D^{-1} [[0, a)]) \land p \in X \land q \in X) \land ⟨p, q⟩ \in (D^{-1} [[0, \frac{a}{2})] \circ D^{-1} [[0, \frac{a}{2})])) \land r \in X) \land (p D^{-1} [[0, \frac{a}{2})] r \land r D^{-1} [[0, \frac{a}{2})] q)) \to ((D \in PsMet (X) \land a \in ℝ^{+}) \land p \in X \land q \in X)$
52		simplr	$⊢ ((((((((X \neq \emptyset \land D \in PsMet (X)) \land A \in F) \land a \in ℝ^{+}) \land A = D^{-1} [[0, a)]) \land p \in X \land q \in X) \land ⟨p, q⟩ \in (D^{-1} [[0, \frac{a}{2})] \circ D^{-1} [[0, \frac{a}{2})])) \land r \in X) \land (p D^{-1} [[0, \frac{a}{2})] r \land r D^{-1} [[0, \frac{a}{2})] q)) \to r \in X$
53		simprl	$⊢ ((((((((X \neq \emptyset \land D \in PsMet (X)) \land A \in F) \land a \in ℝ^{+}) \land A = D^{-1} [[0, a)]) \land p \in X \land q \in X) \land ⟨p, q⟩ \in (D^{-1} [[0, \frac{a}{2})] \circ D^{-1} [[0, \frac{a}{2})])) \land r \in X) \land (p D^{-1} [[0, \frac{a}{2})] r \land r D^{-1} [[0, \frac{a}{2})] q)) \to p D^{-1} [[0, \frac{a}{2})] r$
54		simprr	$⊢ ((((((((X \neq \emptyset \land D \in PsMet (X)) \land A \in F) \land a \in ℝ^{+}) \land A = D^{-1} [[0, a)]) \land p \in X \land q \in X) \land ⟨p, q⟩ \in (D^{-1} [[0, \frac{a}{2})] \circ D^{-1} [[0, \frac{a}{2})])) \land r \in X) \land (p D^{-1} [[0, \frac{a}{2})] r \land r D^{-1} [[0, \frac{a}{2})] q)) \to r D^{-1} [[0, \frac{a}{2})] q$
55		simpll	$⊢ ((((D \in PsMet (X) \land a \in ℝ^{+}) \land p \in X \land q \in X) \land r \in X) \land (p D^{-1} [[0, \frac{a}{2})] r \land r D^{-1} [[0, \frac{a}{2})] q)) \to ((D \in PsMet (X) \land a \in ℝ^{+}) \land p \in X \land q \in X)$
56	55	simp1d	$⊢ ((((D \in PsMet (X) \land a \in ℝ^{+}) \land p \in X \land q \in X) \land r \in X) \land (p D^{-1} [[0, \frac{a}{2})] r \land r D^{-1} [[0, \frac{a}{2})] q)) \to (D \in PsMet (X) \land a \in ℝ^{+})$
57	56	simpld	$⊢ ((((D \in PsMet (X) \land a \in ℝ^{+}) \land p \in X \land q \in X) \land r \in X) \land (p D^{-1} [[0, \frac{a}{2})] r \land r D^{-1} [[0, \frac{a}{2})] q)) \to D \in PsMet (X)$
58	22	ffund	$⊢ D \in PsMet (X) \to Fun D$
59	57 58	syl	$⊢ ((((D \in PsMet (X) \land a \in ℝ^{+}) \land p \in X \land q \in X) \land r \in X) \land (p D^{-1} [[0, \frac{a}{2})] r \land r D^{-1} [[0, \frac{a}{2})] q)) \to Fun D$
60	55	simp2d	$⊢ ((((D \in PsMet (X) \land a \in ℝ^{+}) \land p \in X \land q \in X) \land r \in X) \land (p D^{-1} [[0, \frac{a}{2})] r \land r D^{-1} [[0, \frac{a}{2})] q)) \to p \in X$
61	55	simp3d	$⊢ ((((D \in PsMet (X) \land a \in ℝ^{+}) \land p \in X \land q \in X) \land r \in X) \land (p D^{-1} [[0, \frac{a}{2})] r \land r D^{-1} [[0, \frac{a}{2})] q)) \to q \in X$
62	60 61	opelxpd	$⊢ ((((D \in PsMet (X) \land a \in ℝ^{+}) \land p \in X \land q \in X) \land r \in X) \land (p D^{-1} [[0, \frac{a}{2})] r \land r D^{-1} [[0, \frac{a}{2})] q)) \to ⟨p, q⟩ \in (X \times X)$
63	22	fdmd	$⊢ D \in PsMet (X) \to dom D = X \times X$
64	57 63	syl	$⊢ ((((D \in PsMet (X) \land a \in ℝ^{+}) \land p \in X \land q \in X) \land r \in X) \land (p D^{-1} [[0, \frac{a}{2})] r \land r D^{-1} [[0, \frac{a}{2})] q)) \to dom D = X \times X$
65	62 64	eleqtrrd	$⊢ ((((D \in PsMet (X) \land a \in ℝ^{+}) \land p \in X \land q \in X) \land r \in X) \land (p D^{-1} [[0, \frac{a}{2})] r \land r D^{-1} [[0, \frac{a}{2})] q)) \to ⟨p, q⟩ \in dom D$
66		0xr	$⊢ 0 \in ℝ^{*}$
67	66	a1i	$⊢ ((((D \in PsMet (X) \land a \in ℝ^{+}) \land p \in X \land q \in X) \land r \in X) \land (p D^{-1} [[0, \frac{a}{2})] r \land r D^{-1} [[0, \frac{a}{2})] q)) \to 0 \in ℝ^{*}$
68	56	simprd	$⊢ ((((D \in PsMet (X) \land a \in ℝ^{+}) \land p \in X \land q \in X) \land r \in X) \land (p D^{-1} [[0, \frac{a}{2})] r \land r D^{-1} [[0, \frac{a}{2})] q)) \to a \in ℝ^{+}$
69	68	rpxrd	$⊢ ((((D \in PsMet (X) \land a \in ℝ^{+}) \land p \in X \land q \in X) \land r \in X) \land (p D^{-1} [[0, \frac{a}{2})] r \land r D^{-1} [[0, \frac{a}{2})] q)) \to a \in ℝ^{*}$
70	57 22	syl	$⊢ ((((D \in PsMet (X) \land a \in ℝ^{+}) \land p \in X \land q \in X) \land r \in X) \land (p D^{-1} [[0, \frac{a}{2})] r \land r D^{-1} [[0, \frac{a}{2})] q)) \to D : X \times X ⟶ ℝ^{*}$
71	70 62	ffvelcdmd	$⊢ ((((D \in PsMet (X) \land a \in ℝ^{+}) \land p \in X \land q \in X) \land r \in X) \land (p D^{-1} [[0, \frac{a}{2})] r \land r D^{-1} [[0, \frac{a}{2})] q)) \to D (⟨p, q⟩) \in ℝ^{*}$
72		psmetge0	$⊢ (D \in PsMet (X) \land p \in X \land q \in X) \to 0 \leq p D q$
73	57 60 61 72	syl3anc	$⊢ ((((D \in PsMet (X) \land a \in ℝ^{+}) \land p \in X \land q \in X) \land r \in X) \land (p D^{-1} [[0, \frac{a}{2})] r \land r D^{-1} [[0, \frac{a}{2})] q)) \to 0 \leq p D q$
74		df-ov	$⊢ p D q = D (⟨p, q⟩)$
75	73 74	breqtrdi	$⊢ ((((D \in PsMet (X) \land a \in ℝ^{+}) \land p \in X \land q \in X) \land r \in X) \land (p D^{-1} [[0, \frac{a}{2})] r \land r D^{-1} [[0, \frac{a}{2})] q)) \to 0 \leq D (⟨p, q⟩)$
76	74 71	eqeltrid	$⊢ ((((D \in PsMet (X) \land a \in ℝ^{+}) \land p \in X \land q \in X) \land r \in X) \land (p D^{-1} [[0, \frac{a}{2})] r \land r D^{-1} [[0, \frac{a}{2})] q)) \to p D q \in ℝ^{*}$
77		0red	$⊢ ((((D \in PsMet (X) \land a \in ℝ^{+}) \land p \in X \land q \in X) \land r \in X) \land (p D^{-1} [[0, \frac{a}{2})] r \land r D^{-1} [[0, \frac{a}{2})] q)) \to 0 \in ℝ$
78	68	rpred	$⊢ ((((D \in PsMet (X) \land a \in ℝ^{+}) \land p \in X \land q \in X) \land r \in X) \land (p D^{-1} [[0, \frac{a}{2})] r \land r D^{-1} [[0, \frac{a}{2})] q)) \to a \in ℝ$
79	78	rehalfcld	$⊢ ((((D \in PsMet (X) \land a \in ℝ^{+}) \land p \in X \land q \in X) \land r \in X) \land (p D^{-1} [[0, \frac{a}{2})] r \land r D^{-1} [[0, \frac{a}{2})] q)) \to \frac{a}{2} \in ℝ$
80	79	rexrd	$⊢ ((((D \in PsMet (X) \land a \in ℝ^{+}) \land p \in X \land q \in X) \land r \in X) \land (p D^{-1} [[0, \frac{a}{2})] r \land r D^{-1} [[0, \frac{a}{2})] q)) \to \frac{a}{2} \in ℝ^{*}$
81		df-ov	$⊢ p D r = D (⟨p, r⟩)$
82		simplr	$⊢ ((((D \in PsMet (X) \land a \in ℝ^{+}) \land p \in X \land q \in X) \land r \in X) \land (p D^{-1} [[0, \frac{a}{2})] r \land r D^{-1} [[0, \frac{a}{2})] q)) \to r \in X$
83	60 82	opelxpd	$⊢ ((((D \in PsMet (X) \land a \in ℝ^{+}) \land p \in X \land q \in X) \land r \in X) \land (p D^{-1} [[0, \frac{a}{2})] r \land r D^{-1} [[0, \frac{a}{2})] q)) \to ⟨p, r⟩ \in (X \times X)$
84	83 64	eleqtrrd	$⊢ ((((D \in PsMet (X) \land a \in ℝ^{+}) \land p \in X \land q \in X) \land r \in X) \land (p D^{-1} [[0, \frac{a}{2})] r \land r D^{-1} [[0, \frac{a}{2})] q)) \to ⟨p, r⟩ \in dom D$
85		simprl	$⊢ ((((D \in PsMet (X) \land a \in ℝ^{+}) \land p \in X \land q \in X) \land r \in X) \land (p D^{-1} [[0, \frac{a}{2})] r \land r D^{-1} [[0, \frac{a}{2})] q)) \to p D^{-1} [[0, \frac{a}{2})] r$
86		df-br	$⊢ p D^{-1} [[0, \frac{a}{2})] r \leftrightarrow ⟨p, r⟩ \in D^{-1} [[0, \frac{a}{2})]$
87	85 86	sylib	$⊢ ((((D \in PsMet (X) \land a \in ℝ^{+}) \land p \in X \land q \in X) \land r \in X) \land (p D^{-1} [[0, \frac{a}{2})] r \land r D^{-1} [[0, \frac{a}{2})] q)) \to ⟨p, r⟩ \in D^{-1} [[0, \frac{a}{2})]$
88		fvimacnv	$⊢ (Fun D \land ⟨p, r⟩ \in dom D) \to (D (⟨p, r⟩) \in [0, \frac{a}{2}) \leftrightarrow ⟨p, r⟩ \in D^{-1} [[0, \frac{a}{2})])$
89	88	biimpar	$⊢ ((Fun D \land ⟨p, r⟩ \in dom D) \land ⟨p, r⟩ \in D^{-1} [[0, \frac{a}{2})]) \to D (⟨p, r⟩) \in [0, \frac{a}{2})$
90	59 84 87 89	syl21anc	$⊢ ((((D \in PsMet (X) \land a \in ℝ^{+}) \land p \in X \land q \in X) \land r \in X) \land (p D^{-1} [[0, \frac{a}{2})] r \land r D^{-1} [[0, \frac{a}{2})] q)) \to D (⟨p, r⟩) \in [0, \frac{a}{2})$
91	81 90	eqeltrid	$⊢ ((((D \in PsMet (X) \land a \in ℝ^{+}) \land p \in X \land q \in X) \land r \in X) \land (p D^{-1} [[0, \frac{a}{2})] r \land r D^{-1} [[0, \frac{a}{2})] q)) \to p D r \in [0, \frac{a}{2})$
92		elico2	$⊢ (0 \in ℝ \land \frac{a}{2} \in ℝ^{*}) \to (p D r \in [0, \frac{a}{2}) \leftrightarrow (p D r \in ℝ \land 0 \leq p D r \land p D r < \frac{a}{2}))$
93	92	biimpa	$⊢ ((0 \in ℝ \land \frac{a}{2} \in ℝ^{*}) \land p D r \in [0, \frac{a}{2})) \to (p D r \in ℝ \land 0 \leq p D r \land p D r < \frac{a}{2})$
94	93	simp1d	$⊢ ((0 \in ℝ \land \frac{a}{2} \in ℝ^{*}) \land p D r \in [0, \frac{a}{2})) \to p D r \in ℝ$
95	77 80 91 94	syl21anc	$⊢ ((((D \in PsMet (X) \land a \in ℝ^{+}) \land p \in X \land q \in X) \land r \in X) \land (p D^{-1} [[0, \frac{a}{2})] r \land r D^{-1} [[0, \frac{a}{2})] q)) \to p D r \in ℝ$
96		df-ov	$⊢ r D q = D (⟨r, q⟩)$
97	82 61	opelxpd	$⊢ ((((D \in PsMet (X) \land a \in ℝ^{+}) \land p \in X \land q \in X) \land r \in X) \land (p D^{-1} [[0, \frac{a}{2})] r \land r D^{-1} [[0, \frac{a}{2})] q)) \to ⟨r, q⟩ \in (X \times X)$
98	97 64	eleqtrrd	$⊢ ((((D \in PsMet (X) \land a \in ℝ^{+}) \land p \in X \land q \in X) \land r \in X) \land (p D^{-1} [[0, \frac{a}{2})] r \land r D^{-1} [[0, \frac{a}{2})] q)) \to ⟨r, q⟩ \in dom D$
99		simprr	$⊢ ((((D \in PsMet (X) \land a \in ℝ^{+}) \land p \in X \land q \in X) \land r \in X) \land (p D^{-1} [[0, \frac{a}{2})] r \land r D^{-1} [[0, \frac{a}{2})] q)) \to r D^{-1} [[0, \frac{a}{2})] q$
100		df-br	$⊢ r D^{-1} [[0, \frac{a}{2})] q \leftrightarrow ⟨r, q⟩ \in D^{-1} [[0, \frac{a}{2})]$
101	99 100	sylib	$⊢ ((((D \in PsMet (X) \land a \in ℝ^{+}) \land p \in X \land q \in X) \land r \in X) \land (p D^{-1} [[0, \frac{a}{2})] r \land r D^{-1} [[0, \frac{a}{2})] q)) \to ⟨r, q⟩ \in D^{-1} [[0, \frac{a}{2})]$
102		fvimacnv	$⊢ (Fun D \land ⟨r, q⟩ \in dom D) \to (D (⟨r, q⟩) \in [0, \frac{a}{2}) \leftrightarrow ⟨r, q⟩ \in D^{-1} [[0, \frac{a}{2})])$
103	102	biimpar	$⊢ ((Fun D \land ⟨r, q⟩ \in dom D) \land ⟨r, q⟩ \in D^{-1} [[0, \frac{a}{2})]) \to D (⟨r, q⟩) \in [0, \frac{a}{2})$
104	59 98 101 103	syl21anc	$⊢ ((((D \in PsMet (X) \land a \in ℝ^{+}) \land p \in X \land q \in X) \land r \in X) \land (p D^{-1} [[0, \frac{a}{2})] r \land r D^{-1} [[0, \frac{a}{2})] q)) \to D (⟨r, q⟩) \in [0, \frac{a}{2})$
105	96 104	eqeltrid	$⊢ ((((D \in PsMet (X) \land a \in ℝ^{+}) \land p \in X \land q \in X) \land r \in X) \land (p D^{-1} [[0, \frac{a}{2})] r \land r D^{-1} [[0, \frac{a}{2})] q)) \to r D q \in [0, \frac{a}{2})$
106		elico2	$⊢ (0 \in ℝ \land \frac{a}{2} \in ℝ^{*}) \to (r D q \in [0, \frac{a}{2}) \leftrightarrow (r D q \in ℝ \land 0 \leq r D q \land r D q < \frac{a}{2}))$
107	106	biimpa	$⊢ ((0 \in ℝ \land \frac{a}{2} \in ℝ^{*}) \land r D q \in [0, \frac{a}{2})) \to (r D q \in ℝ \land 0 \leq r D q \land r D q < \frac{a}{2})$
108	107	simp1d	$⊢ ((0 \in ℝ \land \frac{a}{2} \in ℝ^{*}) \land r D q \in [0, \frac{a}{2})) \to r D q \in ℝ$
109	77 80 105 108	syl21anc	$⊢ ((((D \in PsMet (X) \land a \in ℝ^{+}) \land p \in X \land q \in X) \land r \in X) \land (p D^{-1} [[0, \frac{a}{2})] r \land r D^{-1} [[0, \frac{a}{2})] q)) \to r D q \in ℝ$
110	95 109	rexaddd	$⊢ ((((D \in PsMet (X) \land a \in ℝ^{+}) \land p \in X \land q \in X) \land r \in X) \land (p D^{-1} [[0, \frac{a}{2})] r \land r D^{-1} [[0, \frac{a}{2})] q)) \to (p D r) +_{𝑒} (r D q) = (p D r) + (r D q)$
111	95 109	readdcld	$⊢ ((((D \in PsMet (X) \land a \in ℝ^{+}) \land p \in X \land q \in X) \land r \in X) \land (p D^{-1} [[0, \frac{a}{2})] r \land r D^{-1} [[0, \frac{a}{2})] q)) \to (p D r) + (r D q) \in ℝ$
112	110 111	eqeltrd	$⊢ ((((D \in PsMet (X) \land a \in ℝ^{+}) \land p \in X \land q \in X) \land r \in X) \land (p D^{-1} [[0, \frac{a}{2})] r \land r D^{-1} [[0, \frac{a}{2})] q)) \to (p D r) +_{𝑒} (r D q) \in ℝ$
113	112	rexrd	$⊢ ((((D \in PsMet (X) \land a \in ℝ^{+}) \land p \in X \land q \in X) \land r \in X) \land (p D^{-1} [[0, \frac{a}{2})] r \land r D^{-1} [[0, \frac{a}{2})] q)) \to (p D r) +_{𝑒} (r D q) \in ℝ^{*}$
114		psmettri	$⊢ (D \in PsMet (X) \land (p \in X \land q \in X \land r \in X)) \to p D q \leq (p D r) +_{𝑒} (r D q)$
115	57 60 61 82 114	syl13anc	$⊢ ((((D \in PsMet (X) \land a \in ℝ^{+}) \land p \in X \land q \in X) \land r \in X) \land (p D^{-1} [[0, \frac{a}{2})] r \land r D^{-1} [[0, \frac{a}{2})] q)) \to p D q \leq (p D r) +_{𝑒} (r D q)$
116	93	simp3d	$⊢ ((0 \in ℝ \land \frac{a}{2} \in ℝ^{*}) \land p D r \in [0, \frac{a}{2})) \to p D r < \frac{a}{2}$
117	77 80 91 116	syl21anc	$⊢ ((((D \in PsMet (X) \land a \in ℝ^{+}) \land p \in X \land q \in X) \land r \in X) \land (p D^{-1} [[0, \frac{a}{2})] r \land r D^{-1} [[0, \frac{a}{2})] q)) \to p D r < \frac{a}{2}$
118	107	simp3d	$⊢ ((0 \in ℝ \land \frac{a}{2} \in ℝ^{*}) \land r D q \in [0, \frac{a}{2})) \to r D q < \frac{a}{2}$
119	77 80 105 118	syl21anc	$⊢ ((((D \in PsMet (X) \land a \in ℝ^{+}) \land p \in X \land q \in X) \land r \in X) \land (p D^{-1} [[0, \frac{a}{2})] r \land r D^{-1} [[0, \frac{a}{2})] q)) \to r D q < \frac{a}{2}$
120	95 109 78 117 119	lt2halvesd	$⊢ ((((D \in PsMet (X) \land a \in ℝ^{+}) \land p \in X \land q \in X) \land r \in X) \land (p D^{-1} [[0, \frac{a}{2})] r \land r D^{-1} [[0, \frac{a}{2})] q)) \to (p D r) + (r D q) < a$
121	110 120	eqbrtrd	$⊢ ((((D \in PsMet (X) \land a \in ℝ^{+}) \land p \in X \land q \in X) \land r \in X) \land (p D^{-1} [[0, \frac{a}{2})] r \land r D^{-1} [[0, \frac{a}{2})] q)) \to (p D r) +_{𝑒} (r D q) < a$
122	76 113 69 115 121	xrlelttrd	$⊢ ((((D \in PsMet (X) \land a \in ℝ^{+}) \land p \in X \land q \in X) \land r \in X) \land (p D^{-1} [[0, \frac{a}{2})] r \land r D^{-1} [[0, \frac{a}{2})] q)) \to p D q < a$
123	74 122	eqbrtrrid	$⊢ ((((D \in PsMet (X) \land a \in ℝ^{+}) \land p \in X \land q \in X) \land r \in X) \land (p D^{-1} [[0, \frac{a}{2})] r \land r D^{-1} [[0, \frac{a}{2})] q)) \to D (⟨p, q⟩) < a$
124	67 69 71 75 123	elicod	$⊢ ((((D \in PsMet (X) \land a \in ℝ^{+}) \land p \in X \land q \in X) \land r \in X) \land (p D^{-1} [[0, \frac{a}{2})] r \land r D^{-1} [[0, \frac{a}{2})] q)) \to D (⟨p, q⟩) \in [0, a)$
125		fvimacnv	$⊢ (Fun D \land ⟨p, q⟩ \in dom D) \to (D (⟨p, q⟩) \in [0, a) \leftrightarrow ⟨p, q⟩ \in D^{-1} [[0, a)])$
126	125	biimpa	$⊢ ((Fun D \land ⟨p, q⟩ \in dom D) \land D (⟨p, q⟩) \in [0, a)) \to ⟨p, q⟩ \in D^{-1} [[0, a)]$
127		df-br	$⊢ p D^{-1} [[0, a)] q \leftrightarrow ⟨p, q⟩ \in D^{-1} [[0, a)]$
128	126 127	sylibr	$⊢ ((Fun D \land ⟨p, q⟩ \in dom D) \land D (⟨p, q⟩) \in [0, a)) \to p D^{-1} [[0, a)] q$
129	59 65 124 128	syl21anc	$⊢ ((((D \in PsMet (X) \land a \in ℝ^{+}) \land p \in X \land q \in X) \land r \in X) \land (p D^{-1} [[0, \frac{a}{2})] r \land r D^{-1} [[0, \frac{a}{2})] q)) \to p D^{-1} [[0, a)] q$
130	51 52 53 54 129	syl22anc	$⊢ ((((((((X \neq \emptyset \land D \in PsMet (X)) \land A \in F) \land a \in ℝ^{+}) \land A = D^{-1} [[0, a)]) \land p \in X \land q \in X) \land ⟨p, q⟩ \in (D^{-1} [[0, \frac{a}{2})] \circ D^{-1} [[0, \frac{a}{2})])) \land r \in X) \land (p D^{-1} [[0, \frac{a}{2})] r \land r D^{-1} [[0, \frac{a}{2})] q)) \to p D^{-1} [[0, a)] q$
131	45	simprd	$⊢ ((((((((X \neq \emptyset \land D \in PsMet (X)) \land A \in F) \land a \in ℝ^{+}) \land A = D^{-1} [[0, a)]) \land p \in X \land q \in X) \land ⟨p, q⟩ \in (D^{-1} [[0, \frac{a}{2})] \circ D^{-1} [[0, \frac{a}{2})])) \land r \in X) \land (p D^{-1} [[0, \frac{a}{2})] r \land r D^{-1} [[0, \frac{a}{2})] q)) \to A = D^{-1} [[0, a)]$
132	131	breqd	$⊢ ((((((((X \neq \emptyset \land D \in PsMet (X)) \land A \in F) \land a \in ℝ^{+}) \land A = D^{-1} [[0, a)]) \land p \in X \land q \in X) \land ⟨p, q⟩ \in (D^{-1} [[0, \frac{a}{2})] \circ D^{-1} [[0, \frac{a}{2})])) \land r \in X) \land (p D^{-1} [[0, \frac{a}{2})] r \land r D^{-1} [[0, \frac{a}{2})] q)) \to (p A q \leftrightarrow p D^{-1} [[0, a)] q)$
133	130 132	mpbird	$⊢ ((((((((X \neq \emptyset \land D \in PsMet (X)) \land A \in F) \land a \in ℝ^{+}) \land A = D^{-1} [[0, a)]) \land p \in X \land q \in X) \land ⟨p, q⟩ \in (D^{-1} [[0, \frac{a}{2})] \circ D^{-1} [[0, \frac{a}{2})])) \land r \in X) \land (p D^{-1} [[0, \frac{a}{2})] r \land r D^{-1} [[0, \frac{a}{2})] q)) \to p A q$
134		simpr	$⊢ ((((((X \neq \emptyset \land D \in PsMet (X)) \land A \in F) \land a \in ℝ^{+}) \land A = D^{-1} [[0, a)]) \land p \in X \land q \in X) \land ⟨p, q⟩ \in (D^{-1} [[0, \frac{a}{2})] \circ D^{-1} [[0, \frac{a}{2})])) \to ⟨p, q⟩ \in (D^{-1} [[0, \frac{a}{2})] \circ D^{-1} [[0, \frac{a}{2})])$
135		df-br	$⊢ p (D^{-1} [[0, \frac{a}{2})] \circ D^{-1} [[0, \frac{a}{2})]) q \leftrightarrow ⟨p, q⟩ \in (D^{-1} [[0, \frac{a}{2})] \circ D^{-1} [[0, \frac{a}{2})])$
136	134 135	sylibr	$⊢ ((((((X \neq \emptyset \land D \in PsMet (X)) \land A \in F) \land a \in ℝ^{+}) \land A = D^{-1} [[0, a)]) \land p \in X \land q \in X) \land ⟨p, q⟩ \in (D^{-1} [[0, \frac{a}{2})] \circ D^{-1} [[0, \frac{a}{2})])) \to p (D^{-1} [[0, \frac{a}{2})] \circ D^{-1} [[0, \frac{a}{2})]) q$
137		vex	$⊢ p \in V$
138		vex	$⊢ q \in V$
139	137 138	brco	$⊢ p (D^{-1} [[0, \frac{a}{2})] \circ D^{-1} [[0, \frac{a}{2})]) q \leftrightarrow \exists r (p D^{-1} [[0, \frac{a}{2})] r \land r D^{-1} [[0, \frac{a}{2})] q)$
140	136 139	sylib	$⊢ ((((((X \neq \emptyset \land D \in PsMet (X)) \land A \in F) \land a \in ℝ^{+}) \land A = D^{-1} [[0, a)]) \land p \in X \land q \in X) \land ⟨p, q⟩ \in (D^{-1} [[0, \frac{a}{2})] \circ D^{-1} [[0, \frac{a}{2})])) \to \exists r (p D^{-1} [[0, \frac{a}{2})] r \land r D^{-1} [[0, \frac{a}{2})] q)$
141	23	adantl	$⊢ (X \neq \emptyset \land D \in PsMet (X)) \to D^{-1} [[0, \frac{a}{2})] \subseteq X \times X$
142	141 25	syl	$⊢ (X \neq \emptyset \land D \in PsMet (X)) \to ran D^{-1} [[0, \frac{a}{2})] \subseteq ran (X \times X)$
143	31	adantr	$⊢ (X \neq \emptyset \land D \in PsMet (X)) \to ran (X \times X) = X$
144	142 143	sseqtrd	$⊢ (X \neq \emptyset \land D \in PsMet (X)) \to ran D^{-1} [[0, \frac{a}{2})] \subseteq X$
145	144	adantr	$⊢ ((X \neq \emptyset \land D \in PsMet (X)) \land p D^{-1} [[0, \frac{a}{2})] r) \to ran D^{-1} [[0, \frac{a}{2})] \subseteq X$
146		vex	$⊢ r \in V$
147	137 146	brelrn	$⊢ p D^{-1} [[0, \frac{a}{2})] r \to r \in ran D^{-1} [[0, \frac{a}{2})]$
148	147	adantl	$⊢ ((X \neq \emptyset \land D \in PsMet (X)) \land p D^{-1} [[0, \frac{a}{2})] r) \to r \in ran D^{-1} [[0, \frac{a}{2})]$
149	145 148	sseldd	$⊢ ((X \neq \emptyset \land D \in PsMet (X)) \land p D^{-1} [[0, \frac{a}{2})] r) \to r \in X$
150	149	adantrr	$⊢ ((X \neq \emptyset \land D \in PsMet (X)) \land (p D^{-1} [[0, \frac{a}{2})] r \land r D^{-1} [[0, \frac{a}{2})] q)) \to r \in X$
151	150	ex	$⊢ (X \neq \emptyset \land D \in PsMet (X)) \to ((p D^{-1} [[0, \frac{a}{2})] r \land r D^{-1} [[0, \frac{a}{2})] q) \to r \in X)$
152	151	ancrd	$⊢ (X \neq \emptyset \land D \in PsMet (X)) \to ((p D^{-1} [[0, \frac{a}{2})] r \land r D^{-1} [[0, \frac{a}{2})] q) \to (r \in X \land (p D^{-1} [[0, \frac{a}{2})] r \land r D^{-1} [[0, \frac{a}{2})] q)))$
153	152	eximdv	$⊢ (X \neq \emptyset \land D \in PsMet (X)) \to (\exists r (p D^{-1} [[0, \frac{a}{2})] r \land r D^{-1} [[0, \frac{a}{2})] q) \to \exists r (r \in X \land (p D^{-1} [[0, \frac{a}{2})] r \land r D^{-1} [[0, \frac{a}{2})] q)))$
154	153	ad3antrrr	$⊢ ((((X \neq \emptyset \land D \in PsMet (X)) \land A \in F) \land a \in ℝ^{+}) \land A = D^{-1} [[0, a)]) \to (\exists r (p D^{-1} [[0, \frac{a}{2})] r \land r D^{-1} [[0, \frac{a}{2})] q) \to \exists r (r \in X \land (p D^{-1} [[0, \frac{a}{2})] r \land r D^{-1} [[0, \frac{a}{2})] q)))$
155	154	3ad2ant1	$⊢ (((((X \neq \emptyset \land D \in PsMet (X)) \land A \in F) \land a \in ℝ^{+}) \land A = D^{-1} [[0, a)]) \land p \in X \land q \in X) \to (\exists r (p D^{-1} [[0, \frac{a}{2})] r \land r D^{-1} [[0, \frac{a}{2})] q) \to \exists r (r \in X \land (p D^{-1} [[0, \frac{a}{2})] r \land r D^{-1} [[0, \frac{a}{2})] q)))$
156	155	adantr	$⊢ ((((((X \neq \emptyset \land D \in PsMet (X)) \land A \in F) \land a \in ℝ^{+}) \land A = D^{-1} [[0, a)]) \land p \in X \land q \in X) \land ⟨p, q⟩ \in (D^{-1} [[0, \frac{a}{2})] \circ D^{-1} [[0, \frac{a}{2})])) \to (\exists r (p D^{-1} [[0, \frac{a}{2})] r \land r D^{-1} [[0, \frac{a}{2})] q) \to \exists r (r \in X \land (p D^{-1} [[0, \frac{a}{2})] r \land r D^{-1} [[0, \frac{a}{2})] q)))$
157	140 156	mpd	$⊢ ((((((X \neq \emptyset \land D \in PsMet (X)) \land A \in F) \land a \in ℝ^{+}) \land A = D^{-1} [[0, a)]) \land p \in X \land q \in X) \land ⟨p, q⟩ \in (D^{-1} [[0, \frac{a}{2})] \circ D^{-1} [[0, \frac{a}{2})])) \to \exists r (r \in X \land (p D^{-1} [[0, \frac{a}{2})] r \land r D^{-1} [[0, \frac{a}{2})] q))$
158		df-rex	$⊢ \exists r \in X (p D^{-1} [[0, \frac{a}{2})] r \land r D^{-1} [[0, \frac{a}{2})] q) \leftrightarrow \exists r (r \in X \land (p D^{-1} [[0, \frac{a}{2})] r \land r D^{-1} [[0, \frac{a}{2})] q))$
159	157 158	sylibr	$⊢ ((((((X \neq \emptyset \land D \in PsMet (X)) \land A \in F) \land a \in ℝ^{+}) \land A = D^{-1} [[0, a)]) \land p \in X \land q \in X) \land ⟨p, q⟩ \in (D^{-1} [[0, \frac{a}{2})] \circ D^{-1} [[0, \frac{a}{2})])) \to \exists r \in X (p D^{-1} [[0, \frac{a}{2})] r \land r D^{-1} [[0, \frac{a}{2})] q)$
160	133 159	r19.29a	$⊢ ((((((X \neq \emptyset \land D \in PsMet (X)) \land A \in F) \land a \in ℝ^{+}) \land A = D^{-1} [[0, a)]) \land p \in X \land q \in X) \land ⟨p, q⟩ \in (D^{-1} [[0, \frac{a}{2})] \circ D^{-1} [[0, \frac{a}{2})])) \to p A q$
161		df-br	$⊢ p A q \leftrightarrow ⟨p, q⟩ \in A$
162	160 161	sylib	$⊢ ((((((X \neq \emptyset \land D \in PsMet (X)) \land A \in F) \land a \in ℝ^{+}) \land A = D^{-1} [[0, a)]) \land p \in X \land q \in X) \land ⟨p, q⟩ \in (D^{-1} [[0, \frac{a}{2})] \circ D^{-1} [[0, \frac{a}{2})])) \to ⟨p, q⟩ \in A$
163	40 41 42 43 162	syl31anc	$⊢ ((((((X \neq \emptyset \land D \in PsMet (X)) \land A \in F) \land a \in ℝ^{+}) \land A = D^{-1} [[0, a)]) \land ⟨p, q⟩ \in (D^{-1} [[0, \frac{a}{2})] \circ D^{-1} [[0, \frac{a}{2})])) \land (p \in X \land q \in X)) \to ⟨p, q⟩ \in A$
164	39 163	mpdan	$⊢ (((((X \neq \emptyset \land D \in PsMet (X)) \land A \in F) \land a \in ℝ^{+}) \land A = D^{-1} [[0, a)]) \land ⟨p, q⟩ \in (D^{-1} [[0, \frac{a}{2})] \circ D^{-1} [[0, \frac{a}{2})])) \to ⟨p, q⟩ \in A$
165	164	ex	$⊢ ((((X \neq \emptyset \land D \in PsMet (X)) \land A \in F) \land a \in ℝ^{+}) \land A = D^{-1} [[0, a)]) \to (⟨p, q⟩ \in (D^{-1} [[0, \frac{a}{2})] \circ D^{-1} [[0, \frac{a}{2})]) \to ⟨p, q⟩ \in A)$
166	19 165	relssdv	$⊢ ((((X \neq \emptyset \land D \in PsMet (X)) \land A \in F) \land a \in ℝ^{+}) \land A = D^{-1} [[0, a)]) \to D^{-1} [[0, \frac{a}{2})] \circ D^{-1} [[0, \frac{a}{2})] \subseteq A$
167		id	$⊢ v = D^{-1} [[0, \frac{a}{2})] \to v = D^{-1} [[0, \frac{a}{2})]$
168	167 167	coeq12d	$⊢ v = D^{-1} [[0, \frac{a}{2})] \to v \circ v = D^{-1} [[0, \frac{a}{2})] \circ D^{-1} [[0, \frac{a}{2})]$
169	168	sseq1d	$⊢ v = D^{-1} [[0, \frac{a}{2})] \to (v \circ v \subseteq A \leftrightarrow D^{-1} [[0, \frac{a}{2})] \circ D^{-1} [[0, \frac{a}{2})] \subseteq A)$
170	169	rspcev	$⊢ (D^{-1} [[0, \frac{a}{2})] \in F \land D^{-1} [[0, \frac{a}{2})] \circ D^{-1} [[0, \frac{a}{2})] \subseteq A) \to \exists v \in F v \circ v \subseteq A$
171	17 166 170	syl2anc	$⊢ ((((X \neq \emptyset \land D \in PsMet (X)) \land A \in F) \land a \in ℝ^{+}) \land A = D^{-1} [[0, a)]) \to \exists v \in F v \circ v \subseteq A$
172	1	metustel	$⊢ D \in PsMet (X) \to (A \in F \leftrightarrow \exists a \in ℝ^{+} A = D^{-1} [[0, a)])$
173	172	adantl	$⊢ (X \neq \emptyset \land D \in PsMet (X)) \to (A \in F \leftrightarrow \exists a \in ℝ^{+} A = D^{-1} [[0, a)])$
174	173	biimpa	$⊢ ((X \neq \emptyset \land D \in PsMet (X)) \land A \in F) \to \exists a \in ℝ^{+} A = D^{-1} [[0, a)]$
175	171 174	r19.29a	$⊢ ((X \neq \emptyset \land D \in PsMet (X)) \land A \in F) \to \exists v \in F v \circ v \subseteq A$

Metamath Proof Explorer

Theorem metustexhalf

Proof