Metamath Proof Explorer


Theorem opnrebl

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

Ref Expression
Assertion opnrebl A topGen ran . A x A y + x y x + y 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 elmopn2 abs 2 ∞Met A topGen ran . A x A y + x ball abs 2 y A
6 2 5 ax-mp A topGen ran . A x A y + x ball abs 2 y A
7 ssel2 A x A x
8 rpre y + y
9 1 bl2ioo x y x ball abs 2 y = x y x + y
10 8 9 sylan2 x y + x ball abs 2 y = x y x + y
11 10 sseq1d x y + x ball abs 2 y A x y x + y A
12 11 rexbidva x y + x ball abs 2 y A y + x y x + y A
13 7 12 syl A x A y + x ball abs 2 y A y + x y x + y A
14 13 ralbidva A x A y + x ball abs 2 y A x A y + x y x + y A
15 14 pm5.32i A x A y + x ball abs 2 y A A x A y + x y x + y A
16 6 15 bitri A topGen ran . A x A y + x y x + y A