Description: The "section" image of an entourage at a point P always contains a ball (centered on this point). (Contributed by Thierry Arnoux, 8-Dec-2017)
Ref | Expression | ||
---|---|---|---|
Assertion | metustbl | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp1 | |
|
2 | simp3 | |
|
3 | simpr | |
|
4 | eqid | |
|
5 | 4 | elrnmpt | |
6 | 5 | elv | |
7 | 6 | biimpi | |
8 | 7 | ad2antlr | |
9 | sseq1 | |
|
10 | 9 | biimpcd | |
11 | 10 | reximdv | |
12 | 3 8 11 | sylc | |
13 | 2 | ne0d | |
14 | simp2 | |
|
15 | metuel | |
|
16 | 15 | simplbda | |
17 | 13 1 14 16 | syl21anc | |
18 | 12 17 | r19.29a | |
19 | imass1 | |
|
20 | 19 | reximi | |
21 | blval2 | |
|
22 | 21 | sseq1d | |
23 | 22 | 3expa | |
24 | 23 | rexbidva | |
25 | 20 24 | imbitrrid | |
26 | 25 | imp | |
27 | 1 2 18 26 | syl21anc | |
28 | blssexps | |
|
29 | 28 | 3adant2 | |
30 | 27 29 | mpbird | |