Description: The ball around a point P , alternative definition. (Contributed by Thierry Arnoux, 7-Dec-2017) (Revised by Thierry Arnoux, 11-Mar-2018)
Ref | Expression | ||
---|---|---|---|
Assertion | blval2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rpxr | |
|
2 | blvalps | |
|
3 | 1 2 | syl3an3 | |
4 | nfv | |
|
5 | nfcv | |
|
6 | nfrab1 | |
|
7 | psmetf | |
|
8 | ffn | |
|
9 | elpreima | |
|
10 | 7 8 9 | 3syl | |
11 | 10 | 3ad2ant1 | |
12 | opelxp | |
|
13 | 12 | baib | |
14 | 13 | 3ad2ant2 | |
15 | 14 | biimpd | |
16 | 15 | adantrd | |
17 | simprl | |
|
18 | 17 | ex | |
19 | simpl2 | |
|
20 | 19 13 | syl | |
21 | df-ov | |
|
22 | 21 | eleq1i | |
23 | 0xr | |
|
24 | simpl3 | |
|
25 | 24 | rpxrd | |
26 | elico1 | |
|
27 | 23 25 26 | sylancr | |
28 | df-3an | |
|
29 | simpl1 | |
|
30 | simpr | |
|
31 | psmetcl | |
|
32 | 29 19 30 31 | syl3anc | |
33 | psmetge0 | |
|
34 | 29 19 30 33 | syl3anc | |
35 | 32 34 | jca | |
36 | 35 | biantrurd | |
37 | 28 36 | bitr4id | |
38 | 27 37 | bitrd | |
39 | 22 38 | bitr3id | |
40 | 20 39 | anbi12d | |
41 | 40 | ex | |
42 | 16 18 41 | pm5.21ndd | |
43 | 11 42 | bitrd | |
44 | elimasng | |
|
45 | 44 | elvd | |
46 | 45 | 3ad2ant2 | |
47 | rabid | |
|
48 | 47 | a1i | |
49 | 43 46 48 | 3bitr4d | |
50 | 4 5 6 49 | eqrd | |
51 | 3 50 | eqtr4d | |