Metamath Proof Explorer


Theorem metustsym

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 F=rana+D-10a
Assertion metustsym DPsMetXAFA-1=A

Proof

Step Hyp Ref Expression
1 metust.1 F=rana+D-10a
2 1 metustss DPsMetXAFAX×X
3 cnvss AX×XA-1X×X-1
4 cnvxp X×X-1=X×X
5 3 4 sseqtrdi AX×XA-1X×X
6 2 5 syl DPsMetXAFA-1X×X
7 simp-4l DPsMetXAFpXqXa+A=D-10aDPsMetX
8 simpr1r DPsMetXAFpXqXa+A=D-10aqX
9 8 3anassrs DPsMetXAFpXqXa+A=D-10aqX
10 simpr1l DPsMetXAFpXqXa+A=D-10apX
11 10 3anassrs DPsMetXAFpXqXa+A=D-10apX
12 psmetsym DPsMetXqXpXqDp=pDq
13 7 9 11 12 syl3anc DPsMetXAFpXqXa+A=D-10aqDp=pDq
14 df-ov qDp=Dqp
15 df-ov pDq=Dpq
16 13 14 15 3eqtr3g DPsMetXAFpXqXa+A=D-10aDqp=Dpq
17 16 eleq1d DPsMetXAFpXqXa+A=D-10aDqp0aDpq0a
18 psmetf DPsMetXD:X×X*
19 ffun D:X×X*FunD
20 7 18 19 3syl DPsMetXAFpXqXa+A=D-10aFunD
21 simpllr DPsMetXAFpXqXa+A=D-10apXqX
22 21 ancomd DPsMetXAFpXqXa+A=D-10aqXpX
23 opelxpi qXpXqpX×X
24 22 23 syl DPsMetXAFpXqXa+A=D-10aqpX×X
25 fdm D:X×X*domD=X×X
26 7 18 25 3syl DPsMetXAFpXqXa+A=D-10adomD=X×X
27 24 26 eleqtrrd DPsMetXAFpXqXa+A=D-10aqpdomD
28 fvimacnv FunDqpdomDDqp0aqpD-10a
29 20 27 28 syl2anc DPsMetXAFpXqXa+A=D-10aDqp0aqpD-10a
30 opelxpi pXqXpqX×X
31 21 30 syl DPsMetXAFpXqXa+A=D-10apqX×X
32 31 26 eleqtrrd DPsMetXAFpXqXa+A=D-10apqdomD
33 fvimacnv FunDpqdomDDpq0apqD-10a
34 20 32 33 syl2anc DPsMetXAFpXqXa+A=D-10aDpq0apqD-10a
35 17 29 34 3bitr3d DPsMetXAFpXqXa+A=D-10aqpD-10apqD-10a
36 simpr DPsMetXAFpXqXa+A=D-10aA=D-10a
37 36 eleq2d DPsMetXAFpXqXa+A=D-10aqpAqpD-10a
38 36 eleq2d DPsMetXAFpXqXa+A=D-10apqApqD-10a
39 35 37 38 3bitr4d DPsMetXAFpXqXa+A=D-10aqpApqA
40 eqid a+D-10a=a+D-10a
41 40 elrnmpt Arana+D-10aArana+D-10aa+A=D-10a
42 41 ibi Arana+D-10aa+A=D-10a
43 42 1 eleq2s AFa+A=D-10a
44 43 ad2antlr DPsMetXAFpXqXa+A=D-10a
45 39 44 r19.29a DPsMetXAFpXqXqpApqA
46 df-br pA-1qpqA-1
47 vex pV
48 vex qV
49 47 48 opelcnv pqA-1qpA
50 46 49 bitri pA-1qqpA
51 df-br pAqpqA
52 45 50 51 3bitr4g DPsMetXAFpXqXpA-1qpAq
53 52 3impb DPsMetXAFpXqXpA-1qpAq
54 6 2 53 eqbrrdva DPsMetXAFA-1=A