Metamath Proof Explorer

Theorem metustid

Description: The identity diagonal is included in all elements of the filter base generated by the metric D . (Contributed by Thierry Arnoux, 22-Nov-2017) (Revised by Thierry Arnoux, 11-Feb-2018) (Proof shortened by Peter Mazsa, 2-Oct-2022)

Ref Expression
Hypothesis metust.1 
|- F = ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) )
Assertion metustid 
|- ( ( D e. ( PsMet ` X ) /\ A e. F ) -> ( _I |` X ) C_ A )

Proof

Step Hyp Ref Expression
1 metust.1 
 |-  F = ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) )
2 relres 
 |-  Rel ( _I |` X )
3 2 a1i 
 |-  ( ( D e. ( PsMet ` X ) /\ A e. F ) -> Rel ( _I |` X ) )
4 vex 
 |-  q e. _V
5 4 brresi 
 |-  ( p ( _I |` X ) q <-> ( p e. X /\ p _I q ) )
6 df-br 
 |-  ( p ( _I |` X ) q <-> <. p , q >. e. ( _I |` X ) )
7 4 ideq 
 |-  ( p _I q <-> p = q )
8 7 anbi2i 
 |-  ( ( p e. X /\ p _I q ) <-> ( p e. X /\ p = q ) )
9 5 6 8 3bitr3i 
 |-  ( <. p , q >. e. ( _I |` X ) <-> ( p e. X /\ p = q ) )
10 9 biimpi 
 |-  ( <. p , q >. e. ( _I |` X ) -> ( p e. X /\ p = q ) )
11 10 ad2antlr 
 |-  ( ( ( ( D e. ( PsMet ` X ) /\ A e. F ) /\ <. p , q >. e. ( _I |` X ) ) /\ a e. RR+ ) -> ( p e. X /\ p = q ) )
12 11 simprd 
 |-  ( ( ( ( D e. ( PsMet ` X ) /\ A e. F ) /\ <. p , q >. e. ( _I |` X ) ) /\ a e. RR+ ) -> p = q )
13 df-ov 
 |-  ( p D p ) = ( D ` <. p , p >. )
14 opeq2 
 |-  ( p = q -> <. p , p >. = <. p , q >. )
15 14 fveq2d 
 |-  ( p = q -> ( D ` <. p , p >. ) = ( D ` <. p , q >. ) )
16 13 15 syl5eq 
 |-  ( p = q -> ( p D p ) = ( D ` <. p , q >. ) )
17 12 16 syl 
 |-  ( ( ( ( D e. ( PsMet ` X ) /\ A e. F ) /\ <. p , q >. e. ( _I |` X ) ) /\ a e. RR+ ) -> ( p D p ) = ( D ` <. p , q >. ) )
18 simplll 
 |-  ( ( ( ( D e. ( PsMet ` X ) /\ A e. F ) /\ <. p , q >. e. ( _I |` X ) ) /\ a e. RR+ ) -> D e. ( PsMet ` X ) )
19 11 simpld 
 |-  ( ( ( ( D e. ( PsMet ` X ) /\ A e. F ) /\ <. p , q >. e. ( _I |` X ) ) /\ a e. RR+ ) -> p e. X )
20 psmet0 
 |-  ( ( D e. ( PsMet ` X ) /\ p e. X ) -> ( p D p ) = 0 )
21 18 19 20 syl2anc 
 |-  ( ( ( ( D e. ( PsMet ` X ) /\ A e. F ) /\ <. p , q >. e. ( _I |` X ) ) /\ a e. RR+ ) -> ( p D p ) = 0 )
22 17 21 eqtr3d 
 |-  ( ( ( ( D e. ( PsMet ` X ) /\ A e. F ) /\ <. p , q >. e. ( _I |` X ) ) /\ a e. RR+ ) -> ( D ` <. p , q >. ) = 0 )
23 0xr 
 |-  0 e. RR*
24 rpxr 
 |-  ( a e. RR+ -> a e. RR* )
25 rpgt0 
 |-  ( a e. RR+ -> 0 < a )
26 lbico1 
 |-  ( ( 0 e. RR* /\ a e. RR* /\ 0 < a ) -> 0 e. ( 0 [,) a ) )
27 23 24 25 26 mp3an2i 
 |-  ( a e. RR+ -> 0 e. ( 0 [,) a ) )
28 27 adantl 
 |-  ( ( ( ( D e. ( PsMet ` X ) /\ A e. F ) /\ <. p , q >. e. ( _I |` X ) ) /\ a e. RR+ ) -> 0 e. ( 0 [,) a ) )
29 22 28 eqeltrd 
 |-  ( ( ( ( D e. ( PsMet ` X ) /\ A e. F ) /\ <. p , q >. e. ( _I |` X ) ) /\ a e. RR+ ) -> ( D ` <. p , q >. ) e. ( 0 [,) a ) )
30 psmetf 
 |-  ( D e. ( PsMet ` X ) -> D : ( X X. X ) --> RR* )
31 30 ffund 
 |-  ( D e. ( PsMet ` X ) -> Fun D )
32 31 ad3antrrr 
 |-  ( ( ( ( D e. ( PsMet ` X ) /\ A e. F ) /\ <. p , q >. e. ( _I |` X ) ) /\ a e. RR+ ) -> Fun D )
33 12 19 eqeltrrd 
 |-  ( ( ( ( D e. ( PsMet ` X ) /\ A e. F ) /\ <. p , q >. e. ( _I |` X ) ) /\ a e. RR+ ) -> q e. X )
34 19 33 opelxpd 
 |-  ( ( ( ( D e. ( PsMet ` X ) /\ A e. F ) /\ <. p , q >. e. ( _I |` X ) ) /\ a e. RR+ ) -> <. p , q >. e. ( X X. X ) )
35 30 fdmd 
 |-  ( D e. ( PsMet ` X ) -> dom D = ( X X. X ) )
36 35 ad3antrrr 
 |-  ( ( ( ( D e. ( PsMet ` X ) /\ A e. F ) /\ <. p , q >. e. ( _I |` X ) ) /\ a e. RR+ ) -> dom D = ( X X. X ) )
37 34 36 eleqtrrd 
 |-  ( ( ( ( D e. ( PsMet ` X ) /\ A e. F ) /\ <. p , q >. e. ( _I |` X ) ) /\ a e. RR+ ) -> <. p , q >. e. dom D )
38 fvimacnv 
 |-  ( ( Fun D /\ <. p , q >. e. dom D ) -> ( ( D ` <. p , q >. ) e. ( 0 [,) a ) <-> <. p , q >. e. ( `' D " ( 0 [,) a ) ) ) )
39 32 37 38 syl2anc 
 |-  ( ( ( ( D e. ( PsMet ` X ) /\ A e. F ) /\ <. p , q >. e. ( _I |` X ) ) /\ a e. RR+ ) -> ( ( D ` <. p , q >. ) e. ( 0 [,) a ) <-> <. p , q >. e. ( `' D " ( 0 [,) a ) ) ) )
40 29 39 mpbid 
 |-  ( ( ( ( D e. ( PsMet ` X ) /\ A e. F ) /\ <. p , q >. e. ( _I |` X ) ) /\ a e. RR+ ) -> <. p , q >. e. ( `' D " ( 0 [,) a ) ) )
41 40 adantr 
 |-  ( ( ( ( ( D e. ( PsMet ` X ) /\ A e. F ) /\ <. p , q >. e. ( _I |` X ) ) /\ a e. RR+ ) /\ A = ( `' D " ( 0 [,) a ) ) ) -> <. p , q >. e. ( `' D " ( 0 [,) a ) ) )
42 simpr 
 |-  ( ( ( ( ( D e. ( PsMet ` X ) /\ A e. F ) /\ <. p , q >. e. ( _I |` X ) ) /\ a e. RR+ ) /\ A = ( `' D " ( 0 [,) a ) ) ) -> A = ( `' D " ( 0 [,) a ) ) )
43 41 42 eleqtrrd 
 |-  ( ( ( ( ( D e. ( PsMet ` X ) /\ A e. F ) /\ <. p , q >. e. ( _I |` X ) ) /\ a e. RR+ ) /\ A = ( `' D " ( 0 [,) a ) ) ) -> <. p , q >. e. A )
44 simplr 
 |-  ( ( ( D e. ( PsMet ` X ) /\ A e. F ) /\ <. p , q >. e. ( _I |` X ) ) -> A e. F )
45 1 metustel 
 |-  ( D e. ( PsMet ` X ) -> ( A e. F <-> E. a e. RR+ A = ( `' D " ( 0 [,) a ) ) ) )
46 45 ad2antrr 
 |-  ( ( ( D e. ( PsMet ` X ) /\ A e. F ) /\ <. p , q >. e. ( _I |` X ) ) -> ( A e. F <-> E. a e. RR+ A = ( `' D " ( 0 [,) a ) ) ) )
47 44 46 mpbid 
 |-  ( ( ( D e. ( PsMet ` X ) /\ A e. F ) /\ <. p , q >. e. ( _I |` X ) ) -> E. a e. RR+ A = ( `' D " ( 0 [,) a ) ) )
48 43 47 r19.29a 
 |-  ( ( ( D e. ( PsMet ` X ) /\ A e. F ) /\ <. p , q >. e. ( _I |` X ) ) -> <. p , q >. e. A )
49 48 ex 
 |-  ( ( D e. ( PsMet ` X ) /\ A e. F ) -> ( <. p , q >. e. ( _I |` X ) -> <. p , q >. e. A ) )
50 3 49 relssdv 
 |-  ( ( D e. ( PsMet ` X ) /\ A e. F ) -> ( _I |` X ) C_ A )