Metamath Proof Explorer

Theorem tgioo

Description: The topology generated by open intervals of reals is the same as the open sets of the standard metric space on the reals. (Contributed by NM, 7-May-2007) (Revised by Mario Carneiro, 13-Nov-2013)

Ref Expression
Hypotheses remet.1 ⊢ 𝐷 = ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) )
tgioo.2 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
Assertion tgioo ( topGen ‘ ran (,) ) = 𝐽

Proof

Step Hyp Ref Expression
1 remet.1 ⊢ 𝐷 = ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) )
2 tgioo.2 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
3 1 rexmet ⊢ 𝐷 ∈ ( ∞Met ‘ ℝ )
4 2 mopnval ⊢ ( 𝐷 ∈ ( ∞Met ‘ ℝ ) → 𝐽 = ( topGen ‘ ran ( ball ‘ 𝐷 ) ) )
5 3 4 ax-mp ⊢ 𝐽 = ( topGen ‘ ran ( ball ‘ 𝐷 ) )
6 1 blssioo ⊢ ran ( ball ‘ 𝐷 ) ⊆ ran (,)
7 elssuni ⊢ ( 𝑣 ∈ ran (,) → 𝑣 ⊆ ∪ ran (,) )
8 unirnioo ⊢ ℝ = ∪ ran (,)
9 7 8 sseqtrrdi ⊢ ( 𝑣 ∈ ran (,) → 𝑣 ⊆ ℝ )
10 retopbas ⊢ ran (,) ∈ TopBases
11 10 a1i ⊢ ( ( 𝑣 ∈ ran (,) ∧ 𝑥 ∈ 𝑣 ) → ran (,) ∈ TopBases )
12 simpl ⊢ ( ( 𝑣 ∈ ran (,) ∧ 𝑥 ∈ 𝑣 ) → 𝑣 ∈ ran (,) )
13 9 sselda ⊢ ( ( 𝑣 ∈ ran (,) ∧ 𝑥 ∈ 𝑣 ) → 𝑥 ∈ ℝ )
14 1re ⊢ 1 ∈ ℝ
15 1 bl2ioo ⊢ ( ( 𝑥 ∈ ℝ ∧ 1 ∈ ℝ ) → ( 𝑥 ( ball ‘ 𝐷 ) 1 ) = ( ( 𝑥 − 1 ) (,) ( 𝑥 + 1 ) ) )
16 14 15 mpan2 ⊢ ( 𝑥 ∈ ℝ → ( 𝑥 ( ball ‘ 𝐷 ) 1 ) = ( ( 𝑥 − 1 ) (,) ( 𝑥 + 1 ) ) )
17 ioof ⊢ (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ
18 ffn ⊢ ( (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ → (,) Fn ( ℝ* × ℝ* ) )
19 17 18 ax-mp ⊢ (,) Fn ( ℝ* × ℝ* )
20 peano2rem ⊢ ( 𝑥 ∈ ℝ → ( 𝑥 − 1 ) ∈ ℝ )
21 20 rexrd ⊢ ( 𝑥 ∈ ℝ → ( 𝑥 − 1 ) ∈ ℝ* )
22 peano2re ⊢ ( 𝑥 ∈ ℝ → ( 𝑥 + 1 ) ∈ ℝ )
23 22 rexrd ⊢ ( 𝑥 ∈ ℝ → ( 𝑥 + 1 ) ∈ ℝ* )
24 fnovrn ⊢ ( ( (,) Fn ( ℝ* × ℝ* ) ∧ ( 𝑥 − 1 ) ∈ ℝ* ∧ ( 𝑥 + 1 ) ∈ ℝ* ) → ( ( 𝑥 − 1 ) (,) ( 𝑥 + 1 ) ) ∈ ran (,) )
25 19 21 23 24 mp3an2i ⊢ ( 𝑥 ∈ ℝ → ( ( 𝑥 − 1 ) (,) ( 𝑥 + 1 ) ) ∈ ran (,) )
26 16 25 eqeltrd ⊢ ( 𝑥 ∈ ℝ → ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ∈ ran (,) )
27 13 26 syl ⊢ ( ( 𝑣 ∈ ran (,) ∧ 𝑥 ∈ 𝑣 ) → ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ∈ ran (,) )
28 simpr ⊢ ( ( 𝑣 ∈ ran (,) ∧ 𝑥 ∈ 𝑣 ) → 𝑥 ∈ 𝑣 )
29 1rp ⊢ 1 ∈ ℝ+
30 blcntr ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ ℝ ) ∧ 𝑥 ∈ ℝ ∧ 1 ∈ ℝ+ ) → 𝑥 ∈ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) )
31 3 29 30 mp3an13 ⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) )
32 13 31 syl ⊢ ( ( 𝑣 ∈ ran (,) ∧ 𝑥 ∈ 𝑣 ) → 𝑥 ∈ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) )
33 28 32 elind ⊢ ( ( 𝑣 ∈ ran (,) ∧ 𝑥 ∈ 𝑣 ) → 𝑥 ∈ ( 𝑣 ∩ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ) )
34 basis2 ⊢ ( ( ( ran (,) ∈ TopBases ∧ 𝑣 ∈ ran (,) ) ∧ ( ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ∈ ran (,) ∧ 𝑥 ∈ ( 𝑣 ∩ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ) ) ) → ∃ 𝑧 ∈ ran (,) ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ ( 𝑣 ∩ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ) ) )
35 11 12 27 33 34 syl22anc ⊢ ( ( 𝑣 ∈ ran (,) ∧ 𝑥 ∈ 𝑣 ) → ∃ 𝑧 ∈ ran (,) ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ ( 𝑣 ∩ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ) ) )
36 ovelrn ⊢ ( (,) Fn ( ℝ* × ℝ* ) → ( 𝑧 ∈ ran (,) ↔ ∃ 𝑎 ∈ ℝ* ∃ 𝑏 ∈ ℝ* 𝑧 = ( 𝑎 (,) 𝑏 ) ) )
37 19 36 ax-mp ⊢ ( 𝑧 ∈ ran (,) ↔ ∃ 𝑎 ∈ ℝ* ∃ 𝑏 ∈ ℝ* 𝑧 = ( 𝑎 (,) 𝑏 ) )
38 eleq2 ⊢ ( 𝑧 = ( 𝑎 (,) 𝑏 ) → ( 𝑥 ∈ 𝑧 ↔ 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ) )
39 sseq1 ⊢ ( 𝑧 = ( 𝑎 (,) 𝑏 ) → ( 𝑧 ⊆ ( 𝑣 ∩ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ) ↔ ( 𝑎 (,) 𝑏 ) ⊆ ( 𝑣 ∩ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ) ) )
40 38 39 anbi12d ⊢ ( 𝑧 = ( 𝑎 (,) 𝑏 ) → ( ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ ( 𝑣 ∩ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ) ) ↔ ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ∧ ( 𝑎 (,) 𝑏 ) ⊆ ( 𝑣 ∩ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ) ) ) )
41 inss2 ⊢ ( 𝑣 ∩ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ) ⊆ ( 𝑥 ( ball ‘ 𝐷 ) 1 )
42 sstr ⊢ ( ( ( 𝑎 (,) 𝑏 ) ⊆ ( 𝑣 ∩ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ) ∧ ( 𝑣 ∩ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ) ⊆ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ) → ( 𝑎 (,) 𝑏 ) ⊆ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) )
43 41 42 mpan2 ⊢ ( ( 𝑎 (,) 𝑏 ) ⊆ ( 𝑣 ∩ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ) → ( 𝑎 (,) 𝑏 ) ⊆ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) )
44 43 adantl ⊢ ( ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ∧ ( 𝑎 (,) 𝑏 ) ⊆ ( 𝑣 ∩ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ) ) → ( 𝑎 (,) 𝑏 ) ⊆ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) )
45 elioore ⊢ ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) → 𝑥 ∈ ℝ )
46 45 adantr ⊢ ( ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ∧ ( 𝑎 (,) 𝑏 ) ⊆ ( 𝑣 ∩ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ) ) → 𝑥 ∈ ℝ )
47 46 16 syl ⊢ ( ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ∧ ( 𝑎 (,) 𝑏 ) ⊆ ( 𝑣 ∩ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ) ) → ( 𝑥 ( ball ‘ 𝐷 ) 1 ) = ( ( 𝑥 − 1 ) (,) ( 𝑥 + 1 ) ) )
48 44 47 sseqtrd ⊢ ( ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ∧ ( 𝑎 (,) 𝑏 ) ⊆ ( 𝑣 ∩ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ) ) → ( 𝑎 (,) 𝑏 ) ⊆ ( ( 𝑥 − 1 ) (,) ( 𝑥 + 1 ) ) )
49 dfss ⊢ ( ( 𝑎 (,) 𝑏 ) ⊆ ( ( 𝑥 − 1 ) (,) ( 𝑥 + 1 ) ) ↔ ( 𝑎 (,) 𝑏 ) = ( ( 𝑎 (,) 𝑏 ) ∩ ( ( 𝑥 − 1 ) (,) ( 𝑥 + 1 ) ) ) )
50 48 49 sylib ⊢ ( ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ∧ ( 𝑎 (,) 𝑏 ) ⊆ ( 𝑣 ∩ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ) ) → ( 𝑎 (,) 𝑏 ) = ( ( 𝑎 (,) 𝑏 ) ∩ ( ( 𝑥 − 1 ) (,) ( 𝑥 + 1 ) ) ) )
51 eliooxr ⊢ ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) → ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) )
52 21 23 jca ⊢ ( 𝑥 ∈ ℝ → ( ( 𝑥 − 1 ) ∈ ℝ* ∧ ( 𝑥 + 1 ) ∈ ℝ* ) )
53 45 52 syl ⊢ ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) → ( ( 𝑥 − 1 ) ∈ ℝ* ∧ ( 𝑥 + 1 ) ∈ ℝ* ) )
54 iooin ⊢ ( ( ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ∧ ( ( 𝑥 − 1 ) ∈ ℝ* ∧ ( 𝑥 + 1 ) ∈ ℝ* ) ) → ( ( 𝑎 (,) 𝑏 ) ∩ ( ( 𝑥 − 1 ) (,) ( 𝑥 + 1 ) ) ) = ( if ( 𝑎 ≤ ( 𝑥 − 1 ) , ( 𝑥 − 1 ) , 𝑎 ) (,) if ( 𝑏 ≤ ( 𝑥 + 1 ) , 𝑏 , ( 𝑥 + 1 ) ) ) )
55 51 53 54 syl2anc ⊢ ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) → ( ( 𝑎 (,) 𝑏 ) ∩ ( ( 𝑥 − 1 ) (,) ( 𝑥 + 1 ) ) ) = ( if ( 𝑎 ≤ ( 𝑥 − 1 ) , ( 𝑥 − 1 ) , 𝑎 ) (,) if ( 𝑏 ≤ ( 𝑥 + 1 ) , 𝑏 , ( 𝑥 + 1 ) ) ) )
56 55 adantr ⊢ ( ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ∧ ( 𝑎 (,) 𝑏 ) ⊆ ( 𝑣 ∩ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ) ) → ( ( 𝑎 (,) 𝑏 ) ∩ ( ( 𝑥 − 1 ) (,) ( 𝑥 + 1 ) ) ) = ( if ( 𝑎 ≤ ( 𝑥 − 1 ) , ( 𝑥 − 1 ) , 𝑎 ) (,) if ( 𝑏 ≤ ( 𝑥 + 1 ) , 𝑏 , ( 𝑥 + 1 ) ) ) )
57 50 56 eqtrd ⊢ ( ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ∧ ( 𝑎 (,) 𝑏 ) ⊆ ( 𝑣 ∩ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ) ) → ( 𝑎 (,) 𝑏 ) = ( if ( 𝑎 ≤ ( 𝑥 − 1 ) , ( 𝑥 − 1 ) , 𝑎 ) (,) if ( 𝑏 ≤ ( 𝑥 + 1 ) , 𝑏 , ( 𝑥 + 1 ) ) ) )
58 mnfxr ⊢ -∞ ∈ ℝ*
59 58 a1i ⊢ ( ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ∧ ( 𝑎 (,) 𝑏 ) ⊆ ( 𝑣 ∩ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ) ) → -∞ ∈ ℝ* )
60 46 21 syl ⊢ ( ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ∧ ( 𝑎 (,) 𝑏 ) ⊆ ( 𝑣 ∩ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ) ) → ( 𝑥 − 1 ) ∈ ℝ* )
61 51 adantr ⊢ ( ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ∧ ( 𝑎 (,) 𝑏 ) ⊆ ( 𝑣 ∩ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ) ) → ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) )
62 61 simpld ⊢ ( ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ∧ ( 𝑎 (,) 𝑏 ) ⊆ ( 𝑣 ∩ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ) ) → 𝑎 ∈ ℝ* )
63 60 62 ifcld ⊢ ( ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ∧ ( 𝑎 (,) 𝑏 ) ⊆ ( 𝑣 ∩ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ) ) → if ( 𝑎 ≤ ( 𝑥 − 1 ) , ( 𝑥 − 1 ) , 𝑎 ) ∈ ℝ* )
64 61 simprd ⊢ ( ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ∧ ( 𝑎 (,) 𝑏 ) ⊆ ( 𝑣 ∩ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ) ) → 𝑏 ∈ ℝ* )
65 46 22 syl ⊢ ( ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ∧ ( 𝑎 (,) 𝑏 ) ⊆ ( 𝑣 ∩ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ) ) → ( 𝑥 + 1 ) ∈ ℝ )
66 65 rexrd ⊢ ( ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ∧ ( 𝑎 (,) 𝑏 ) ⊆ ( 𝑣 ∩ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ) ) → ( 𝑥 + 1 ) ∈ ℝ* )
67 64 66 ifcld ⊢ ( ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ∧ ( 𝑎 (,) 𝑏 ) ⊆ ( 𝑣 ∩ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ) ) → if ( 𝑏 ≤ ( 𝑥 + 1 ) , 𝑏 , ( 𝑥 + 1 ) ) ∈ ℝ* )
68 45 20 syl ⊢ ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) → ( 𝑥 − 1 ) ∈ ℝ )
69 68 adantr ⊢ ( ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ∧ ( 𝑎 (,) 𝑏 ) ⊆ ( 𝑣 ∩ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ) ) → ( 𝑥 − 1 ) ∈ ℝ )
70 69 mnfltd ⊢ ( ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ∧ ( 𝑎 (,) 𝑏 ) ⊆ ( 𝑣 ∩ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ) ) → -∞ < ( 𝑥 − 1 ) )
71 xrmax2 ⊢ ( ( 𝑎 ∈ ℝ* ∧ ( 𝑥 − 1 ) ∈ ℝ* ) → ( 𝑥 − 1 ) ≤ if ( 𝑎 ≤ ( 𝑥 − 1 ) , ( 𝑥 − 1 ) , 𝑎 ) )
72 62 60 71 syl2anc ⊢ ( ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ∧ ( 𝑎 (,) 𝑏 ) ⊆ ( 𝑣 ∩ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ) ) → ( 𝑥 − 1 ) ≤ if ( 𝑎 ≤ ( 𝑥 − 1 ) , ( 𝑥 − 1 ) , 𝑎 ) )
73 59 60 63 70 72 xrltletrd ⊢ ( ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ∧ ( 𝑎 (,) 𝑏 ) ⊆ ( 𝑣 ∩ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ) ) → -∞ < if ( 𝑎 ≤ ( 𝑥 − 1 ) , ( 𝑥 − 1 ) , 𝑎 ) )
74 simpl ⊢ ( ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ∧ ( 𝑎 (,) 𝑏 ) ⊆ ( 𝑣 ∩ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ) ) → 𝑥 ∈ ( 𝑎 (,) 𝑏 ) )
75 74 57 eleqtrd ⊢ ( ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ∧ ( 𝑎 (,) 𝑏 ) ⊆ ( 𝑣 ∩ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ) ) → 𝑥 ∈ ( if ( 𝑎 ≤ ( 𝑥 − 1 ) , ( 𝑥 − 1 ) , 𝑎 ) (,) if ( 𝑏 ≤ ( 𝑥 + 1 ) , 𝑏 , ( 𝑥 + 1 ) ) ) )
76 eliooxr ⊢ ( 𝑥 ∈ ( if ( 𝑎 ≤ ( 𝑥 − 1 ) , ( 𝑥 − 1 ) , 𝑎 ) (,) if ( 𝑏 ≤ ( 𝑥 + 1 ) , 𝑏 , ( 𝑥 + 1 ) ) ) → ( if ( 𝑎 ≤ ( 𝑥 − 1 ) , ( 𝑥 − 1 ) , 𝑎 ) ∈ ℝ* ∧ if ( 𝑏 ≤ ( 𝑥 + 1 ) , 𝑏 , ( 𝑥 + 1 ) ) ∈ ℝ* ) )
77 ne0i ⊢ ( 𝑥 ∈ ( if ( 𝑎 ≤ ( 𝑥 − 1 ) , ( 𝑥 − 1 ) , 𝑎 ) (,) if ( 𝑏 ≤ ( 𝑥 + 1 ) , 𝑏 , ( 𝑥 + 1 ) ) ) → ( if ( 𝑎 ≤ ( 𝑥 − 1 ) , ( 𝑥 − 1 ) , 𝑎 ) (,) if ( 𝑏 ≤ ( 𝑥 + 1 ) , 𝑏 , ( 𝑥 + 1 ) ) ) ≠ ∅ )
78 ioon0 ⊢ ( ( if ( 𝑎 ≤ ( 𝑥 − 1 ) , ( 𝑥 − 1 ) , 𝑎 ) ∈ ℝ* ∧ if ( 𝑏 ≤ ( 𝑥 + 1 ) , 𝑏 , ( 𝑥 + 1 ) ) ∈ ℝ* ) → ( ( if ( 𝑎 ≤ ( 𝑥 − 1 ) , ( 𝑥 − 1 ) , 𝑎 ) (,) if ( 𝑏 ≤ ( 𝑥 + 1 ) , 𝑏 , ( 𝑥 + 1 ) ) ) ≠ ∅ ↔ if ( 𝑎 ≤ ( 𝑥 − 1 ) , ( 𝑥 − 1 ) , 𝑎 ) < if ( 𝑏 ≤ ( 𝑥 + 1 ) , 𝑏 , ( 𝑥 + 1 ) ) ) )
79 77 78 syl5ib ⊢ ( ( if ( 𝑎 ≤ ( 𝑥 − 1 ) , ( 𝑥 − 1 ) , 𝑎 ) ∈ ℝ* ∧ if ( 𝑏 ≤ ( 𝑥 + 1 ) , 𝑏 , ( 𝑥 + 1 ) ) ∈ ℝ* ) → ( 𝑥 ∈ ( if ( 𝑎 ≤ ( 𝑥 − 1 ) , ( 𝑥 − 1 ) , 𝑎 ) (,) if ( 𝑏 ≤ ( 𝑥 + 1 ) , 𝑏 , ( 𝑥 + 1 ) ) ) → if ( 𝑎 ≤ ( 𝑥 − 1 ) , ( 𝑥 − 1 ) , 𝑎 ) < if ( 𝑏 ≤ ( 𝑥 + 1 ) , 𝑏 , ( 𝑥 + 1 ) ) ) )
80 76 79 mpcom ⊢ ( 𝑥 ∈ ( if ( 𝑎 ≤ ( 𝑥 − 1 ) , ( 𝑥 − 1 ) , 𝑎 ) (,) if ( 𝑏 ≤ ( 𝑥 + 1 ) , 𝑏 , ( 𝑥 + 1 ) ) ) → if ( 𝑎 ≤ ( 𝑥 − 1 ) , ( 𝑥 − 1 ) , 𝑎 ) < if ( 𝑏 ≤ ( 𝑥 + 1 ) , 𝑏 , ( 𝑥 + 1 ) ) )
81 75 80 syl ⊢ ( ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ∧ ( 𝑎 (,) 𝑏 ) ⊆ ( 𝑣 ∩ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ) ) → if ( 𝑎 ≤ ( 𝑥 − 1 ) , ( 𝑥 − 1 ) , 𝑎 ) < if ( 𝑏 ≤ ( 𝑥 + 1 ) , 𝑏 , ( 𝑥 + 1 ) ) )
82 xrre2 ⊢ ( ( ( -∞ ∈ ℝ* ∧ if ( 𝑎 ≤ ( 𝑥 − 1 ) , ( 𝑥 − 1 ) , 𝑎 ) ∈ ℝ* ∧ if ( 𝑏 ≤ ( 𝑥 + 1 ) , 𝑏 , ( 𝑥 + 1 ) ) ∈ ℝ* ) ∧ ( -∞ < if ( 𝑎 ≤ ( 𝑥 − 1 ) , ( 𝑥 − 1 ) , 𝑎 ) ∧ if ( 𝑎 ≤ ( 𝑥 − 1 ) , ( 𝑥 − 1 ) , 𝑎 ) < if ( 𝑏 ≤ ( 𝑥 + 1 ) , 𝑏 , ( 𝑥 + 1 ) ) ) ) → if ( 𝑎 ≤ ( 𝑥 − 1 ) , ( 𝑥 − 1 ) , 𝑎 ) ∈ ℝ )
83 59 63 67 73 81 82 syl32anc ⊢ ( ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ∧ ( 𝑎 (,) 𝑏 ) ⊆ ( 𝑣 ∩ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ) ) → if ( 𝑎 ≤ ( 𝑥 − 1 ) , ( 𝑥 − 1 ) , 𝑎 ) ∈ ℝ )
84 mnfle ⊢ ( if ( 𝑎 ≤ ( 𝑥 − 1 ) , ( 𝑥 − 1 ) , 𝑎 ) ∈ ℝ* → -∞ ≤ if ( 𝑎 ≤ ( 𝑥 − 1 ) , ( 𝑥 − 1 ) , 𝑎 ) )
85 63 84 syl ⊢ ( ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ∧ ( 𝑎 (,) 𝑏 ) ⊆ ( 𝑣 ∩ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ) ) → -∞ ≤ if ( 𝑎 ≤ ( 𝑥 − 1 ) , ( 𝑥 − 1 ) , 𝑎 ) )
86 59 63 67 85 81 xrlelttrd ⊢ ( ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ∧ ( 𝑎 (,) 𝑏 ) ⊆ ( 𝑣 ∩ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ) ) → -∞ < if ( 𝑏 ≤ ( 𝑥 + 1 ) , 𝑏 , ( 𝑥 + 1 ) ) )
87 xrmin2 ⊢ ( ( 𝑏 ∈ ℝ* ∧ ( 𝑥 + 1 ) ∈ ℝ* ) → if ( 𝑏 ≤ ( 𝑥 + 1 ) , 𝑏 , ( 𝑥 + 1 ) ) ≤ ( 𝑥 + 1 ) )
88 64 66 87 syl2anc ⊢ ( ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ∧ ( 𝑎 (,) 𝑏 ) ⊆ ( 𝑣 ∩ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ) ) → if ( 𝑏 ≤ ( 𝑥 + 1 ) , 𝑏 , ( 𝑥 + 1 ) ) ≤ ( 𝑥 + 1 ) )
89 xrre ⊢ ( ( ( if ( 𝑏 ≤ ( 𝑥 + 1 ) , 𝑏 , ( 𝑥 + 1 ) ) ∈ ℝ* ∧ ( 𝑥 + 1 ) ∈ ℝ ) ∧ ( -∞ < if ( 𝑏 ≤ ( 𝑥 + 1 ) , 𝑏 , ( 𝑥 + 1 ) ) ∧ if ( 𝑏 ≤ ( 𝑥 + 1 ) , 𝑏 , ( 𝑥 + 1 ) ) ≤ ( 𝑥 + 1 ) ) ) → if ( 𝑏 ≤ ( 𝑥 + 1 ) , 𝑏 , ( 𝑥 + 1 ) ) ∈ ℝ )
90 67 65 86 88 89 syl22anc ⊢ ( ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ∧ ( 𝑎 (,) 𝑏 ) ⊆ ( 𝑣 ∩ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ) ) → if ( 𝑏 ≤ ( 𝑥 + 1 ) , 𝑏 , ( 𝑥 + 1 ) ) ∈ ℝ )
91 1 ioo2blex ⊢ ( ( if ( 𝑎 ≤ ( 𝑥 − 1 ) , ( 𝑥 − 1 ) , 𝑎 ) ∈ ℝ ∧ if ( 𝑏 ≤ ( 𝑥 + 1 ) , 𝑏 , ( 𝑥 + 1 ) ) ∈ ℝ ) → ( if ( 𝑎 ≤ ( 𝑥 − 1 ) , ( 𝑥 − 1 ) , 𝑎 ) (,) if ( 𝑏 ≤ ( 𝑥 + 1 ) , 𝑏 , ( 𝑥 + 1 ) ) ) ∈ ran ( ball ‘ 𝐷 ) )
92 83 90 91 syl2anc ⊢ ( ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ∧ ( 𝑎 (,) 𝑏 ) ⊆ ( 𝑣 ∩ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ) ) → ( if ( 𝑎 ≤ ( 𝑥 − 1 ) , ( 𝑥 − 1 ) , 𝑎 ) (,) if ( 𝑏 ≤ ( 𝑥 + 1 ) , 𝑏 , ( 𝑥 + 1 ) ) ) ∈ ran ( ball ‘ 𝐷 ) )
93 57 92 eqeltrd ⊢ ( ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ∧ ( 𝑎 (,) 𝑏 ) ⊆ ( 𝑣 ∩ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ) ) → ( 𝑎 (,) 𝑏 ) ∈ ran ( ball ‘ 𝐷 ) )
94 inss1 ⊢ ( 𝑣 ∩ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ) ⊆ 𝑣
95 sstr ⊢ ( ( ( 𝑎 (,) 𝑏 ) ⊆ ( 𝑣 ∩ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ) ∧ ( 𝑣 ∩ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ) ⊆ 𝑣 ) → ( 𝑎 (,) 𝑏 ) ⊆ 𝑣 )
96 94 95 mpan2 ⊢ ( ( 𝑎 (,) 𝑏 ) ⊆ ( 𝑣 ∩ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ) → ( 𝑎 (,) 𝑏 ) ⊆ 𝑣 )
97 96 adantl ⊢ ( ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ∧ ( 𝑎 (,) 𝑏 ) ⊆ ( 𝑣 ∩ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ) ) → ( 𝑎 (,) 𝑏 ) ⊆ 𝑣 )
98 sseq1 ⊢ ( 𝑧 = ( 𝑎 (,) 𝑏 ) → ( 𝑧 ⊆ 𝑣 ↔ ( 𝑎 (,) 𝑏 ) ⊆ 𝑣 ) )
99 38 98 anbi12d ⊢ ( 𝑧 = ( 𝑎 (,) 𝑏 ) → ( ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣 ) ↔ ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ∧ ( 𝑎 (,) 𝑏 ) ⊆ 𝑣 ) ) )
100 99 rspcev ⊢ ( ( ( 𝑎 (,) 𝑏 ) ∈ ran ( ball ‘ 𝐷 ) ∧ ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ∧ ( 𝑎 (,) 𝑏 ) ⊆ 𝑣 ) ) → ∃ 𝑧 ∈ ran ( ball ‘ 𝐷 ) ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣 ) )
101 93 74 97 100 syl12anc ⊢ ( ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ∧ ( 𝑎 (,) 𝑏 ) ⊆ ( 𝑣 ∩ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ) ) → ∃ 𝑧 ∈ ran ( ball ‘ 𝐷 ) ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣 ) )
102 blssex ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ ℝ ) ∧ 𝑥 ∈ ℝ ) → ( ∃ 𝑧 ∈ ran ( ball ‘ 𝐷 ) ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣 ) ↔ ∃ 𝑦 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑦 ) ⊆ 𝑣 ) )
103 3 46 102 sylancr ⊢ ( ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ∧ ( 𝑎 (,) 𝑏 ) ⊆ ( 𝑣 ∩ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ) ) → ( ∃ 𝑧 ∈ ran ( ball ‘ 𝐷 ) ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣 ) ↔ ∃ 𝑦 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑦 ) ⊆ 𝑣 ) )
104 101 103 mpbid ⊢ ( ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ∧ ( 𝑎 (,) 𝑏 ) ⊆ ( 𝑣 ∩ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ) ) → ∃ 𝑦 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑦 ) ⊆ 𝑣 )
105 40 104 syl6bi ⊢ ( 𝑧 = ( 𝑎 (,) 𝑏 ) → ( ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ ( 𝑣 ∩ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ) ) → ∃ 𝑦 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑦 ) ⊆ 𝑣 ) )
106 105 a1i ⊢ ( ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) → ( 𝑧 = ( 𝑎 (,) 𝑏 ) → ( ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ ( 𝑣 ∩ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ) ) → ∃ 𝑦 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑦 ) ⊆ 𝑣 ) ) )
107 106 rexlimivv ⊢ ( ∃ 𝑎 ∈ ℝ* ∃ 𝑏 ∈ ℝ* 𝑧 = ( 𝑎 (,) 𝑏 ) → ( ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ ( 𝑣 ∩ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ) ) → ∃ 𝑦 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑦 ) ⊆ 𝑣 ) )
108 107 imp ⊢ ( ( ∃ 𝑎 ∈ ℝ* ∃ 𝑏 ∈ ℝ* 𝑧 = ( 𝑎 (,) 𝑏 ) ∧ ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ ( 𝑣 ∩ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ) ) ) → ∃ 𝑦 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑦 ) ⊆ 𝑣 )
109 37 108 sylanb ⊢ ( ( 𝑧 ∈ ran (,) ∧ ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ ( 𝑣 ∩ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ) ) ) → ∃ 𝑦 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑦 ) ⊆ 𝑣 )
110 109 rexlimiva ⊢ ( ∃ 𝑧 ∈ ran (,) ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ ( 𝑣 ∩ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ) ) → ∃ 𝑦 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑦 ) ⊆ 𝑣 )
111 35 110 syl ⊢ ( ( 𝑣 ∈ ran (,) ∧ 𝑥 ∈ 𝑣 ) → ∃ 𝑦 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑦 ) ⊆ 𝑣 )
112 111 ralrimiva ⊢ ( 𝑣 ∈ ran (,) → ∀ 𝑥 ∈ 𝑣 ∃ 𝑦 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑦 ) ⊆ 𝑣 )
113 2 elmopn2 ⊢ ( 𝐷 ∈ ( ∞Met ‘ ℝ ) → ( 𝑣 ∈ 𝐽 ↔ ( 𝑣 ⊆ ℝ ∧ ∀ 𝑥 ∈ 𝑣 ∃ 𝑦 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑦 ) ⊆ 𝑣 ) ) )
114 3 113 ax-mp ⊢ ( 𝑣 ∈ 𝐽 ↔ ( 𝑣 ⊆ ℝ ∧ ∀ 𝑥 ∈ 𝑣 ∃ 𝑦 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑦 ) ⊆ 𝑣 ) )
115 9 112 114 sylanbrc ⊢ ( 𝑣 ∈ ran (,) → 𝑣 ∈ 𝐽 )
116 115 ssriv ⊢ ran (,) ⊆ 𝐽
117 116 5 sseqtri ⊢ ran (,) ⊆ ( topGen ‘ ran ( ball ‘ 𝐷 ) )
118 2basgen ⊢ ( ( ran ( ball ‘ 𝐷 ) ⊆ ran (,) ∧ ran (,) ⊆ ( topGen ‘ ran ( ball ‘ 𝐷 ) ) ) → ( topGen ‘ ran ( ball ‘ 𝐷 ) ) = ( topGen ‘ ran (,) ) )
119 6 117 118 mp2an ⊢ ( topGen ‘ ran ( ball ‘ 𝐷 ) ) = ( topGen ‘ ran (,) )
120 5 119 eqtr2i ⊢ ( topGen ‘ ran (,) ) = 𝐽