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 = ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) )
Assertion metustsym 
|- ( ( D e. ( PsMet ` X ) /\ A e. F ) -> `' A = A )

Proof

Step Hyp Ref Expression
1 metust.1 
 |-  F = ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) )
2 1 metustss 
 |-  ( ( D e. ( PsMet ` X ) /\ A e. F ) -> A C_ ( X X. X ) )
3 cnvss 
 |-  ( A C_ ( X X. X ) -> `' A C_ `' ( X X. X ) )
4 cnvxp 
 |-  `' ( X X. X ) = ( X X. X )
5 3 4 sseqtrdi 
 |-  ( A C_ ( X X. X ) -> `' A C_ ( X X. X ) )
6 2 5 syl 
 |-  ( ( D e. ( PsMet ` X ) /\ A e. F ) -> `' A C_ ( X X. X ) )
7 simp-4l 
 |-  ( ( ( ( ( D e. ( PsMet ` X ) /\ A e. F ) /\ ( p e. X /\ q e. X ) ) /\ a e. RR+ ) /\ A = ( `' D " ( 0 [,) a ) ) ) -> D e. ( PsMet ` X ) )
8 simpr1r 
 |-  ( ( ( D e. ( PsMet ` X ) /\ A e. F ) /\ ( ( p e. X /\ q e. X ) /\ a e. RR+ /\ A = ( `' D " ( 0 [,) a ) ) ) ) -> q e. X )
9 8 3anassrs 
 |-  ( ( ( ( ( D e. ( PsMet ` X ) /\ A e. F ) /\ ( p e. X /\ q e. X ) ) /\ a e. RR+ ) /\ A = ( `' D " ( 0 [,) a ) ) ) -> q e. X )
10 simpr1l 
 |-  ( ( ( D e. ( PsMet ` X ) /\ A e. F ) /\ ( ( p e. X /\ q e. X ) /\ a e. RR+ /\ A = ( `' D " ( 0 [,) a ) ) ) ) -> p e. X )
11 10 3anassrs 
 |-  ( ( ( ( ( D e. ( PsMet ` X ) /\ A e. F ) /\ ( p e. X /\ q e. X ) ) /\ a e. RR+ ) /\ A = ( `' D " ( 0 [,) a ) ) ) -> p e. X )
12 psmetsym 
 |-  ( ( D e. ( PsMet ` X ) /\ q e. X /\ p e. X ) -> ( q D p ) = ( p D q ) )
13 7 9 11 12 syl3anc 
 |-  ( ( ( ( ( D e. ( PsMet ` X ) /\ A e. F ) /\ ( p e. X /\ q e. X ) ) /\ a e. RR+ ) /\ A = ( `' D " ( 0 [,) a ) ) ) -> ( q D p ) = ( p D q ) )
14 df-ov 
 |-  ( q D p ) = ( D ` <. q , p >. )
15 df-ov 
 |-  ( p D q ) = ( D ` <. p , q >. )
16 13 14 15 3eqtr3g 
 |-  ( ( ( ( ( D e. ( PsMet ` X ) /\ A e. F ) /\ ( p e. X /\ q e. X ) ) /\ a e. RR+ ) /\ A = ( `' D " ( 0 [,) a ) ) ) -> ( D ` <. q , p >. ) = ( D ` <. p , q >. ) )
17 16 eleq1d 
 |-  ( ( ( ( ( D e. ( PsMet ` X ) /\ A e. F ) /\ ( p e. X /\ q e. X ) ) /\ a e. RR+ ) /\ A = ( `' D " ( 0 [,) a ) ) ) -> ( ( D ` <. q , p >. ) e. ( 0 [,) a ) <-> ( D ` <. p , q >. ) e. ( 0 [,) a ) ) )
18 psmetf 
 |-  ( D e. ( PsMet ` X ) -> D : ( X X. X ) --> RR* )
19 ffun 
 |-  ( D : ( X X. X ) --> RR* -> Fun D )
20 7 18 19 3syl 
 |-  ( ( ( ( ( D e. ( PsMet ` X ) /\ A e. F ) /\ ( p e. X /\ q e. X ) ) /\ a e. RR+ ) /\ A = ( `' D " ( 0 [,) a ) ) ) -> Fun D )
21 simpllr 
 |-  ( ( ( ( ( D e. ( PsMet ` X ) /\ A e. F ) /\ ( p e. X /\ q e. X ) ) /\ a e. RR+ ) /\ A = ( `' D " ( 0 [,) a ) ) ) -> ( p e. X /\ q e. X ) )
22 21 ancomd 
 |-  ( ( ( ( ( D e. ( PsMet ` X ) /\ A e. F ) /\ ( p e. X /\ q e. X ) ) /\ a e. RR+ ) /\ A = ( `' D " ( 0 [,) a ) ) ) -> ( q e. X /\ p e. X ) )
23 opelxpi 
 |-  ( ( q e. X /\ p e. X ) -> <. q , p >. e. ( X X. X ) )
24 22 23 syl 
 |-  ( ( ( ( ( D e. ( PsMet ` X ) /\ A e. F ) /\ ( p e. X /\ q e. X ) ) /\ a e. RR+ ) /\ A = ( `' D " ( 0 [,) a ) ) ) -> <. q , p >. e. ( X X. X ) )
25 fdm 
 |-  ( D : ( X X. X ) --> RR* -> dom D = ( X X. X ) )
26 7 18 25 3syl 
 |-  ( ( ( ( ( D e. ( PsMet ` X ) /\ A e. F ) /\ ( p e. X /\ q e. X ) ) /\ a e. RR+ ) /\ A = ( `' D " ( 0 [,) a ) ) ) -> dom D = ( X X. X ) )
27 24 26 eleqtrrd 
 |-  ( ( ( ( ( D e. ( PsMet ` X ) /\ A e. F ) /\ ( p e. X /\ q e. X ) ) /\ a e. RR+ ) /\ A = ( `' D " ( 0 [,) a ) ) ) -> <. q , p >. e. dom D )
28 fvimacnv 
 |-  ( ( Fun D /\ <. q , p >. e. dom D ) -> ( ( D ` <. q , p >. ) e. ( 0 [,) a ) <-> <. q , p >. e. ( `' D " ( 0 [,) a ) ) ) )
29 20 27 28 syl2anc 
 |-  ( ( ( ( ( D e. ( PsMet ` X ) /\ A e. F ) /\ ( p e. X /\ q e. X ) ) /\ a e. RR+ ) /\ A = ( `' D " ( 0 [,) a ) ) ) -> ( ( D ` <. q , p >. ) e. ( 0 [,) a ) <-> <. q , p >. e. ( `' D " ( 0 [,) a ) ) ) )
30 opelxpi 
 |-  ( ( p e. X /\ q e. X ) -> <. p , q >. e. ( X X. X ) )
31 21 30 syl 
 |-  ( ( ( ( ( D e. ( PsMet ` X ) /\ A e. F ) /\ ( p e. X /\ q e. X ) ) /\ a e. RR+ ) /\ A = ( `' D " ( 0 [,) a ) ) ) -> <. p , q >. e. ( X X. X ) )
32 31 26 eleqtrrd 
 |-  ( ( ( ( ( D e. ( PsMet ` X ) /\ A e. F ) /\ ( p e. X /\ q e. X ) ) /\ a e. RR+ ) /\ A = ( `' D " ( 0 [,) a ) ) ) -> <. p , q >. e. dom D )
33 fvimacnv 
 |-  ( ( Fun D /\ <. p , q >. e. dom D ) -> ( ( D ` <. p , q >. ) e. ( 0 [,) a ) <-> <. p , q >. e. ( `' D " ( 0 [,) a ) ) ) )
34 20 32 33 syl2anc 
 |-  ( ( ( ( ( D e. ( PsMet ` X ) /\ A e. F ) /\ ( p e. X /\ q e. X ) ) /\ a e. RR+ ) /\ A = ( `' D " ( 0 [,) a ) ) ) -> ( ( D ` <. p , q >. ) e. ( 0 [,) a ) <-> <. p , q >. e. ( `' D " ( 0 [,) a ) ) ) )
35 17 29 34 3bitr3d 
 |-  ( ( ( ( ( D e. ( PsMet ` X ) /\ A e. F ) /\ ( p e. X /\ q e. X ) ) /\ a e. RR+ ) /\ A = ( `' D " ( 0 [,) a ) ) ) -> ( <. q , p >. e. ( `' D " ( 0 [,) a ) ) <-> <. p , q >. e. ( `' D " ( 0 [,) a ) ) ) )
36 simpr 
 |-  ( ( ( ( ( D e. ( PsMet ` X ) /\ A e. F ) /\ ( p e. X /\ q e. X ) ) /\ a e. RR+ ) /\ A = ( `' D " ( 0 [,) a ) ) ) -> A = ( `' D " ( 0 [,) a ) ) )
37 36 eleq2d 
 |-  ( ( ( ( ( D e. ( PsMet ` X ) /\ A e. F ) /\ ( p e. X /\ q e. X ) ) /\ a e. RR+ ) /\ A = ( `' D " ( 0 [,) a ) ) ) -> ( <. q , p >. e. A <-> <. q , p >. e. ( `' D " ( 0 [,) a ) ) ) )
38 36 eleq2d 
 |-  ( ( ( ( ( D e. ( PsMet ` X ) /\ A e. F ) /\ ( p e. X /\ q e. X ) ) /\ a e. RR+ ) /\ A = ( `' D " ( 0 [,) a ) ) ) -> ( <. p , q >. e. A <-> <. p , q >. e. ( `' D " ( 0 [,) a ) ) ) )
39 35 37 38 3bitr4d 
 |-  ( ( ( ( ( D e. ( PsMet ` X ) /\ A e. F ) /\ ( p e. X /\ q e. X ) ) /\ a e. RR+ ) /\ A = ( `' D " ( 0 [,) a ) ) ) -> ( <. q , p >. e. A <-> <. p , q >. e. A ) )
40 eqid 
 |-  ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) = ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) )
41 40 elrnmpt 
 |-  ( A e. ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) -> ( A e. ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) <-> E. a e. RR+ A = ( `' D " ( 0 [,) a ) ) ) )
42 41 ibi 
 |-  ( A e. ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) -> E. a e. RR+ A = ( `' D " ( 0 [,) a ) ) )
43 42 1 eleq2s 
 |-  ( A e. F -> E. a e. RR+ A = ( `' D " ( 0 [,) a ) ) )
44 43 ad2antlr 
 |-  ( ( ( D e. ( PsMet ` X ) /\ A e. F ) /\ ( p e. X /\ q e. X ) ) -> E. a e. RR+ A = ( `' D " ( 0 [,) a ) ) )
45 39 44 r19.29a 
 |-  ( ( ( D e. ( PsMet ` X ) /\ A e. F ) /\ ( p e. X /\ q e. X ) ) -> ( <. q , p >. e. A <-> <. p , q >. e. A ) )
46 df-br 
 |-  ( p `' A q <-> <. p , q >. e. `' A )
47 vex 
 |-  p e. _V
48 vex 
 |-  q e. _V
49 47 48 opelcnv 
 |-  ( <. p , q >. e. `' A <-> <. q , p >. e. A )
50 46 49 bitri 
 |-  ( p `' A q <-> <. q , p >. e. A )
51 df-br 
 |-  ( p A q <-> <. p , q >. e. A )
52 45 50 51 3bitr4g 
 |-  ( ( ( D e. ( PsMet ` X ) /\ A e. F ) /\ ( p e. X /\ q e. X ) ) -> ( p `' A q <-> p A q ) )
53 52 3impb 
 |-  ( ( ( D e. ( PsMet ` X ) /\ A e. F ) /\ p e. X /\ q e. X ) -> ( p `' A q <-> p A q ) )
54 6 2 53 eqbrrdva 
 |-  ( ( D e. ( PsMet ` X ) /\ A e. F ) -> `' A = A )