Metamath Proof Explorer

Theorem metustss

Description: Range of the elements of the filter base generated by the metric D . (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 metustss 
|- ( ( D e. ( PsMet ` X ) /\ A e. F ) -> A C_ ( X X. X ) )

Proof

Step Hyp Ref Expression
1 metust.1 
 |-  F = ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) )
2 cnvimass 
 |-  ( `' D " ( 0 [,) a ) ) C_ dom D
3 psmetf 
 |-  ( D e. ( PsMet ` X ) -> D : ( X X. X ) --> RR* )
4 2 3 fssdm 
 |-  ( D e. ( PsMet ` X ) -> ( `' D " ( 0 [,) a ) ) C_ ( X X. X ) )
5 4 ad2antrr 
 |-  ( ( ( D e. ( PsMet ` X ) /\ A e. F ) /\ a e. RR+ ) -> ( `' D " ( 0 [,) a ) ) C_ ( X X. X ) )
6 cnvexg 
 |-  ( D e. ( PsMet ` X ) -> `' D e. _V )
7 imaexg 
 |-  ( `' D e. _V -> ( `' D " ( 0 [,) a ) ) e. _V )
8 elpwg 
 |-  ( ( `' D " ( 0 [,) a ) ) e. _V -> ( ( `' D " ( 0 [,) a ) ) e. ~P ( X X. X ) <-> ( `' D " ( 0 [,) a ) ) C_ ( X X. X ) ) )
9 6 7 8 3syl 
 |-  ( D e. ( PsMet ` X ) -> ( ( `' D " ( 0 [,) a ) ) e. ~P ( X X. X ) <-> ( `' D " ( 0 [,) a ) ) C_ ( X X. X ) ) )
10 9 ad2antrr 
 |-  ( ( ( D e. ( PsMet ` X ) /\ A e. F ) /\ a e. RR+ ) -> ( ( `' D " ( 0 [,) a ) ) e. ~P ( X X. X ) <-> ( `' D " ( 0 [,) a ) ) C_ ( X X. X ) ) )
11 5 10 mpbird 
 |-  ( ( ( D e. ( PsMet ` X ) /\ A e. F ) /\ a e. RR+ ) -> ( `' D " ( 0 [,) a ) ) e. ~P ( X X. X ) )
12 11 ralrimiva 
 |-  ( ( D e. ( PsMet ` X ) /\ A e. F ) -> A. a e. RR+ ( `' D " ( 0 [,) a ) ) e. ~P ( X X. X ) )
13 eqid 
 |-  ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) = ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) )
14 13 rnmptss 
 |-  ( A. a e. RR+ ( `' D " ( 0 [,) a ) ) e. ~P ( X X. X ) -> ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) C_ ~P ( X X. X ) )
15 12 14 syl 
 |-  ( ( D e. ( PsMet ` X ) /\ A e. F ) -> ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) C_ ~P ( X X. X ) )
16 1 15 eqsstrid 
 |-  ( ( D e. ( PsMet ` X ) /\ A e. F ) -> F C_ ~P ( X X. X ) )
17 simpr 
 |-  ( ( D e. ( PsMet ` X ) /\ A e. F ) -> A e. F )
18 16 17 sseldd 
 |-  ( ( D e. ( PsMet ` X ) /\ A e. F ) -> A e. ~P ( X X. X ) )
19 18 elpwid 
 |-  ( ( D e. ( PsMet ` X ) /\ A e. F ) -> A C_ ( X X. X ) )