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 ( 𝐴 ∈ ( topGen β€˜ ran (,) ) ↔ ( 𝐴 βŠ† ℝ ∧ βˆ€ π‘₯ ∈ 𝐴 βˆ€ 𝑦 ∈ ℝ+ βˆƒ 𝑧 ∈ ℝ+ ( 𝑧 ≀ 𝑦 ∧ ( ( π‘₯ βˆ’ 𝑧 ) (,) ( π‘₯ + 𝑧 ) ) βŠ† 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 eqid ⊒ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) = ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) )
2 1 rexmet ⊒ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ∈ ( ∞Met β€˜ ℝ )
3 eqid ⊒ ( MetOpen β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) = ( MetOpen β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) )
4 1 3 tgioo ⊒ ( topGen β€˜ ran (,) ) = ( MetOpen β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) )
5 4 mopnss ⊒ ( ( ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ∈ ( ∞Met β€˜ ℝ ) ∧ 𝐴 ∈ ( topGen β€˜ ran (,) ) ) β†’ 𝐴 βŠ† ℝ )
6 2 5 mpan ⊒ ( 𝐴 ∈ ( topGen β€˜ ran (,) ) β†’ 𝐴 βŠ† ℝ )
7 4 mopni3 ⊒ ( ( ( ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ∈ ( ∞Met β€˜ ℝ ) ∧ 𝐴 ∈ ( topGen β€˜ ran (,) ) ∧ π‘₯ ∈ 𝐴 ) ∧ 𝑦 ∈ ℝ+ ) β†’ βˆƒ 𝑧 ∈ ℝ+ ( 𝑧 < 𝑦 ∧ ( π‘₯ ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) 𝑧 ) βŠ† 𝐴 ) )
8 7 ex ⊒ ( ( ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ∈ ( ∞Met β€˜ ℝ ) ∧ 𝐴 ∈ ( topGen β€˜ ran (,) ) ∧ π‘₯ ∈ 𝐴 ) β†’ ( 𝑦 ∈ ℝ+ β†’ βˆƒ 𝑧 ∈ ℝ+ ( 𝑧 < 𝑦 ∧ ( π‘₯ ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) 𝑧 ) βŠ† 𝐴 ) ) )
9 2 8 mp3an1 ⊒ ( ( 𝐴 ∈ ( topGen β€˜ ran (,) ) ∧ π‘₯ ∈ 𝐴 ) β†’ ( 𝑦 ∈ ℝ+ β†’ βˆƒ 𝑧 ∈ ℝ+ ( 𝑧 < 𝑦 ∧ ( π‘₯ ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) 𝑧 ) βŠ† 𝐴 ) ) )
10 6 sselda ⊒ ( ( 𝐴 ∈ ( topGen β€˜ ran (,) ) ∧ π‘₯ ∈ 𝐴 ) β†’ π‘₯ ∈ ℝ )
11 rpre ⊒ ( 𝑧 ∈ ℝ+ β†’ 𝑧 ∈ ℝ )
12 1 bl2ioo ⊒ ( ( π‘₯ ∈ ℝ ∧ 𝑧 ∈ ℝ ) β†’ ( π‘₯ ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) 𝑧 ) = ( ( π‘₯ βˆ’ 𝑧 ) (,) ( π‘₯ + 𝑧 ) ) )
13 11 12 sylan2 ⊒ ( ( π‘₯ ∈ ℝ ∧ 𝑧 ∈ ℝ+ ) β†’ ( π‘₯ ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) 𝑧 ) = ( ( π‘₯ βˆ’ 𝑧 ) (,) ( π‘₯ + 𝑧 ) ) )
14 13 sseq1d ⊒ ( ( π‘₯ ∈ ℝ ∧ 𝑧 ∈ ℝ+ ) β†’ ( ( π‘₯ ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) 𝑧 ) βŠ† 𝐴 ↔ ( ( π‘₯ βˆ’ 𝑧 ) (,) ( π‘₯ + 𝑧 ) ) βŠ† 𝐴 ) )
15 14 anbi2d ⊒ ( ( π‘₯ ∈ ℝ ∧ 𝑧 ∈ ℝ+ ) β†’ ( ( 𝑧 < 𝑦 ∧ ( π‘₯ ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) 𝑧 ) βŠ† 𝐴 ) ↔ ( 𝑧 < 𝑦 ∧ ( ( π‘₯ βˆ’ 𝑧 ) (,) ( π‘₯ + 𝑧 ) ) βŠ† 𝐴 ) ) )
16 15 rexbidva ⊒ ( π‘₯ ∈ ℝ β†’ ( βˆƒ 𝑧 ∈ ℝ+ ( 𝑧 < 𝑦 ∧ ( π‘₯ ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) 𝑧 ) βŠ† 𝐴 ) ↔ βˆƒ 𝑧 ∈ ℝ+ ( 𝑧 < 𝑦 ∧ ( ( π‘₯ βˆ’ 𝑧 ) (,) ( π‘₯ + 𝑧 ) ) βŠ† 𝐴 ) ) )
17 16 biimpd ⊒ ( π‘₯ ∈ ℝ β†’ ( βˆƒ 𝑧 ∈ ℝ+ ( 𝑧 < 𝑦 ∧ ( π‘₯ ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) 𝑧 ) βŠ† 𝐴 ) β†’ βˆƒ 𝑧 ∈ ℝ+ ( 𝑧 < 𝑦 ∧ ( ( π‘₯ βˆ’ 𝑧 ) (,) ( π‘₯ + 𝑧 ) ) βŠ† 𝐴 ) ) )
18 rpre ⊒ ( 𝑦 ∈ ℝ+ β†’ 𝑦 ∈ ℝ )
19 ltle ⊒ ( ( 𝑧 ∈ ℝ ∧ 𝑦 ∈ ℝ ) β†’ ( 𝑧 < 𝑦 β†’ 𝑧 ≀ 𝑦 ) )
20 11 18 19 syl2anr ⊒ ( ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) β†’ ( 𝑧 < 𝑦 β†’ 𝑧 ≀ 𝑦 ) )
21 20 anim1d ⊒ ( ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) β†’ ( ( 𝑧 < 𝑦 ∧ ( ( π‘₯ βˆ’ 𝑧 ) (,) ( π‘₯ + 𝑧 ) ) βŠ† 𝐴 ) β†’ ( 𝑧 ≀ 𝑦 ∧ ( ( π‘₯ βˆ’ 𝑧 ) (,) ( π‘₯ + 𝑧 ) ) βŠ† 𝐴 ) ) )
22 21 reximdva ⊒ ( 𝑦 ∈ ℝ+ β†’ ( βˆƒ 𝑧 ∈ ℝ+ ( 𝑧 < 𝑦 ∧ ( ( π‘₯ βˆ’ 𝑧 ) (,) ( π‘₯ + 𝑧 ) ) βŠ† 𝐴 ) β†’ βˆƒ 𝑧 ∈ ℝ+ ( 𝑧 ≀ 𝑦 ∧ ( ( π‘₯ βˆ’ 𝑧 ) (,) ( π‘₯ + 𝑧 ) ) βŠ† 𝐴 ) ) )
23 17 22 syl9 ⊒ ( π‘₯ ∈ ℝ β†’ ( 𝑦 ∈ ℝ+ β†’ ( βˆƒ 𝑧 ∈ ℝ+ ( 𝑧 < 𝑦 ∧ ( π‘₯ ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) 𝑧 ) βŠ† 𝐴 ) β†’ βˆƒ 𝑧 ∈ ℝ+ ( 𝑧 ≀ 𝑦 ∧ ( ( π‘₯ βˆ’ 𝑧 ) (,) ( π‘₯ + 𝑧 ) ) βŠ† 𝐴 ) ) ) )
24 10 23 syl ⊒ ( ( 𝐴 ∈ ( topGen β€˜ ran (,) ) ∧ π‘₯ ∈ 𝐴 ) β†’ ( 𝑦 ∈ ℝ+ β†’ ( βˆƒ 𝑧 ∈ ℝ+ ( 𝑧 < 𝑦 ∧ ( π‘₯ ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) 𝑧 ) βŠ† 𝐴 ) β†’ βˆƒ 𝑧 ∈ ℝ+ ( 𝑧 ≀ 𝑦 ∧ ( ( π‘₯ βˆ’ 𝑧 ) (,) ( π‘₯ + 𝑧 ) ) βŠ† 𝐴 ) ) ) )
25 9 24 mpdd ⊒ ( ( 𝐴 ∈ ( topGen β€˜ ran (,) ) ∧ π‘₯ ∈ 𝐴 ) β†’ ( 𝑦 ∈ ℝ+ β†’ βˆƒ 𝑧 ∈ ℝ+ ( 𝑧 ≀ 𝑦 ∧ ( ( π‘₯ βˆ’ 𝑧 ) (,) ( π‘₯ + 𝑧 ) ) βŠ† 𝐴 ) ) )
26 25 expimpd ⊒ ( 𝐴 ∈ ( topGen β€˜ ran (,) ) β†’ ( ( π‘₯ ∈ 𝐴 ∧ 𝑦 ∈ ℝ+ ) β†’ βˆƒ 𝑧 ∈ ℝ+ ( 𝑧 ≀ 𝑦 ∧ ( ( π‘₯ βˆ’ 𝑧 ) (,) ( π‘₯ + 𝑧 ) ) βŠ† 𝐴 ) ) )
27 26 ralrimivv ⊒ ( 𝐴 ∈ ( topGen β€˜ ran (,) ) β†’ βˆ€ π‘₯ ∈ 𝐴 βˆ€ 𝑦 ∈ ℝ+ βˆƒ 𝑧 ∈ ℝ+ ( 𝑧 ≀ 𝑦 ∧ ( ( π‘₯ βˆ’ 𝑧 ) (,) ( π‘₯ + 𝑧 ) ) βŠ† 𝐴 ) )
28 6 27 jca ⊒ ( 𝐴 ∈ ( topGen β€˜ ran (,) ) β†’ ( 𝐴 βŠ† ℝ ∧ βˆ€ π‘₯ ∈ 𝐴 βˆ€ 𝑦 ∈ ℝ+ βˆƒ 𝑧 ∈ ℝ+ ( 𝑧 ≀ 𝑦 ∧ ( ( π‘₯ βˆ’ 𝑧 ) (,) ( π‘₯ + 𝑧 ) ) βŠ† 𝐴 ) ) )
29 ssel2 ⊒ ( ( 𝐴 βŠ† ℝ ∧ π‘₯ ∈ 𝐴 ) β†’ π‘₯ ∈ ℝ )
30 1rp ⊒ 1 ∈ ℝ+
31 simpr ⊒ ( ( 𝑧 ≀ 𝑦 ∧ ( ( π‘₯ βˆ’ 𝑧 ) (,) ( π‘₯ + 𝑧 ) ) βŠ† 𝐴 ) β†’ ( ( π‘₯ βˆ’ 𝑧 ) (,) ( π‘₯ + 𝑧 ) ) βŠ† 𝐴 )
32 31 reximi ⊒ ( βˆƒ 𝑧 ∈ ℝ+ ( 𝑧 ≀ 𝑦 ∧ ( ( π‘₯ βˆ’ 𝑧 ) (,) ( π‘₯ + 𝑧 ) ) βŠ† 𝐴 ) β†’ βˆƒ 𝑧 ∈ ℝ+ ( ( π‘₯ βˆ’ 𝑧 ) (,) ( π‘₯ + 𝑧 ) ) βŠ† 𝐴 )
33 32 ralimi ⊒ ( βˆ€ 𝑦 ∈ ℝ+ βˆƒ 𝑧 ∈ ℝ+ ( 𝑧 ≀ 𝑦 ∧ ( ( π‘₯ βˆ’ 𝑧 ) (,) ( π‘₯ + 𝑧 ) ) βŠ† 𝐴 ) β†’ βˆ€ 𝑦 ∈ ℝ+ βˆƒ 𝑧 ∈ ℝ+ ( ( π‘₯ βˆ’ 𝑧 ) (,) ( π‘₯ + 𝑧 ) ) βŠ† 𝐴 )
34 biidd ⊒ ( 𝑦 = 1 β†’ ( βˆƒ 𝑧 ∈ ℝ+ ( ( π‘₯ βˆ’ 𝑧 ) (,) ( π‘₯ + 𝑧 ) ) βŠ† 𝐴 ↔ βˆƒ 𝑧 ∈ ℝ+ ( ( π‘₯ βˆ’ 𝑧 ) (,) ( π‘₯ + 𝑧 ) ) βŠ† 𝐴 ) )
35 34 rspcv ⊒ ( 1 ∈ ℝ+ β†’ ( βˆ€ 𝑦 ∈ ℝ+ βˆƒ 𝑧 ∈ ℝ+ ( ( π‘₯ βˆ’ 𝑧 ) (,) ( π‘₯ + 𝑧 ) ) βŠ† 𝐴 β†’ βˆƒ 𝑧 ∈ ℝ+ ( ( π‘₯ βˆ’ 𝑧 ) (,) ( π‘₯ + 𝑧 ) ) βŠ† 𝐴 ) )
36 30 33 35 mpsyl ⊒ ( βˆ€ 𝑦 ∈ ℝ+ βˆƒ 𝑧 ∈ ℝ+ ( 𝑧 ≀ 𝑦 ∧ ( ( π‘₯ βˆ’ 𝑧 ) (,) ( π‘₯ + 𝑧 ) ) βŠ† 𝐴 ) β†’ βˆƒ 𝑧 ∈ ℝ+ ( ( π‘₯ βˆ’ 𝑧 ) (,) ( π‘₯ + 𝑧 ) ) βŠ† 𝐴 )
37 14 rexbidva ⊒ ( π‘₯ ∈ ℝ β†’ ( βˆƒ 𝑧 ∈ ℝ+ ( π‘₯ ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) 𝑧 ) βŠ† 𝐴 ↔ βˆƒ 𝑧 ∈ ℝ+ ( ( π‘₯ βˆ’ 𝑧 ) (,) ( π‘₯ + 𝑧 ) ) βŠ† 𝐴 ) )
38 36 37 imbitrrid ⊒ ( π‘₯ ∈ ℝ β†’ ( βˆ€ 𝑦 ∈ ℝ+ βˆƒ 𝑧 ∈ ℝ+ ( 𝑧 ≀ 𝑦 ∧ ( ( π‘₯ βˆ’ 𝑧 ) (,) ( π‘₯ + 𝑧 ) ) βŠ† 𝐴 ) β†’ βˆƒ 𝑧 ∈ ℝ+ ( π‘₯ ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) 𝑧 ) βŠ† 𝐴 ) )
39 29 38 syl ⊒ ( ( 𝐴 βŠ† ℝ ∧ π‘₯ ∈ 𝐴 ) β†’ ( βˆ€ 𝑦 ∈ ℝ+ βˆƒ 𝑧 ∈ ℝ+ ( 𝑧 ≀ 𝑦 ∧ ( ( π‘₯ βˆ’ 𝑧 ) (,) ( π‘₯ + 𝑧 ) ) βŠ† 𝐴 ) β†’ βˆƒ 𝑧 ∈ ℝ+ ( π‘₯ ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) 𝑧 ) βŠ† 𝐴 ) )
40 39 ralimdva ⊒ ( 𝐴 βŠ† ℝ β†’ ( βˆ€ π‘₯ ∈ 𝐴 βˆ€ 𝑦 ∈ ℝ+ βˆƒ 𝑧 ∈ ℝ+ ( 𝑧 ≀ 𝑦 ∧ ( ( π‘₯ βˆ’ 𝑧 ) (,) ( π‘₯ + 𝑧 ) ) βŠ† 𝐴 ) β†’ βˆ€ π‘₯ ∈ 𝐴 βˆƒ 𝑧 ∈ ℝ+ ( π‘₯ ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) 𝑧 ) βŠ† 𝐴 ) )
41 40 imdistani ⊒ ( ( 𝐴 βŠ† ℝ ∧ βˆ€ π‘₯ ∈ 𝐴 βˆ€ 𝑦 ∈ ℝ+ βˆƒ 𝑧 ∈ ℝ+ ( 𝑧 ≀ 𝑦 ∧ ( ( π‘₯ βˆ’ 𝑧 ) (,) ( π‘₯ + 𝑧 ) ) βŠ† 𝐴 ) ) β†’ ( 𝐴 βŠ† ℝ ∧ βˆ€ π‘₯ ∈ 𝐴 βˆƒ 𝑧 ∈ ℝ+ ( π‘₯ ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) 𝑧 ) βŠ† 𝐴 ) )
42 4 elmopn2 ⊒ ( ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ∈ ( ∞Met β€˜ ℝ ) β†’ ( 𝐴 ∈ ( topGen β€˜ ran (,) ) ↔ ( 𝐴 βŠ† ℝ ∧ βˆ€ π‘₯ ∈ 𝐴 βˆƒ 𝑧 ∈ ℝ+ ( π‘₯ ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) 𝑧 ) βŠ† 𝐴 ) ) )
43 2 42 ax-mp ⊒ ( 𝐴 ∈ ( topGen β€˜ ran (,) ) ↔ ( 𝐴 βŠ† ℝ ∧ βˆ€ π‘₯ ∈ 𝐴 βˆƒ 𝑧 ∈ ℝ+ ( π‘₯ ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) 𝑧 ) βŠ† 𝐴 ) )
44 41 43 sylibr ⊒ ( ( 𝐴 βŠ† ℝ ∧ βˆ€ π‘₯ ∈ 𝐴 βˆ€ 𝑦 ∈ ℝ+ βˆƒ 𝑧 ∈ ℝ+ ( 𝑧 ≀ 𝑦 ∧ ( ( π‘₯ βˆ’ 𝑧 ) (,) ( π‘₯ + 𝑧 ) ) βŠ† 𝐴 ) ) β†’ 𝐴 ∈ ( topGen β€˜ ran (,) ) )
45 28 44 impbii ⊒ ( 𝐴 ∈ ( topGen β€˜ ran (,) ) ↔ ( 𝐴 βŠ† ℝ ∧ βˆ€ π‘₯ ∈ 𝐴 βˆ€ 𝑦 ∈ ℝ+ βˆƒ 𝑧 ∈ ℝ+ ( 𝑧 ≀ 𝑦 ∧ ( ( π‘₯ βˆ’ 𝑧 ) (,) ( π‘₯ + 𝑧 ) ) βŠ† 𝐴 ) ) )