restmetu

Description: The uniform structure generated by the restriction of a metric is its trace. (Contributed by Thierry Arnoux, 18-Dec-2017)

		Ref	Expression
	Assertion	restmetu	$⊢ (A \neq \emptyset \land D \in PsMet (X) \land A \subseteq X) \to metUnif (D) ↾_{𝑡} (A \times A) = metUnif ({D ↾}_{(A \times A)})$

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (A \neq \emptyset \land D \in PsMet (X) \land A \subseteq X) \to A \neq \emptyset$
2		psmetres2	$⊢ (D \in PsMet (X) \land A \subseteq X) \to {D ↾}_{(A \times A)} \in PsMet (A)$
3	2	3adant1	$⊢ (A \neq \emptyset \land D \in PsMet (X) \land A \subseteq X) \to {D ↾}_{(A \times A)} \in PsMet (A)$
4		oveq2	$⊢ a = b \to [0, a) = [0, b)$
5	4	imaeq2d	$⊢ a = b \to {({D ↾}_{(A \times A)})}^{-1} [[0, a)] = {({D ↾}_{(A \times A)})}^{-1} [[0, b)]$
6	5	cbvmptv	$⊢ (a \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, a)]) = (b \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, b)])$
7	6	rneqi	$⊢ ran (a \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, a)]) = ran (b \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, b)])$
8	7	metustfbas	$⊢ (A \neq \emptyset \land {D ↾}_{(A \times A)} \in PsMet (A)) \to ran (a \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, a)]) \in fBas (A \times A)$
9	1 3 8	syl2anc	$⊢ (A \neq \emptyset \land D \in PsMet (X) \land A \subseteq X) \to ran (a \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, a)]) \in fBas (A \times A)$
10		fgval	$⊢ ran (a \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, a)]) \in fBas (A \times A) \to (A \times A) filGen ran (a \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, a)]) = \{v \in 𝒫 (A \times A) \| ran (a \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, a)]) \cap 𝒫 v \neq \emptyset\}$
11	9 10	syl	$⊢ (A \neq \emptyset \land D \in PsMet (X) \land A \subseteq X) \to (A \times A) filGen ran (a \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, a)]) = \{v \in 𝒫 (A \times A) \| ran (a \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, a)]) \cap 𝒫 v \neq \emptyset\}$
12		metuval	$⊢ {D ↾}_{(A \times A)} \in PsMet (A) \to metUnif ({D ↾}_{(A \times A)}) = (A \times A) filGen ran (a \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, a)])$
13	3 12	syl	$⊢ (A \neq \emptyset \land D \in PsMet (X) \land A \subseteq X) \to metUnif ({D ↾}_{(A \times A)}) = (A \times A) filGen ran (a \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, a)])$
14		fvex	$⊢ metUnif (D) \in V$
15	3	elfvexd	$⊢ (A \neq \emptyset \land D \in PsMet (X) \land A \subseteq X) \to A \in V$
16	15 15	xpexd	$⊢ (A \neq \emptyset \land D \in PsMet (X) \land A \subseteq X) \to A \times A \in V$
17		restval	$⊢ (metUnif (D) \in V \land A \times A \in V) \to metUnif (D) ↾_{𝑡} (A \times A) = ran (v \in metUnif (D) ⟼ v \cap (A \times A))$
18	14 16 17	sylancr	$⊢ (A \neq \emptyset \land D \in PsMet (X) \land A \subseteq X) \to metUnif (D) ↾_{𝑡} (A \times A) = ran (v \in metUnif (D) ⟼ v \cap (A \times A))$
19		inss2	$⊢ v \cap (A \times A) \subseteq A \times A$
20		sseq1	$⊢ u = v \cap (A \times A) \to (u \subseteq A \times A \leftrightarrow v \cap (A \times A) \subseteq A \times A)$
21	19 20	mpbiri	$⊢ u = v \cap (A \times A) \to u \subseteq A \times A$
22		vex	$⊢ u \in V$
23	22	elpw	$⊢ u \in 𝒫 (A \times A) \leftrightarrow u \subseteq A \times A$
24	21 23	sylibr	$⊢ u = v \cap (A \times A) \to u \in 𝒫 (A \times A)$
25	24	rexlimivw	$⊢ \exists v \in metUnif (D) u = v \cap (A \times A) \to u \in 𝒫 (A \times A)$
26	25	adantl	$⊢ ((A \neq \emptyset \land D \in PsMet (X) \land A \subseteq X) \land \exists v \in metUnif (D) u = v \cap (A \times A)) \to u \in 𝒫 (A \times A)$
27		nfv	$⊢ Ⅎ a (((A \neq \emptyset \land D \in PsMet (X) \land A \subseteq X) \land v \in metUnif (D)) \land u = v \cap (A \times A))$
28		nfmpt1	$⊢ \underline{Ⅎ} a (a \in ℝ^{+} ⟼ D^{-1} [[0, a)])$
29	28	nfrn	$⊢ \underline{Ⅎ} a ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)])$
30	29	nfcri	$⊢ Ⅎ a w \in ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)])$
31	27 30	nfan	$⊢ Ⅎ a ((((A \neq \emptyset \land D \in PsMet (X) \land A \subseteq X) \land v \in metUnif (D)) \land u = v \cap (A \times A)) \land w \in ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)]))$
32		nfv	$⊢ Ⅎ a w \subseteq v$
33	31 32	nfan	$⊢ Ⅎ a (((((A \neq \emptyset \land D \in PsMet (X) \land A \subseteq X) \land v \in metUnif (D)) \land u = v \cap (A \times A)) \land w \in ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)])) \land w \subseteq v)$
34		nfmpt1	$⊢ \underline{Ⅎ} a (a \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, a)])$
35	34	nfrn	$⊢ \underline{Ⅎ} a ran (a \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, a)])$
36		nfcv	$⊢ \underline{Ⅎ} a 𝒫 u$
37	35 36	nfin	$⊢ \underline{Ⅎ} a (ran (a \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, a)]) \cap 𝒫 u)$
38		nfcv	$⊢ \underline{Ⅎ} a \emptyset$
39	37 38	nfne	$⊢ Ⅎ a ran (a \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, a)]) \cap 𝒫 u \neq \emptyset$
40		simplr	$⊢ (((((((A \neq \emptyset \land D \in PsMet (X) \land A \subseteq X) \land v \in metUnif (D)) \land u = v \cap (A \times A)) \land w \in ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)])) \land w \subseteq v) \land a \in ℝ^{+}) \land w = D^{-1} [[0, a)]) \to a \in ℝ^{+}$
41		ineq1	$⊢ w = D^{-1} [[0, a)] \to w \cap (A \times A) = D^{-1} [[0, a)] \cap (A \times A)$
42	41	adantl	$⊢ (((((((A \neq \emptyset \land D \in PsMet (X) \land A \subseteq X) \land v \in metUnif (D)) \land u = v \cap (A \times A)) \land w \in ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)])) \land w \subseteq v) \land a \in ℝ^{+}) \land w = D^{-1} [[0, a)]) \to w \cap (A \times A) = D^{-1} [[0, a)] \cap (A \times A)$
43		simp2	$⊢ (A \neq \emptyset \land D \in PsMet (X) \land A \subseteq X) \to D \in PsMet (X)$
44		psmetf	$⊢ D \in PsMet (X) \to D : X \times X ⟶ ℝ^{*}$
45		ffun	$⊢ D : X \times X ⟶ ℝ^{*} \to Fun D$
46		respreima	$⊢ Fun D \to {({D ↾}_{(A \times A)})}^{-1} [[0, a)] = D^{-1} [[0, a)] \cap (A \times A)$
47	43 44 45 46	4syl	$⊢ (A \neq \emptyset \land D \in PsMet (X) \land A \subseteq X) \to {({D ↾}_{(A \times A)})}^{-1} [[0, a)] = D^{-1} [[0, a)] \cap (A \times A)$
48	47	ad6antr	$⊢ (((((((A \neq \emptyset \land D \in PsMet (X) \land A \subseteq X) \land v \in metUnif (D)) \land u = v \cap (A \times A)) \land w \in ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)])) \land w \subseteq v) \land a \in ℝ^{+}) \land w = D^{-1} [[0, a)]) \to {({D ↾}_{(A \times A)})}^{-1} [[0, a)] = D^{-1} [[0, a)] \cap (A \times A)$
49	42 48	eqtr4d	$⊢ (((((((A \neq \emptyset \land D \in PsMet (X) \land A \subseteq X) \land v \in metUnif (D)) \land u = v \cap (A \times A)) \land w \in ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)])) \land w \subseteq v) \land a \in ℝ^{+}) \land w = D^{-1} [[0, a)]) \to w \cap (A \times A) = {({D ↾}_{(A \times A)})}^{-1} [[0, a)]$
50		rspe	$⊢ (a \in ℝ^{+} \land w \cap (A \times A) = {({D ↾}_{(A \times A)})}^{-1} [[0, a)]) \to \exists a \in ℝ^{+} w \cap (A \times A) = {({D ↾}_{(A \times A)})}^{-1} [[0, a)]$
51	40 49 50	syl2anc	$⊢ (((((((A \neq \emptyset \land D \in PsMet (X) \land A \subseteq X) \land v \in metUnif (D)) \land u = v \cap (A \times A)) \land w \in ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)])) \land w \subseteq v) \land a \in ℝ^{+}) \land w = D^{-1} [[0, a)]) \to \exists a \in ℝ^{+} w \cap (A \times A) = {({D ↾}_{(A \times A)})}^{-1} [[0, a)]$
52		vex	$⊢ w \in V$
53	52	inex1	$⊢ w \cap (A \times A) \in V$
54		eqid	$⊢ (a \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, a)]) = (a \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, a)])$
55	54	elrnmpt	$⊢ w \cap (A \times A) \in V \to (w \cap (A \times A) \in ran (a \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, a)]) \leftrightarrow \exists a \in ℝ^{+} w \cap (A \times A) = {({D ↾}_{(A \times A)})}^{-1} [[0, a)])$
56	53 55	ax-mp	$⊢ w \cap (A \times A) \in ran (a \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, a)]) \leftrightarrow \exists a \in ℝ^{+} w \cap (A \times A) = {({D ↾}_{(A \times A)})}^{-1} [[0, a)]$
57	51 56	sylibr	$⊢ (((((((A \neq \emptyset \land D \in PsMet (X) \land A \subseteq X) \land v \in metUnif (D)) \land u = v \cap (A \times A)) \land w \in ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)])) \land w \subseteq v) \land a \in ℝ^{+}) \land w = D^{-1} [[0, a)]) \to w \cap (A \times A) \in ran (a \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, a)])$
58		simpllr	$⊢ (((((((A \neq \emptyset \land D \in PsMet (X) \land A \subseteq X) \land v \in metUnif (D)) \land u = v \cap (A \times A)) \land w \in ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)])) \land w \subseteq v) \land a \in ℝ^{+}) \land w = D^{-1} [[0, a)]) \to w \subseteq v$
59		ssinss1	$⊢ w \subseteq v \to w \cap (A \times A) \subseteq v$
60	58 59	syl	$⊢ (((((((A \neq \emptyset \land D \in PsMet (X) \land A \subseteq X) \land v \in metUnif (D)) \land u = v \cap (A \times A)) \land w \in ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)])) \land w \subseteq v) \land a \in ℝ^{+}) \land w = D^{-1} [[0, a)]) \to w \cap (A \times A) \subseteq v$
61		inss2	$⊢ w \cap (A \times A) \subseteq A \times A$
62	61	a1i	$⊢ (((((((A \neq \emptyset \land D \in PsMet (X) \land A \subseteq X) \land v \in metUnif (D)) \land u = v \cap (A \times A)) \land w \in ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)])) \land w \subseteq v) \land a \in ℝ^{+}) \land w = D^{-1} [[0, a)]) \to w \cap (A \times A) \subseteq A \times A$
63		pweq	$⊢ u = v \cap (A \times A) \to 𝒫 u = 𝒫 (v \cap (A \times A))$
64	63	eleq2d	$⊢ u = v \cap (A \times A) \to (w \cap (A \times A) \in 𝒫 u \leftrightarrow w \cap (A \times A) \in 𝒫 (v \cap (A \times A)))$
65	53	elpw	$⊢ w \cap (A \times A) \in 𝒫 (v \cap (A \times A)) \leftrightarrow w \cap (A \times A) \subseteq v \cap (A \times A)$
66	64 65	bitrdi	$⊢ u = v \cap (A \times A) \to (w \cap (A \times A) \in 𝒫 u \leftrightarrow w \cap (A \times A) \subseteq v \cap (A \times A))$
67		ssin	$⊢ (w \cap (A \times A) \subseteq v \land w \cap (A \times A) \subseteq A \times A) \leftrightarrow w \cap (A \times A) \subseteq v \cap (A \times A)$
68	66 67	bitr4di	$⊢ u = v \cap (A \times A) \to (w \cap (A \times A) \in 𝒫 u \leftrightarrow (w \cap (A \times A) \subseteq v \land w \cap (A \times A) \subseteq A \times A))$
69	68	ad5antlr	$⊢ (((((((A \neq \emptyset \land D \in PsMet (X) \land A \subseteq X) \land v \in metUnif (D)) \land u = v \cap (A \times A)) \land w \in ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)])) \land w \subseteq v) \land a \in ℝ^{+}) \land w = D^{-1} [[0, a)]) \to (w \cap (A \times A) \in 𝒫 u \leftrightarrow (w \cap (A \times A) \subseteq v \land w \cap (A \times A) \subseteq A \times A))$
70	60 62 69	mpbir2and	$⊢ (((((((A \neq \emptyset \land D \in PsMet (X) \land A \subseteq X) \land v \in metUnif (D)) \land u = v \cap (A \times A)) \land w \in ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)])) \land w \subseteq v) \land a \in ℝ^{+}) \land w = D^{-1} [[0, a)]) \to w \cap (A \times A) \in 𝒫 u$
71		inelcm	$⊢ (w \cap (A \times A) \in ran (a \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, a)]) \land w \cap (A \times A) \in 𝒫 u) \to ran (a \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, a)]) \cap 𝒫 u \neq \emptyset$
72	57 70 71	syl2anc	$⊢ (((((((A \neq \emptyset \land D \in PsMet (X) \land A \subseteq X) \land v \in metUnif (D)) \land u = v \cap (A \times A)) \land w \in ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)])) \land w \subseteq v) \land a \in ℝ^{+}) \land w = D^{-1} [[0, a)]) \to ran (a \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, a)]) \cap 𝒫 u \neq \emptyset$
73		simplr	$⊢ (((((A \neq \emptyset \land D \in PsMet (X) \land A \subseteq X) \land v \in metUnif (D)) \land u = v \cap (A \times A)) \land w \in ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)])) \land w \subseteq v) \to w \in ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)])$
74		eqid	$⊢ (a \in ℝ^{+} ⟼ D^{-1} [[0, a)]) = (a \in ℝ^{+} ⟼ D^{-1} [[0, a)])$
75	74	elrnmpt	$⊢ w \in V \to (w \in ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)]) \leftrightarrow \exists a \in ℝ^{+} w = D^{-1} [[0, a)])$
76	75	elv	$⊢ w \in ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)]) \leftrightarrow \exists a \in ℝ^{+} w = D^{-1} [[0, a)]$
77	73 76	sylib	$⊢ (((((A \neq \emptyset \land D \in PsMet (X) \land A \subseteq X) \land v \in metUnif (D)) \land u = v \cap (A \times A)) \land w \in ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)])) \land w \subseteq v) \to \exists a \in ℝ^{+} w = D^{-1} [[0, a)]$
78	33 39 72 77	r19.29af2	$⊢ (((((A \neq \emptyset \land D \in PsMet (X) \land A \subseteq X) \land v \in metUnif (D)) \land u = v \cap (A \times A)) \land w \in ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)])) \land w \subseteq v) \to ran (a \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, a)]) \cap 𝒫 u \neq \emptyset$
79		ssn0	$⊢ (A \subseteq X \land A \neq \emptyset) \to X \neq \emptyset$
80	79	ancoms	$⊢ (A \neq \emptyset \land A \subseteq X) \to X \neq \emptyset$
81	80	3adant2	$⊢ (A \neq \emptyset \land D \in PsMet (X) \land A \subseteq X) \to X \neq \emptyset$
82		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))$
83	81 43 82	syl2anc	$⊢ (A \neq \emptyset \land D \in PsMet (X) \land A \subseteq 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))$
84	83	simplbda	$⊢ ((A \neq \emptyset \land D \in PsMet (X) \land A \subseteq X) \land v \in metUnif (D)) \to \exists w \in ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)]) w \subseteq v$
85	84	adantr	$⊢ (((A \neq \emptyset \land D \in PsMet (X) \land A \subseteq X) \land v \in metUnif (D)) \land u = v \cap (A \times A)) \to \exists w \in ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)]) w \subseteq v$
86	78 85	r19.29a	$⊢ (((A \neq \emptyset \land D \in PsMet (X) \land A \subseteq X) \land v \in metUnif (D)) \land u = v \cap (A \times A)) \to ran (a \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, a)]) \cap 𝒫 u \neq \emptyset$
87	86	r19.29an	$⊢ ((A \neq \emptyset \land D \in PsMet (X) \land A \subseteq X) \land \exists v \in metUnif (D) u = v \cap (A \times A)) \to ran (a \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, a)]) \cap 𝒫 u \neq \emptyset$
88	26 87	jca	$⊢ ((A \neq \emptyset \land D \in PsMet (X) \land A \subseteq X) \land \exists v \in metUnif (D) u = v \cap (A \times A)) \to (u \in 𝒫 (A \times A) \land ran (a \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, a)]) \cap 𝒫 u \neq \emptyset)$
89		simprl	$⊢ ((A \neq \emptyset \land D \in PsMet (X) \land A \subseteq X) \land (u \in 𝒫 (A \times A) \land ran (a \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, a)]) \cap 𝒫 u \neq \emptyset)) \to u \in 𝒫 (A \times A)$
90	89	elpwid	$⊢ ((A \neq \emptyset \land D \in PsMet (X) \land A \subseteq X) \land (u \in 𝒫 (A \times A) \land ran (a \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, a)]) \cap 𝒫 u \neq \emptyset)) \to u \subseteq A \times A$
91		simpl3	$⊢ ((A \neq \emptyset \land D \in PsMet (X) \land A \subseteq X) \land (u \in 𝒫 (A \times A) \land ran (a \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, a)]) \cap 𝒫 u \neq \emptyset)) \to A \subseteq X$
92		xpss12	$⊢ (A \subseteq X \land A \subseteq X) \to A \times A \subseteq X \times X$
93	91 91 92	syl2anc	$⊢ ((A \neq \emptyset \land D \in PsMet (X) \land A \subseteq X) \land (u \in 𝒫 (A \times A) \land ran (a \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, a)]) \cap 𝒫 u \neq \emptyset)) \to A \times A \subseteq X \times X$
94	90 93	sstrd	$⊢ ((A \neq \emptyset \land D \in PsMet (X) \land A \subseteq X) \land (u \in 𝒫 (A \times A) \land ran (a \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, a)]) \cap 𝒫 u \neq \emptyset)) \to u \subseteq X \times X$
95		difssd	$⊢ ((A \neq \emptyset \land D \in PsMet (X) \land A \subseteq X) \land (u \in 𝒫 (A \times A) \land ran (a \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, a)]) \cap 𝒫 u \neq \emptyset)) \to (X \times X) ∖ (A \times A) \subseteq X \times X$
96	94 95	unssd	$⊢ ((A \neq \emptyset \land D \in PsMet (X) \land A \subseteq X) \land (u \in 𝒫 (A \times A) \land ran (a \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, a)]) \cap 𝒫 u \neq \emptyset)) \to u \cup ((X \times X) ∖ (A \times A)) \subseteq X \times X$
97		simplr	$⊢ (((((A \neq \emptyset \land D \in PsMet (X) \land A \subseteq X) \land (u \in 𝒫 (A \times A) \land ran (a \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, a)]) \cap 𝒫 u \neq \emptyset)) \land v \in 𝒫 u) \land b \in ℝ^{+}) \land v = {({D ↾}_{(A \times A)})}^{-1} [[0, b)]) \to b \in ℝ^{+}$
98		eqidd	$⊢ (((((A \neq \emptyset \land D \in PsMet (X) \land A \subseteq X) \land (u \in 𝒫 (A \times A) \land ran (a \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, a)]) \cap 𝒫 u \neq \emptyset)) \land v \in 𝒫 u) \land b \in ℝ^{+}) \land v = {({D ↾}_{(A \times A)})}^{-1} [[0, b)]) \to D^{-1} [[0, b)] = D^{-1} [[0, b)]$
99	4	imaeq2d	$⊢ a = b \to D^{-1} [[0, a)] = D^{-1} [[0, b)]$
100	99	rspceeqv	$⊢ (b \in ℝ^{+} \land D^{-1} [[0, b)] = D^{-1} [[0, b)]) \to \exists a \in ℝ^{+} D^{-1} [[0, b)] = D^{-1} [[0, a)]$
101	97 98 100	syl2anc	$⊢ (((((A \neq \emptyset \land D \in PsMet (X) \land A \subseteq X) \land (u \in 𝒫 (A \times A) \land ran (a \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, a)]) \cap 𝒫 u \neq \emptyset)) \land v \in 𝒫 u) \land b \in ℝ^{+}) \land v = {({D ↾}_{(A \times A)})}^{-1} [[0, b)]) \to \exists a \in ℝ^{+} D^{-1} [[0, b)] = D^{-1} [[0, a)]$
102	43	ad4antr	$⊢ (((((A \neq \emptyset \land D \in PsMet (X) \land A \subseteq X) \land (u \in 𝒫 (A \times A) \land ran (a \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, a)]) \cap 𝒫 u \neq \emptyset)) \land v \in 𝒫 u) \land b \in ℝ^{+}) \land v = {({D ↾}_{(A \times A)})}^{-1} [[0, b)]) \to D \in PsMet (X)$
103		cnvexg	$⊢ D \in PsMet (X) \to D^{-1} \in V$
104		imaexg	$⊢ D^{-1} \in V \to D^{-1} [[0, b)] \in V$
105	74	elrnmpt	$⊢ D^{-1} [[0, b)] \in V \to (D^{-1} [[0, b)] \in ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)]) \leftrightarrow \exists a \in ℝ^{+} D^{-1} [[0, b)] = D^{-1} [[0, a)])$
106	102 103 104 105	4syl	$⊢ (((((A \neq \emptyset \land D \in PsMet (X) \land A \subseteq X) \land (u \in 𝒫 (A \times A) \land ran (a \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, a)]) \cap 𝒫 u \neq \emptyset)) \land v \in 𝒫 u) \land b \in ℝ^{+}) \land v = {({D ↾}_{(A \times A)})}^{-1} [[0, b)]) \to (D^{-1} [[0, b)] \in ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)]) \leftrightarrow \exists a \in ℝ^{+} D^{-1} [[0, b)] = D^{-1} [[0, a)])$
107	101 106	mpbird	$⊢ (((((A \neq \emptyset \land D \in PsMet (X) \land A \subseteq X) \land (u \in 𝒫 (A \times A) \land ran (a \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, a)]) \cap 𝒫 u \neq \emptyset)) \land v \in 𝒫 u) \land b \in ℝ^{+}) \land v = {({D ↾}_{(A \times A)})}^{-1} [[0, b)]) \to D^{-1} [[0, b)] \in ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)])$
108		cnvimass	$⊢ D^{-1} [[0, b)] \subseteq dom D$
109	108 44	fssdm	$⊢ D \in PsMet (X) \to D^{-1} [[0, b)] \subseteq X \times X$
110	102 109	syl	$⊢ (((((A \neq \emptyset \land D \in PsMet (X) \land A \subseteq X) \land (u \in 𝒫 (A \times A) \land ran (a \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, a)]) \cap 𝒫 u \neq \emptyset)) \land v \in 𝒫 u) \land b \in ℝ^{+}) \land v = {({D ↾}_{(A \times A)})}^{-1} [[0, b)]) \to D^{-1} [[0, b)] \subseteq X \times X$
111		ssdif0	$⊢ D^{-1} [[0, b)] \subseteq X \times X \leftrightarrow D^{-1} [[0, b)] ∖ (X \times X) = \emptyset$
112	110 111	sylib	$⊢ (((((A \neq \emptyset \land D \in PsMet (X) \land A \subseteq X) \land (u \in 𝒫 (A \times A) \land ran (a \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, a)]) \cap 𝒫 u \neq \emptyset)) \land v \in 𝒫 u) \land b \in ℝ^{+}) \land v = {({D ↾}_{(A \times A)})}^{-1} [[0, b)]) \to D^{-1} [[0, b)] ∖ (X \times X) = \emptyset$
113		0ss	$⊢ \emptyset \subseteq u$
114	112 113	eqsstrdi	$⊢ (((((A \neq \emptyset \land D \in PsMet (X) \land A \subseteq X) \land (u \in 𝒫 (A \times A) \land ran (a \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, a)]) \cap 𝒫 u \neq \emptyset)) \land v \in 𝒫 u) \land b \in ℝ^{+}) \land v = {({D ↾}_{(A \times A)})}^{-1} [[0, b)]) \to D^{-1} [[0, b)] ∖ (X \times X) \subseteq u$
115		respreima	$⊢ Fun D \to {({D ↾}_{(A \times A)})}^{-1} [[0, b)] = D^{-1} [[0, b)] \cap (A \times A)$
116	102 44 45 115	4syl	$⊢ (((((A \neq \emptyset \land D \in PsMet (X) \land A \subseteq X) \land (u \in 𝒫 (A \times A) \land ran (a \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, a)]) \cap 𝒫 u \neq \emptyset)) \land v \in 𝒫 u) \land b \in ℝ^{+}) \land v = {({D ↾}_{(A \times A)})}^{-1} [[0, b)]) \to {({D ↾}_{(A \times A)})}^{-1} [[0, b)] = D^{-1} [[0, b)] \cap (A \times A)$
117		simpr	$⊢ (((((A \neq \emptyset \land D \in PsMet (X) \land A \subseteq X) \land (u \in 𝒫 (A \times A) \land ran (a \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, a)]) \cap 𝒫 u \neq \emptyset)) \land v \in 𝒫 u) \land b \in ℝ^{+}) \land v = {({D ↾}_{(A \times A)})}^{-1} [[0, b)]) \to v = {({D ↾}_{(A \times A)})}^{-1} [[0, b)]$
118		simpllr	$⊢ (((((A \neq \emptyset \land D \in PsMet (X) \land A \subseteq X) \land (u \in 𝒫 (A \times A) \land ran (a \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, a)]) \cap 𝒫 u \neq \emptyset)) \land v \in 𝒫 u) \land b \in ℝ^{+}) \land v = {({D ↾}_{(A \times A)})}^{-1} [[0, b)]) \to v \in 𝒫 u$
119	118	elpwid	$⊢ (((((A \neq \emptyset \land D \in PsMet (X) \land A \subseteq X) \land (u \in 𝒫 (A \times A) \land ran (a \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, a)]) \cap 𝒫 u \neq \emptyset)) \land v \in 𝒫 u) \land b \in ℝ^{+}) \land v = {({D ↾}_{(A \times A)})}^{-1} [[0, b)]) \to v \subseteq u$
120	117 119	eqsstrrd	$⊢ (((((A \neq \emptyset \land D \in PsMet (X) \land A \subseteq X) \land (u \in 𝒫 (A \times A) \land ran (a \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, a)]) \cap 𝒫 u \neq \emptyset)) \land v \in 𝒫 u) \land b \in ℝ^{+}) \land v = {({D ↾}_{(A \times A)})}^{-1} [[0, b)]) \to {({D ↾}_{(A \times A)})}^{-1} [[0, b)] \subseteq u$
121	116 120	eqsstrrd	$⊢ (((((A \neq \emptyset \land D \in PsMet (X) \land A \subseteq X) \land (u \in 𝒫 (A \times A) \land ran (a \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, a)]) \cap 𝒫 u \neq \emptyset)) \land v \in 𝒫 u) \land b \in ℝ^{+}) \land v = {({D ↾}_{(A \times A)})}^{-1} [[0, b)]) \to D^{-1} [[0, b)] \cap (A \times A) \subseteq u$
122	114 121	unssd	$⊢ (((((A \neq \emptyset \land D \in PsMet (X) \land A \subseteq X) \land (u \in 𝒫 (A \times A) \land ran (a \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, a)]) \cap 𝒫 u \neq \emptyset)) \land v \in 𝒫 u) \land b \in ℝ^{+}) \land v = {({D ↾}_{(A \times A)})}^{-1} [[0, b)]) \to (D^{-1} [[0, b)] ∖ (X \times X)) \cup (D^{-1} [[0, b)] \cap (A \times A)) \subseteq u$
123		ssundif	$⊢ D^{-1} [[0, b)] \subseteq u \cup ((X \times X) ∖ (A \times A)) \leftrightarrow D^{-1} [[0, b)] ∖ u \subseteq (X \times X) ∖ (A \times A)$
124		difcom	$⊢ D^{-1} [[0, b)] ∖ u \subseteq (X \times X) ∖ (A \times A) \leftrightarrow D^{-1} [[0, b)] ∖ ((X \times X) ∖ (A \times A)) \subseteq u$
125		difdif2	$⊢ D^{-1} [[0, b)] ∖ ((X \times X) ∖ (A \times A)) = (D^{-1} [[0, b)] ∖ (X \times X)) \cup (D^{-1} [[0, b)] \cap (A \times A))$
126	125	sseq1i	$⊢ D^{-1} [[0, b)] ∖ ((X \times X) ∖ (A \times A)) \subseteq u \leftrightarrow (D^{-1} [[0, b)] ∖ (X \times X)) \cup (D^{-1} [[0, b)] \cap (A \times A)) \subseteq u$
127	123 124 126	3bitri	$⊢ D^{-1} [[0, b)] \subseteq u \cup ((X \times X) ∖ (A \times A)) \leftrightarrow (D^{-1} [[0, b)] ∖ (X \times X)) \cup (D^{-1} [[0, b)] \cap (A \times A)) \subseteq u$
128	122 127	sylibr	$⊢ (((((A \neq \emptyset \land D \in PsMet (X) \land A \subseteq X) \land (u \in 𝒫 (A \times A) \land ran (a \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, a)]) \cap 𝒫 u \neq \emptyset)) \land v \in 𝒫 u) \land b \in ℝ^{+}) \land v = {({D ↾}_{(A \times A)})}^{-1} [[0, b)]) \to D^{-1} [[0, b)] \subseteq u \cup ((X \times X) ∖ (A \times A))$
129		sseq1	$⊢ w = D^{-1} [[0, b)] \to (w \subseteq u \cup ((X \times X) ∖ (A \times A)) \leftrightarrow D^{-1} [[0, b)] \subseteq u \cup ((X \times X) ∖ (A \times A)))$
130	129	rspcev	$⊢ (D^{-1} [[0, b)] \in ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)]) \land D^{-1} [[0, b)] \subseteq u \cup ((X \times X) ∖ (A \times A))) \to \exists w \in ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)]) w \subseteq u \cup ((X \times X) ∖ (A \times A))$
131	107 128 130	syl2anc	$⊢ (((((A \neq \emptyset \land D \in PsMet (X) \land A \subseteq X) \land (u \in 𝒫 (A \times A) \land ran (a \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, a)]) \cap 𝒫 u \neq \emptyset)) \land v \in 𝒫 u) \land b \in ℝ^{+}) \land v = {({D ↾}_{(A \times A)})}^{-1} [[0, b)]) \to \exists w \in ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)]) w \subseteq u \cup ((X \times X) ∖ (A \times A))$
132		elin	$⊢ v \in (ran (a \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, a)]) \cap 𝒫 u) \leftrightarrow (v \in ran (a \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, a)]) \land v \in 𝒫 u)$
133	6	elrnmpt	$⊢ v \in V \to (v \in ran (a \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, a)]) \leftrightarrow \exists b \in ℝ^{+} v = {({D ↾}_{(A \times A)})}^{-1} [[0, b)])$
134	133	elv	$⊢ v \in ran (a \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, a)]) \leftrightarrow \exists b \in ℝ^{+} v = {({D ↾}_{(A \times A)})}^{-1} [[0, b)]$
135	134	anbi1i	$⊢ (v \in ran (a \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, a)]) \land v \in 𝒫 u) \leftrightarrow (\exists b \in ℝ^{+} v = {({D ↾}_{(A \times A)})}^{-1} [[0, b)] \land v \in 𝒫 u)$
136		ancom	$⊢ (\exists b \in ℝ^{+} v = {({D ↾}_{(A \times A)})}^{-1} [[0, b)] \land v \in 𝒫 u) \leftrightarrow (v \in 𝒫 u \land \exists b \in ℝ^{+} v = {({D ↾}_{(A \times A)})}^{-1} [[0, b)])$
137	132 135 136	3bitri	$⊢ v \in (ran (a \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, a)]) \cap 𝒫 u) \leftrightarrow (v \in 𝒫 u \land \exists b \in ℝ^{+} v = {({D ↾}_{(A \times A)})}^{-1} [[0, b)])$
138	137	exbii	$⊢ \exists v v \in (ran (a \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, a)]) \cap 𝒫 u) \leftrightarrow \exists v (v \in 𝒫 u \land \exists b \in ℝ^{+} v = {({D ↾}_{(A \times A)})}^{-1} [[0, b)])$
139		n0	$⊢ ran (a \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, a)]) \cap 𝒫 u \neq \emptyset \leftrightarrow \exists v v \in (ran (a \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, a)]) \cap 𝒫 u)$
140		df-rex	$⊢ \exists v \in 𝒫 u \exists b \in ℝ^{+} v = {({D ↾}_{(A \times A)})}^{-1} [[0, b)] \leftrightarrow \exists v (v \in 𝒫 u \land \exists b \in ℝ^{+} v = {({D ↾}_{(A \times A)})}^{-1} [[0, b)])$
141	138 139 140	3bitr4i	$⊢ ran (a \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, a)]) \cap 𝒫 u \neq \emptyset \leftrightarrow \exists v \in 𝒫 u \exists b \in ℝ^{+} v = {({D ↾}_{(A \times A)})}^{-1} [[0, b)]$
142	141	biimpi	$⊢ ran (a \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, a)]) \cap 𝒫 u \neq \emptyset \to \exists v \in 𝒫 u \exists b \in ℝ^{+} v = {({D ↾}_{(A \times A)})}^{-1} [[0, b)]$
143	142	ad2antll	$⊢ ((A \neq \emptyset \land D \in PsMet (X) \land A \subseteq X) \land (u \in 𝒫 (A \times A) \land ran (a \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, a)]) \cap 𝒫 u \neq \emptyset)) \to \exists v \in 𝒫 u \exists b \in ℝ^{+} v = {({D ↾}_{(A \times A)})}^{-1} [[0, b)]$
144	131 143	r19.29vva	$⊢ ((A \neq \emptyset \land D \in PsMet (X) \land A \subseteq X) \land (u \in 𝒫 (A \times A) \land ran (a \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, a)]) \cap 𝒫 u \neq \emptyset)) \to \exists w \in ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)]) w \subseteq u \cup ((X \times X) ∖ (A \times A))$
145	81	adantr	$⊢ ((A \neq \emptyset \land D \in PsMet (X) \land A \subseteq X) \land (u \in 𝒫 (A \times A) \land ran (a \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, a)]) \cap 𝒫 u \neq \emptyset)) \to X \neq \emptyset$
146	43	adantr	$⊢ ((A \neq \emptyset \land D \in PsMet (X) \land A \subseteq X) \land (u \in 𝒫 (A \times A) \land ran (a \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, a)]) \cap 𝒫 u \neq \emptyset)) \to D \in PsMet (X)$
147		metuel	$⊢ (X \neq \emptyset \land D \in PsMet (X)) \to (u \cup ((X \times X) ∖ (A \times A)) \in metUnif (D) \leftrightarrow (u \cup ((X \times X) ∖ (A \times A)) \subseteq X \times X \land \exists w \in ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)]) w \subseteq u \cup ((X \times X) ∖ (A \times A))))$
148	145 146 147	syl2anc	$⊢ ((A \neq \emptyset \land D \in PsMet (X) \land A \subseteq X) \land (u \in 𝒫 (A \times A) \land ran (a \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, a)]) \cap 𝒫 u \neq \emptyset)) \to (u \cup ((X \times X) ∖ (A \times A)) \in metUnif (D) \leftrightarrow (u \cup ((X \times X) ∖ (A \times A)) \subseteq X \times X \land \exists w \in ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)]) w \subseteq u \cup ((X \times X) ∖ (A \times A))))$
149	96 144 148	mpbir2and	$⊢ ((A \neq \emptyset \land D \in PsMet (X) \land A \subseteq X) \land (u \in 𝒫 (A \times A) \land ran (a \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, a)]) \cap 𝒫 u \neq \emptyset)) \to u \cup ((X \times X) ∖ (A \times A)) \in metUnif (D)$
150		indir	$⊢ (u \cup ((X \times X) ∖ (A \times A))) \cap (A \times A) = (u \cap (A \times A)) \cup (((X \times X) ∖ (A \times A)) \cap (A \times A))$
151		incom	$⊢ (A \times A) \cap ((X \times X) ∖ (A \times A)) = ((X \times X) ∖ (A \times A)) \cap (A \times A)$
152		disjdif	$⊢ (A \times A) \cap ((X \times X) ∖ (A \times A)) = \emptyset$
153	151 152	eqtr3i	$⊢ ((X \times X) ∖ (A \times A)) \cap (A \times A) = \emptyset$
154	153	uneq2i	$⊢ (u \cap (A \times A)) \cup (((X \times X) ∖ (A \times A)) \cap (A \times A)) = (u \cap (A \times A)) \cup \emptyset$
155		un0	$⊢ (u \cap (A \times A)) \cup \emptyset = u \cap (A \times A)$
156	150 154 155	3eqtri	$⊢ (u \cup ((X \times X) ∖ (A \times A))) \cap (A \times A) = u \cap (A \times A)$
157		df-ss	$⊢ u \subseteq A \times A \leftrightarrow u \cap (A \times A) = u$
158	90 157	sylib	$⊢ ((A \neq \emptyset \land D \in PsMet (X) \land A \subseteq X) \land (u \in 𝒫 (A \times A) \land ran (a \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, a)]) \cap 𝒫 u \neq \emptyset)) \to u \cap (A \times A) = u$
159	156 158	syl5req	$⊢ ((A \neq \emptyset \land D \in PsMet (X) \land A \subseteq X) \land (u \in 𝒫 (A \times A) \land ran (a \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, a)]) \cap 𝒫 u \neq \emptyset)) \to u = (u \cup ((X \times X) ∖ (A \times A))) \cap (A \times A)$
160		ineq1	$⊢ v = u \cup ((X \times X) ∖ (A \times A)) \to v \cap (A \times A) = (u \cup ((X \times X) ∖ (A \times A))) \cap (A \times A)$
161	160	rspceeqv	$⊢ (u \cup ((X \times X) ∖ (A \times A)) \in metUnif (D) \land u = (u \cup ((X \times X) ∖ (A \times A))) \cap (A \times A)) \to \exists v \in metUnif (D) u = v \cap (A \times A)$
162	149 159 161	syl2anc	$⊢ ((A \neq \emptyset \land D \in PsMet (X) \land A \subseteq X) \land (u \in 𝒫 (A \times A) \land ran (a \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, a)]) \cap 𝒫 u \neq \emptyset)) \to \exists v \in metUnif (D) u = v \cap (A \times A)$
163	88 162	impbida	$⊢ (A \neq \emptyset \land D \in PsMet (X) \land A \subseteq X) \to (\exists v \in metUnif (D) u = v \cap (A \times A) \leftrightarrow (u \in 𝒫 (A \times A) \land ran (a \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, a)]) \cap 𝒫 u \neq \emptyset))$
164		eqid	$⊢ (v \in metUnif (D) ⟼ v \cap (A \times A)) = (v \in metUnif (D) ⟼ v \cap (A \times A))$
165	164	elrnmpt	$⊢ u \in V \to (u \in ran (v \in metUnif (D) ⟼ v \cap (A \times A)) \leftrightarrow \exists v \in metUnif (D) u = v \cap (A \times A))$
166	165	elv	$⊢ u \in ran (v \in metUnif (D) ⟼ v \cap (A \times A)) \leftrightarrow \exists v \in metUnif (D) u = v \cap (A \times A)$
167		pweq	$⊢ v = u \to 𝒫 v = 𝒫 u$
168	167	ineq2d	$⊢ v = u \to ran (a \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, a)]) \cap 𝒫 v = ran (a \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, a)]) \cap 𝒫 u$
169	168	neeq1d	$⊢ v = u \to (ran (a \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, a)]) \cap 𝒫 v \neq \emptyset \leftrightarrow ran (a \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, a)]) \cap 𝒫 u \neq \emptyset)$
170	169	elrab	$⊢ u \in \{v \in 𝒫 (A \times A) \| ran (a \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, a)]) \cap 𝒫 v \neq \emptyset\} \leftrightarrow (u \in 𝒫 (A \times A) \land ran (a \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, a)]) \cap 𝒫 u \neq \emptyset)$
171	163 166 170	3bitr4g	$⊢ (A \neq \emptyset \land D \in PsMet (X) \land A \subseteq X) \to (u \in ran (v \in metUnif (D) ⟼ v \cap (A \times A)) \leftrightarrow u \in \{v \in 𝒫 (A \times A) \| ran (a \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, a)]) \cap 𝒫 v \neq \emptyset\})$
172	171	eqrdv	$⊢ (A \neq \emptyset \land D \in PsMet (X) \land A \subseteq X) \to ran (v \in metUnif (D) ⟼ v \cap (A \times A)) = \{v \in 𝒫 (A \times A) \| ran (a \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, a)]) \cap 𝒫 v \neq \emptyset\}$
173	18 172	eqtrd	$⊢ (A \neq \emptyset \land D \in PsMet (X) \land A \subseteq X) \to metUnif (D) ↾_{𝑡} (A \times A) = \{v \in 𝒫 (A \times A) \| ran (a \in ℝ^{+} ⟼ {({D ↾}_{(A \times A)})}^{-1} [[0, a)]) \cap 𝒫 v \neq \emptyset\}$
174	11 13 173	3eqtr4rd	$⊢ (A \neq \emptyset \land D \in PsMet (X) \land A \subseteq X) \to metUnif (D) ↾_{𝑡} (A \times A) = metUnif ({D ↾}_{(A \times A)})$

Metamath Proof Explorer

Theorem restmetu

Proof