Metamath Proof Explorer

Theorem iccntr

Description: The interior of a closed interval in the standard topology on RR is the corresponding open interval. (Contributed by Mario Carneiro, 1-Sep-2014)

Ref Expression
Assertion iccntr ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) = ( 𝐴 (,) 𝐵 ) )

Proof

Step Hyp Ref Expression
1 rexr ⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℝ* )
2 rexr ⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℝ* )
3 icc0 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( 𝐴 [,] 𝐵 ) = ∅ ↔ 𝐵 < 𝐴 ) )
4 1 2 3 syl2an ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 [,] 𝐵 ) = ∅ ↔ 𝐵 < 𝐴 ) )
5 4 biimpar ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐵 < 𝐴 ) → ( 𝐴 [,] 𝐵 ) = ∅ )
6 5 fveq2d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐵 < 𝐴 ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) = ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ∅ ) )
7 retop ⊢ ( topGen ‘ ran (,) ) ∈ Top
8 ntr0 ⊢ ( ( topGen ‘ ran (,) ) ∈ Top → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ∅ ) = ∅ )
9 7 8 ax-mp ⊢ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ∅ ) = ∅
10 0ss ⊢ ∅ ⊆ ( { 𝐴 , 𝐵 } ∪ ( 𝐴 (,) 𝐵 ) )
11 9 10 eqsstri ⊢ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ∅ ) ⊆ ( { 𝐴 , 𝐵 } ∪ ( 𝐴 (,) 𝐵 ) )
12 6 11 eqsstrdi ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐵 < 𝐴 ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ⊆ ( { 𝐴 , 𝐵 } ∪ ( 𝐴 (,) 𝐵 ) ) )
13 iccssre ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
14 uniretop ⊢ ℝ = ∪ ( topGen ‘ ran (,) )
15 14 ntrss2 ⊢ ( ( ( topGen ‘ ran (,) ) ∈ Top ∧ ( 𝐴 [,] 𝐵 ) ⊆ ℝ ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ⊆ ( 𝐴 [,] 𝐵 ) )
16 7 13 15 sylancr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ⊆ ( 𝐴 [,] 𝐵 ) )
17 16 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≤ 𝐵 ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ⊆ ( 𝐴 [,] 𝐵 ) )
18 1 2 anim12i ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) )
19 uncom ⊢ ( { 𝐴 , 𝐵 } ∪ ( 𝐴 (,) 𝐵 ) ) = ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐴 , 𝐵 } )
20 prunioo ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) → ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐴 , 𝐵 } ) = ( 𝐴 [,] 𝐵 ) )
21 19 20 syl5eq ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) → ( { 𝐴 , 𝐵 } ∪ ( 𝐴 (,) 𝐵 ) ) = ( 𝐴 [,] 𝐵 ) )
22 21 3expa ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 ≤ 𝐵 ) → ( { 𝐴 , 𝐵 } ∪ ( 𝐴 (,) 𝐵 ) ) = ( 𝐴 [,] 𝐵 ) )
23 18 22 sylan ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≤ 𝐵 ) → ( { 𝐴 , 𝐵 } ∪ ( 𝐴 (,) 𝐵 ) ) = ( 𝐴 [,] 𝐵 ) )
24 17 23 sseqtrrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≤ 𝐵 ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ⊆ ( { 𝐴 , 𝐵 } ∪ ( 𝐴 (,) 𝐵 ) ) )
25 simpr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝐵 ∈ ℝ )
26 simpl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝐴 ∈ ℝ )
27 12 24 25 26 ltlecasei ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ⊆ ( { 𝐴 , 𝐵 } ∪ ( 𝐴 (,) 𝐵 ) ) )
28 14 ntropn ⊢ ( ( ( topGen ‘ ran (,) ) ∈ Top ∧ ( 𝐴 [,] 𝐵 ) ⊆ ℝ ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ∈ ( topGen ‘ ran (,) ) )
29 7 13 28 sylancr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ∈ ( topGen ‘ ran (,) ) )
30 eqid ⊢ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) = ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) )
31 30 rexmet ⊢ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ∈ ( ∞Met ‘ ℝ )
32 eqid ⊢ ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) )
33 30 32 tgioo ⊢ ( topGen ‘ ran (,) ) = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) )
34 33 mopni2 ⊢ ( ( ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ∈ ( ∞Met ‘ ℝ ) ∧ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ∈ ( topGen ‘ ran (,) ) ∧ 𝐴 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) → ∃ 𝑥 ∈ ℝ+ ( 𝐴 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑥 ) ⊆ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) )
35 31 34 mp3an1 ⊢ ( ( ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ∈ ( topGen ‘ ran (,) ) ∧ 𝐴 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) → ∃ 𝑥 ∈ ℝ+ ( 𝐴 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑥 ) ⊆ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) )
36 29 35 sylan ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) → ∃ 𝑥 ∈ ℝ+ ( 𝐴 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑥 ) ⊆ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) )
37 26 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 ∈ ℝ+ ) → 𝐴 ∈ ℝ )
38 rphalfcl ⊢ ( 𝑥 ∈ ℝ+ → ( 𝑥 / 2 ) ∈ ℝ+ )
39 38 adantl ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝑥 / 2 ) ∈ ℝ+ )
40 37 39 ltsubrpd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝐴 − ( 𝑥 / 2 ) ) < 𝐴 )
41 39 rpred ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝑥 / 2 ) ∈ ℝ )
42 37 41 resubcld ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝐴 − ( 𝑥 / 2 ) ) ∈ ℝ )
43 42 37 ltnled ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 ∈ ℝ+ ) → ( ( 𝐴 − ( 𝑥 / 2 ) ) < 𝐴 ↔ ¬ 𝐴 ≤ ( 𝐴 − ( 𝑥 / 2 ) ) ) )
44 40 43 mpbid ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 ∈ ℝ+ ) → ¬ 𝐴 ≤ ( 𝐴 − ( 𝑥 / 2 ) ) )
45 rpre ⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ∈ ℝ )
46 45 adantl ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℝ )
47 rphalflt ⊢ ( 𝑥 ∈ ℝ+ → ( 𝑥 / 2 ) < 𝑥 )
48 47 adantl ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝑥 / 2 ) < 𝑥 )
49 41 46 37 48 ltsub2dd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝐴 − 𝑥 ) < ( 𝐴 − ( 𝑥 / 2 ) ) )
50 37 46 readdcld ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝐴 + 𝑥 ) ∈ ℝ )
51 ltaddrp ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑥 ∈ ℝ+ ) → 𝐴 < ( 𝐴 + 𝑥 ) )
52 37 51 sylancom ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 ∈ ℝ+ ) → 𝐴 < ( 𝐴 + 𝑥 ) )
53 42 37 50 40 52 lttrd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝐴 − ( 𝑥 / 2 ) ) < ( 𝐴 + 𝑥 ) )
54 37 46 resubcld ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝐴 − 𝑥 ) ∈ ℝ )
55 54 rexrd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝐴 − 𝑥 ) ∈ ℝ* )
56 50 rexrd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝐴 + 𝑥 ) ∈ ℝ* )
57 elioo2 ⊢ ( ( ( 𝐴 − 𝑥 ) ∈ ℝ* ∧ ( 𝐴 + 𝑥 ) ∈ ℝ* ) → ( ( 𝐴 − ( 𝑥 / 2 ) ) ∈ ( ( 𝐴 − 𝑥 ) (,) ( 𝐴 + 𝑥 ) ) ↔ ( ( 𝐴 − ( 𝑥 / 2 ) ) ∈ ℝ ∧ ( 𝐴 − 𝑥 ) < ( 𝐴 − ( 𝑥 / 2 ) ) ∧ ( 𝐴 − ( 𝑥 / 2 ) ) < ( 𝐴 + 𝑥 ) ) ) )
58 55 56 57 syl2anc ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 ∈ ℝ+ ) → ( ( 𝐴 − ( 𝑥 / 2 ) ) ∈ ( ( 𝐴 − 𝑥 ) (,) ( 𝐴 + 𝑥 ) ) ↔ ( ( 𝐴 − ( 𝑥 / 2 ) ) ∈ ℝ ∧ ( 𝐴 − 𝑥 ) < ( 𝐴 − ( 𝑥 / 2 ) ) ∧ ( 𝐴 − ( 𝑥 / 2 ) ) < ( 𝐴 + 𝑥 ) ) ) )
59 42 49 53 58 mpbir3and ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝐴 − ( 𝑥 / 2 ) ) ∈ ( ( 𝐴 − 𝑥 ) (,) ( 𝐴 + 𝑥 ) ) )
60 30 bl2ioo ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( 𝐴 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑥 ) = ( ( 𝐴 − 𝑥 ) (,) ( 𝐴 + 𝑥 ) ) )
61 37 46 60 syl2anc ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝐴 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑥 ) = ( ( 𝐴 − 𝑥 ) (,) ( 𝐴 + 𝑥 ) ) )
62 59 61 eleqtrrd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝐴 − ( 𝑥 / 2 ) ) ∈ ( 𝐴 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑥 ) )
63 ssel ⊢ ( ( 𝐴 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑥 ) ⊆ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) → ( ( 𝐴 − ( 𝑥 / 2 ) ) ∈ ( 𝐴 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑥 ) → ( 𝐴 − ( 𝑥 / 2 ) ) ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) )
64 62 63 syl5com ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 ∈ ℝ+ ) → ( ( 𝐴 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑥 ) ⊆ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) → ( 𝐴 − ( 𝑥 / 2 ) ) ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) )
65 16 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 ∈ ℝ+ ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ⊆ ( 𝐴 [,] 𝐵 ) )
66 65 sseld ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 ∈ ℝ+ ) → ( ( 𝐴 − ( 𝑥 / 2 ) ) ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) → ( 𝐴 − ( 𝑥 / 2 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) )
67 elicc2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 − ( 𝑥 / 2 ) ) ∈ ( 𝐴 [,] 𝐵 ) ↔ ( ( 𝐴 − ( 𝑥 / 2 ) ) ∈ ℝ ∧ 𝐴 ≤ ( 𝐴 − ( 𝑥 / 2 ) ) ∧ ( 𝐴 − ( 𝑥 / 2 ) ) ≤ 𝐵 ) ) )
68 simp2 ⊢ ( ( ( 𝐴 − ( 𝑥 / 2 ) ) ∈ ℝ ∧ 𝐴 ≤ ( 𝐴 − ( 𝑥 / 2 ) ) ∧ ( 𝐴 − ( 𝑥 / 2 ) ) ≤ 𝐵 ) → 𝐴 ≤ ( 𝐴 − ( 𝑥 / 2 ) ) )
69 67 68 syl6bi ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 − ( 𝑥 / 2 ) ) ∈ ( 𝐴 [,] 𝐵 ) → 𝐴 ≤ ( 𝐴 − ( 𝑥 / 2 ) ) ) )
70 69 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 ∈ ℝ+ ) → ( ( 𝐴 − ( 𝑥 / 2 ) ) ∈ ( 𝐴 [,] 𝐵 ) → 𝐴 ≤ ( 𝐴 − ( 𝑥 / 2 ) ) ) )
71 64 66 70 3syld ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 ∈ ℝ+ ) → ( ( 𝐴 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑥 ) ⊆ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) → 𝐴 ≤ ( 𝐴 − ( 𝑥 / 2 ) ) ) )
72 44 71 mtod ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 ∈ ℝ+ ) → ¬ ( 𝐴 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑥 ) ⊆ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) )
73 72 nrexdv ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) → ¬ ∃ 𝑥 ∈ ℝ+ ( 𝐴 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑥 ) ⊆ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) )
74 36 73 pm2.65da ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ¬ 𝐴 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) )
75 33 mopni2 ⊢ ( ( ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ∈ ( ∞Met ‘ ℝ ) ∧ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ∈ ( topGen ‘ ran (,) ) ∧ 𝐵 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) → ∃ 𝑥 ∈ ℝ+ ( 𝐵 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑥 ) ⊆ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) )
76 31 75 mp3an1 ⊢ ( ( ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ∈ ( topGen ‘ ran (,) ) ∧ 𝐵 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) → ∃ 𝑥 ∈ ℝ+ ( 𝐵 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑥 ) ⊆ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) )
77 29 76 sylan ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐵 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) → ∃ 𝑥 ∈ ℝ+ ( 𝐵 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑥 ) ⊆ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) )
78 25 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐵 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 ∈ ℝ+ ) → 𝐵 ∈ ℝ )
79 38 adantl ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐵 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝑥 / 2 ) ∈ ℝ+ )
80 78 79 ltaddrpd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐵 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 ∈ ℝ+ ) → 𝐵 < ( 𝐵 + ( 𝑥 / 2 ) ) )
81 79 rpred ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐵 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝑥 / 2 ) ∈ ℝ )
82 78 81 readdcld ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐵 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝐵 + ( 𝑥 / 2 ) ) ∈ ℝ )
83 78 82 ltnled ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐵 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝐵 < ( 𝐵 + ( 𝑥 / 2 ) ) ↔ ¬ ( 𝐵 + ( 𝑥 / 2 ) ) ≤ 𝐵 ) )
84 80 83 mpbid ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐵 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 ∈ ℝ+ ) → ¬ ( 𝐵 + ( 𝑥 / 2 ) ) ≤ 𝐵 )
85 45 adantl ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐵 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℝ )
86 78 85 resubcld ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐵 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝐵 − 𝑥 ) ∈ ℝ )
87 ltsubrp ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝑥 ∈ ℝ+ ) → ( 𝐵 − 𝑥 ) < 𝐵 )
88 78 87 sylancom ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐵 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝐵 − 𝑥 ) < 𝐵 )
89 86 78 82 88 80 lttrd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐵 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝐵 − 𝑥 ) < ( 𝐵 + ( 𝑥 / 2 ) ) )
90 47 adantl ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐵 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝑥 / 2 ) < 𝑥 )
91 81 85 78 90 ltadd2dd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐵 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝐵 + ( 𝑥 / 2 ) ) < ( 𝐵 + 𝑥 ) )
92 86 rexrd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐵 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝐵 − 𝑥 ) ∈ ℝ* )
93 78 85 readdcld ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐵 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝐵 + 𝑥 ) ∈ ℝ )
94 93 rexrd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐵 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝐵 + 𝑥 ) ∈ ℝ* )
95 elioo2 ⊢ ( ( ( 𝐵 − 𝑥 ) ∈ ℝ* ∧ ( 𝐵 + 𝑥 ) ∈ ℝ* ) → ( ( 𝐵 + ( 𝑥 / 2 ) ) ∈ ( ( 𝐵 − 𝑥 ) (,) ( 𝐵 + 𝑥 ) ) ↔ ( ( 𝐵 + ( 𝑥 / 2 ) ) ∈ ℝ ∧ ( 𝐵 − 𝑥 ) < ( 𝐵 + ( 𝑥 / 2 ) ) ∧ ( 𝐵 + ( 𝑥 / 2 ) ) < ( 𝐵 + 𝑥 ) ) ) )
96 92 94 95 syl2anc ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐵 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 ∈ ℝ+ ) → ( ( 𝐵 + ( 𝑥 / 2 ) ) ∈ ( ( 𝐵 − 𝑥 ) (,) ( 𝐵 + 𝑥 ) ) ↔ ( ( 𝐵 + ( 𝑥 / 2 ) ) ∈ ℝ ∧ ( 𝐵 − 𝑥 ) < ( 𝐵 + ( 𝑥 / 2 ) ) ∧ ( 𝐵 + ( 𝑥 / 2 ) ) < ( 𝐵 + 𝑥 ) ) ) )
97 82 89 91 96 mpbir3and ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐵 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝐵 + ( 𝑥 / 2 ) ) ∈ ( ( 𝐵 − 𝑥 ) (,) ( 𝐵 + 𝑥 ) ) )
98 30 bl2ioo ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( 𝐵 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑥 ) = ( ( 𝐵 − 𝑥 ) (,) ( 𝐵 + 𝑥 ) ) )
99 78 85 98 syl2anc ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐵 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝐵 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑥 ) = ( ( 𝐵 − 𝑥 ) (,) ( 𝐵 + 𝑥 ) ) )
100 97 99 eleqtrrd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐵 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝐵 + ( 𝑥 / 2 ) ) ∈ ( 𝐵 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑥 ) )
101 ssel ⊢ ( ( 𝐵 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑥 ) ⊆ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) → ( ( 𝐵 + ( 𝑥 / 2 ) ) ∈ ( 𝐵 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑥 ) → ( 𝐵 + ( 𝑥 / 2 ) ) ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) )
102 100 101 syl5com ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐵 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 ∈ ℝ+ ) → ( ( 𝐵 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑥 ) ⊆ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) → ( 𝐵 + ( 𝑥 / 2 ) ) ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) )
103 16 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐵 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 ∈ ℝ+ ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ⊆ ( 𝐴 [,] 𝐵 ) )
104 103 sseld ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐵 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 ∈ ℝ+ ) → ( ( 𝐵 + ( 𝑥 / 2 ) ) ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) → ( 𝐵 + ( 𝑥 / 2 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) )
105 elicc2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐵 + ( 𝑥 / 2 ) ) ∈ ( 𝐴 [,] 𝐵 ) ↔ ( ( 𝐵 + ( 𝑥 / 2 ) ) ∈ ℝ ∧ 𝐴 ≤ ( 𝐵 + ( 𝑥 / 2 ) ) ∧ ( 𝐵 + ( 𝑥 / 2 ) ) ≤ 𝐵 ) ) )
106 simp3 ⊢ ( ( ( 𝐵 + ( 𝑥 / 2 ) ) ∈ ℝ ∧ 𝐴 ≤ ( 𝐵 + ( 𝑥 / 2 ) ) ∧ ( 𝐵 + ( 𝑥 / 2 ) ) ≤ 𝐵 ) → ( 𝐵 + ( 𝑥 / 2 ) ) ≤ 𝐵 )
107 105 106 syl6bi ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐵 + ( 𝑥 / 2 ) ) ∈ ( 𝐴 [,] 𝐵 ) → ( 𝐵 + ( 𝑥 / 2 ) ) ≤ 𝐵 ) )
108 107 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐵 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 ∈ ℝ+ ) → ( ( 𝐵 + ( 𝑥 / 2 ) ) ∈ ( 𝐴 [,] 𝐵 ) → ( 𝐵 + ( 𝑥 / 2 ) ) ≤ 𝐵 ) )
109 102 104 108 3syld ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐵 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 ∈ ℝ+ ) → ( ( 𝐵 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑥 ) ⊆ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) → ( 𝐵 + ( 𝑥 / 2 ) ) ≤ 𝐵 ) )
110 84 109 mtod ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐵 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 ∈ ℝ+ ) → ¬ ( 𝐵 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑥 ) ⊆ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) )
111 110 nrexdv ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐵 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) → ¬ ∃ 𝑥 ∈ ℝ+ ( 𝐵 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑥 ) ⊆ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) )
112 77 111 pm2.65da ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ¬ 𝐵 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) )
113 eleq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ↔ 𝐴 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) )
114 113 notbid ⊢ ( 𝑥 = 𝐴 → ( ¬ 𝑥 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ↔ ¬ 𝐴 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) )
115 eleq1 ⊢ ( 𝑥 = 𝐵 → ( 𝑥 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ↔ 𝐵 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) )
116 115 notbid ⊢ ( 𝑥 = 𝐵 → ( ¬ 𝑥 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ↔ ¬ 𝐵 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) )
117 114 116 ralprg ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ∀ 𝑥 ∈ { 𝐴 , 𝐵 } ¬ 𝑥 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ↔ ( ¬ 𝐴 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝐵 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) ) )
118 74 112 117 mpbir2and ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ∀ 𝑥 ∈ { 𝐴 , 𝐵 } ¬ 𝑥 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) )
119 disjr ⊢ ( ( ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ∩ { 𝐴 , 𝐵 } ) = ∅ ↔ ∀ 𝑥 ∈ { 𝐴 , 𝐵 } ¬ 𝑥 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) )
120 118 119 sylibr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ∩ { 𝐴 , 𝐵 } ) = ∅ )
121 disjssun ⊢ ( ( ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ∩ { 𝐴 , 𝐵 } ) = ∅ → ( ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ⊆ ( { 𝐴 , 𝐵 } ∪ ( 𝐴 (,) 𝐵 ) ) ↔ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ⊆ ( 𝐴 (,) 𝐵 ) ) )
122 120 121 syl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ⊆ ( { 𝐴 , 𝐵 } ∪ ( 𝐴 (,) 𝐵 ) ) ↔ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ⊆ ( 𝐴 (,) 𝐵 ) ) )
123 27 122 mpbid ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ⊆ ( 𝐴 (,) 𝐵 ) )
124 iooretop ⊢ ( 𝐴 (,) 𝐵 ) ∈ ( topGen ‘ ran (,) )
125 ioossicc ⊢ ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 )
126 14 ssntr ⊢ ( ( ( ( topGen ‘ ran (,) ) ∈ Top ∧ ( 𝐴 [,] 𝐵 ) ⊆ ℝ ) ∧ ( ( 𝐴 (,) 𝐵 ) ∈ ( topGen ‘ ran (,) ) ∧ ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝐴 (,) 𝐵 ) ⊆ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) )
127 124 125 126 mpanr12 ⊢ ( ( ( topGen ‘ ran (,) ) ∈ Top ∧ ( 𝐴 [,] 𝐵 ) ⊆ ℝ ) → ( 𝐴 (,) 𝐵 ) ⊆ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) )
128 7 13 127 sylancr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 (,) 𝐵 ) ⊆ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) )
129 123 128 eqssd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) = ( 𝐴 (,) 𝐵 ) )