Description: Elements of the filter base generated by the metric D are relations. (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 | metustrel | |- ( ( D e. ( PsMet ` X ) /\ A e. F ) -> Rel A ) |
| 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 | xpss | |- ( X X. X ) C_ ( _V X. _V ) |
|
| 4 | 2 3 | sstrdi | |- ( ( D e. ( PsMet ` X ) /\ A e. F ) -> A C_ ( _V X. _V ) ) |
| 5 | df-rel | |- ( Rel A <-> A C_ ( _V X. _V ) ) |
|
| 6 | 4 5 | sylibr | |- ( ( D e. ( PsMet ` X ) /\ A e. F ) -> Rel A ) |