Description: Elements of the filter base generated by the metric D are symmetric. (Contributed by Thierry Arnoux, 28-Nov-2017) (Revised by Thierry Arnoux, 11-Feb-2018)
Ref | Expression | ||
---|---|---|---|
Hypothesis | metust.1 | |
|
Assertion | metustsym | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | metust.1 | |
|
2 | 1 | metustss | |
3 | cnvss | |
|
4 | cnvxp | |
|
5 | 3 4 | sseqtrdi | |
6 | 2 5 | syl | |
7 | simp-4l | |
|
8 | simpr1r | |
|
9 | 8 | 3anassrs | |
10 | simpr1l | |
|
11 | 10 | 3anassrs | |
12 | psmetsym | |
|
13 | 7 9 11 12 | syl3anc | |
14 | df-ov | |
|
15 | df-ov | |
|
16 | 13 14 15 | 3eqtr3g | |
17 | 16 | eleq1d | |
18 | psmetf | |
|
19 | ffun | |
|
20 | 7 18 19 | 3syl | |
21 | simpllr | |
|
22 | 21 | ancomd | |
23 | opelxpi | |
|
24 | 22 23 | syl | |
25 | fdm | |
|
26 | 7 18 25 | 3syl | |
27 | 24 26 | eleqtrrd | |
28 | fvimacnv | |
|
29 | 20 27 28 | syl2anc | |
30 | opelxpi | |
|
31 | 21 30 | syl | |
32 | 31 26 | eleqtrrd | |
33 | fvimacnv | |
|
34 | 20 32 33 | syl2anc | |
35 | 17 29 34 | 3bitr3d | |
36 | simpr | |
|
37 | 36 | eleq2d | |
38 | 36 | eleq2d | |
39 | 35 37 38 | 3bitr4d | |
40 | eqid | |
|
41 | 40 | elrnmpt | |
42 | 41 | ibi | |
43 | 42 1 | eleq2s | |
44 | 43 | ad2antlr | |
45 | 39 44 | r19.29a | |
46 | df-br | |
|
47 | vex | |
|
48 | vex | |
|
49 | 47 48 | opelcnv | |
50 | 46 49 | bitri | |
51 | df-br | |
|
52 | 45 50 51 | 3bitr4g | |
53 | 52 | 3impb | |
54 | 6 2 53 | eqbrrdva | |