Description: Express the predicate " <. X , D >. is an extended metric space" with underlying set X and distance function D . (Contributed by Mario Carneiro, 2-Sep-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | isms.j | |
|
isms.x | |
||
isms.d | |
||
Assertion | isxms2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | isms.j | |
|
2 | isms.x | |
|
3 | isms.d | |
|
4 | 1 2 3 | isxms | |
5 | 2 1 | istps | |
6 | df-mopn | |
|
7 | 6 | dmmptss | |
8 | toponmax | |
|
9 | 8 | adantl | |
10 | simpl | |
|
11 | 9 10 | eleqtrd | |
12 | elfvdm | |
|
13 | 11 12 | syl | |
14 | 7 13 | sselid | |
15 | xmetunirn | |
|
16 | 14 15 | sylib | |
17 | eqid | |
|
18 | 17 | mopntopon | |
19 | 16 18 | syl | |
20 | 10 19 | eqeltrd | |
21 | toponuni | |
|
22 | 20 21 | syl | |
23 | toponuni | |
|
24 | 23 | adantl | |
25 | 22 24 | eqtr4d | |
26 | 25 | fveq2d | |
27 | 16 26 | eleqtrd | |
28 | 27 | ex | |
29 | 17 | mopntopon | |
30 | eleq1 | |
|
31 | 29 30 | syl5ibr | |
32 | 28 31 | impbid | |
33 | 5 32 | syl5bb | |
34 | 33 | pm5.32ri | |
35 | 4 34 | bitri | |