Metamath Proof Explorer


Theorem 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 D PsMet X V U V X × X d + x X y X x D y < d x V y

Proof

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