Metamath Proof Explorer


Theorem opnrebl2

Description: A set is open in the standard topology of the reals precisely when every point can be enclosed in an arbitrarily small ball. (Contributed by Jeff Hankins, 22-Sep-2013) (Proof shortened by Mario Carneiro, 30-Jan-2014)

Ref Expression
Assertion opnrebl2 A topGen ran . A x A y + z + z y x z x + z A

Proof

Step Hyp Ref Expression
1 eqid abs 2 = abs 2
2 1 rexmet abs 2 ∞Met
3 eqid MetOpen abs 2 = MetOpen abs 2
4 1 3 tgioo topGen ran . = MetOpen abs 2
5 4 mopnss abs 2 ∞Met A topGen ran . A
6 2 5 mpan A topGen ran . A
7 4 mopni3 abs 2 ∞Met A topGen ran . x A y + z + z < y x ball abs 2 z A
8 7 ex abs 2 ∞Met A topGen ran . x A y + z + z < y x ball abs 2 z A
9 2 8 mp3an1 A topGen ran . x A y + z + z < y x ball abs 2 z A
10 6 sselda A topGen ran . x A x
11 rpre z + z
12 1 bl2ioo x z x ball abs 2 z = x z x + z
13 11 12 sylan2 x z + x ball abs 2 z = x z x + z
14 13 sseq1d x z + x ball abs 2 z A x z x + z A
15 14 anbi2d x z + z < y x ball abs 2 z A z < y x z x + z A
16 15 rexbidva x z + z < y x ball abs 2 z A z + z < y x z x + z A
17 16 biimpd x z + z < y x ball abs 2 z A z + z < y x z x + z A
18 rpre y + y
19 ltle z y z < y z y
20 11 18 19 syl2anr y + z + z < y z y
21 20 anim1d y + z + z < y x z x + z A z y x z x + z A
22 21 reximdva y + z + z < y x z x + z A z + z y x z x + z A
23 17 22 syl9 x y + z + z < y x ball abs 2 z A z + z y x z x + z A
24 10 23 syl A topGen ran . x A y + z + z < y x ball abs 2 z A z + z y x z x + z A
25 9 24 mpdd A topGen ran . x A y + z + z y x z x + z A
26 25 expimpd A topGen ran . x A y + z + z y x z x + z A
27 26 ralrimivv A topGen ran . x A y + z + z y x z x + z A
28 6 27 jca A topGen ran . A x A y + z + z y x z x + z A
29 ssel2 A x A x
30 1rp 1 +
31 simpr z y x z x + z A x z x + z A
32 31 reximi z + z y x z x + z A z + x z x + z A
33 32 ralimi y + z + z y x z x + z A y + z + x z x + z A
34 biidd y = 1 z + x z x + z A z + x z x + z A
35 34 rspcv 1 + y + z + x z x + z A z + x z x + z A
36 30 33 35 mpsyl y + z + z y x z x + z A z + x z x + z A
37 14 rexbidva x z + x ball abs 2 z A z + x z x + z A
38 36 37 syl5ibr x y + z + z y x z x + z A z + x ball abs 2 z A
39 29 38 syl A x A y + z + z y x z x + z A z + x ball abs 2 z A
40 39 ralimdva A x A y + z + z y x z x + z A x A z + x ball abs 2 z A
41 40 imdistani A x A y + z + z y x z x + z A A x A z + x ball abs 2 z A
42 4 elmopn2 abs 2 ∞Met A topGen ran . A x A z + x ball abs 2 z A
43 2 42 ax-mp A topGen ran . A x A z + x ball abs 2 z A
44 41 43 sylibr A x A y + z + z y x z x + z A A topGen ran .
45 28 44 impbii A topGen ran . A x A y + z + z y x z x + z A