Description: Restriction of a pseudometric. (Contributed by Thierry Arnoux, 11-Feb-2018)
Ref | Expression | ||
---|---|---|---|
Assertion | psmetres2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | psmetf | |
|
2 | 1 | adantr | |
3 | simpr | |
|
4 | xpss12 | |
|
5 | 3 3 4 | syl2anc | |
6 | 2 5 | fssresd | |
7 | simpr | |
|
8 | 7 7 | ovresd | |
9 | simpll | |
|
10 | 3 | sselda | |
11 | psmet0 | |
|
12 | 9 10 11 | syl2anc | |
13 | 8 12 | eqtrd | |
14 | 9 | ad2antrr | |
15 | 3 | ad2antrr | |
16 | 15 | sselda | |
17 | 10 | ad2antrr | |
18 | 3 | adantr | |
19 | 18 | sselda | |
20 | 19 | adantr | |
21 | psmettri2 | |
|
22 | 14 16 17 20 21 | syl13anc | |
23 | 7 | adantr | |
24 | simpr | |
|
25 | 23 24 | ovresd | |
26 | 25 | adantr | |
27 | simpr | |
|
28 | 7 | ad2antrr | |
29 | 27 28 | ovresd | |
30 | 24 | adantr | |
31 | 27 30 | ovresd | |
32 | 29 31 | oveq12d | |
33 | 22 26 32 | 3brtr4d | |
34 | 33 | ralrimiva | |
35 | 34 | ralrimiva | |
36 | 13 35 | jca | |
37 | 36 | ralrimiva | |
38 | elfvex | |
|
39 | 38 | adantr | |
40 | 39 3 | ssexd | |
41 | ispsmet | |
|
42 | 40 41 | syl | |
43 | 6 37 42 | mpbir2and | |