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 )