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 
|- ( ( A e. RR /\ B e. RR ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A [,] B ) ) = ( A (,) B ) )

Proof

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