MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  iccntr Unicode version

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

Proof of Theorem iccntr
StepHypRef Expression
1 rexr 8831 . . . . . . . 8  |-  ( A  e.  RR  ->  A  e.  RR* )
2 rexr 8831 . . . . . . . 8  |-  ( B  e.  RR  ->  B  e.  RR* )
3 icc0 10656 . . . . . . . 8  |-  ( ( A  e.  RR*  /\  B  e.  RR* )  ->  (
( A [,] B
)  =  (/)  <->  B  <  A ) )
41, 2, 3syl2an 465 . . . . . . 7  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( ( A [,] B )  =  (/)  <->  B  <  A ) )
54biimpar 473 . . . . . 6  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  B  <  A
)  ->  ( A [,] B )  =  (/) )
65fveq2d 5448 . . . . 5  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  B  <  A
)  ->  ( ( int `  ( topGen `  ran  (,) ) ) `  ( A [,] B ) )  =  ( ( int `  ( topGen `  ran  (,) )
) `  (/) ) )
7 retop 18218 . . . . . . . 8  |-  ( topGen ` 
ran  (,) )  e.  Top
8 ntr0 16766 . . . . . . . 8  |-  ( (
topGen `  ran  (,) )  e.  Top  ->  ( ( int `  ( topGen `  ran  (,) ) ) `  (/) )  =  (/) )
97, 8ax-mp 10 . . . . . . 7  |-  ( ( int `  ( topGen ` 
ran  (,) ) ) `  (/) )  =  (/)
10 0ss 3444 . . . . . . 7  |-  (/)  C_  ( { A ,  B }  u.  ( A (,) B
) )
119, 10eqsstri 3169 . . . . . 6  |-  ( ( int `  ( topGen ` 
ran  (,) ) ) `  (/) )  C_  ( { A ,  B }  u.  ( A (,) B
) )
1211a1i 12 . . . . 5  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  B  <  A
)  ->  ( ( int `  ( topGen `  ran  (,) ) ) `  (/) )  C_  ( { A ,  B }  u.  ( A (,) B ) ) )
136, 12eqsstrd 3173 . . . 4  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  B  <  A
)  ->  ( ( int `  ( topGen `  ran  (,) ) ) `  ( A [,] B ) ) 
C_  ( { A ,  B }  u.  ( A (,) B ) ) )
14 iccssre 10683 . . . . . . 7  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A [,] B
)  C_  RR )
15 uniretop 18219 . . . . . . . 8  |-  RR  =  U. ( topGen `  ran  (,) )
1615ntrss2 16742 . . . . . . 7  |-  ( ( ( topGen `  ran  (,) )  e.  Top  /\  ( A [,] B )  C_  RR )  ->  ( ( int `  ( topGen ` 
ran  (,) ) ) `  ( A [,] B ) )  C_  ( A [,] B ) )
177, 14, 16sylancr 647 . . . . . 6  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( ( int `  ( topGen `
 ran  (,) )
) `  ( A [,] B ) )  C_  ( A [,] B ) )
1817adantr 453 . . . . 5  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  A  <_  B
)  ->  ( ( int `  ( topGen `  ran  (,) ) ) `  ( A [,] B ) ) 
C_  ( A [,] B ) )
191, 2anim12i 551 . . . . . 6  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  e.  RR*  /\  B  e.  RR* )
)
20 uncom 3280 . . . . . . . 8  |-  ( { A ,  B }  u.  ( A (,) B
) )  =  ( ( A (,) B
)  u.  { A ,  B } )
21 prunioo 10716 . . . . . . . 8  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  A  <_  B )  ->  (
( A (,) B
)  u.  { A ,  B } )  =  ( A [,] B
) )
2220, 21syl5eq 2300 . . . . . . 7  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  A  <_  B )  ->  ( { A ,  B }  u.  ( A (,) B
) )  =  ( A [,] B ) )
23223expa 1156 . . . . . 6  |-  ( ( ( A  e.  RR*  /\  B  e.  RR* )  /\  A  <_  B )  ->  ( { A ,  B }  u.  ( A (,) B ) )  =  ( A [,] B ) )
2419, 23sylan 459 . . . . 5  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  A  <_  B
)  ->  ( { A ,  B }  u.  ( A (,) B
) )  =  ( A [,] B ) )
2518, 24sseqtr4d 3176 . . . 4  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  A  <_  B
)  ->  ( ( int `  ( topGen `  ran  (,) ) ) `  ( A [,] B ) ) 
C_  ( { A ,  B }  u.  ( A (,) B ) ) )
26 simpr 449 . . . 4  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  B  e.  RR )
27 simpl 445 . . . 4  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  A  e.  RR )
2813, 25, 26, 27ltlecasei 8882 . . 3  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( ( int `  ( topGen `
 ran  (,) )
) `  ( A [,] B ) )  C_  ( { A ,  B }  u.  ( A (,) B ) ) )
2915ntropn 16734 . . . . . . . . 9  |-  ( ( ( topGen `  ran  (,) )  e.  Top  /\  ( A [,] B )  C_  RR )  ->  ( ( int `  ( topGen ` 
ran  (,) ) ) `  ( A [,] B ) )  e.  ( topGen ` 
ran  (,) ) )
307, 14, 29sylancr 647 . . . . . . . 8  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( ( int `  ( topGen `
 ran  (,) )
) `  ( A [,] B ) )  e.  ( topGen `  ran  (,) )
)
31 eqid 2256 . . . . . . . . . 10  |-  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) )  =  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) )
3231rexmet 18245 . . . . . . . . 9  |-  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) )  e.  ( * Met `  RR )
33 eqid 2256 . . . . . . . . . . 11  |-  ( MetOpen `  ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) ) )  =  ( MetOpen `  ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) ) )
3431, 33tgioo 18250 . . . . . . . . . 10  |-  ( topGen ` 
ran  (,) )  =  (
MetOpen `  ( ( abs 
o.  -  )  |`  ( RR  X.  RR ) ) )
3534mopni2 17987 . . . . . . . . 9  |-  ( ( ( ( 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 ) ) )
3632, 35mp3an1 1269 . . . . . . . 8  |-  ( ( ( ( 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 ) ) )
3730, 36sylan 459 . . . . . . 7  |-  ( ( ( 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 ) ) )
3827ad2antrr 709 . . . . . . . . . . 11  |-  ( ( ( ( A  e.  RR  /\  B  e.  RR )  /\  A  e.  ( ( int `  ( topGen `
 ran  (,) )
) `  ( A [,] B ) ) )  /\  x  e.  RR+ )  ->  A  e.  RR )
39 rphalfcl 10331 . . . . . . . . . . . 12  |-  ( x  e.  RR+  ->  ( x  /  2 )  e.  RR+ )
4039adantl 454 . . . . . . . . . . 11  |-  ( ( ( ( A  e.  RR  /\  B  e.  RR )  /\  A  e.  ( ( int `  ( topGen `
 ran  (,) )
) `  ( A [,] B ) ) )  /\  x  e.  RR+ )  ->  ( x  / 
2 )  e.  RR+ )
4138, 40ltsubrpd 10371 . . . . . . . . . 10  |-  ( ( ( ( A  e.  RR  /\  B  e.  RR )  /\  A  e.  ( ( int `  ( topGen `
 ran  (,) )
) `  ( A [,] B ) ) )  /\  x  e.  RR+ )  ->  ( A  -  ( x  /  2
) )  <  A
)
4240rpred 10343 . . . . . . . . . . . 12  |-  ( ( ( ( A  e.  RR  /\  B  e.  RR )  /\  A  e.  ( ( int `  ( topGen `
 ran  (,) )
) `  ( A [,] B ) ) )  /\  x  e.  RR+ )  ->  ( x  / 
2 )  e.  RR )
4338, 42resubcld 9165 . . . . . . . . . . 11  |-  ( ( ( ( A  e.  RR  /\  B  e.  RR )  /\  A  e.  ( ( int `  ( topGen `
 ran  (,) )
) `  ( A [,] B ) ) )  /\  x  e.  RR+ )  ->  ( A  -  ( x  /  2
) )  e.  RR )
4443, 38ltnled 8920 . . . . . . . . . 10  |-  ( ( ( ( A  e.  RR  /\  B  e.  RR )  /\  A  e.  ( ( int `  ( topGen `
 ran  (,) )
) `  ( A [,] B ) ) )  /\  x  e.  RR+ )  ->  ( ( A  -  ( x  / 
2 ) )  < 
A  <->  -.  A  <_  ( A  -  ( x  /  2 ) ) ) )
4541, 44mpbid 203 . . . . . . . . 9  |-  ( ( ( ( A  e.  RR  /\  B  e.  RR )  /\  A  e.  ( ( int `  ( topGen `
 ran  (,) )
) `  ( A [,] B ) ) )  /\  x  e.  RR+ )  ->  -.  A  <_  ( A  -  ( x  /  2 ) ) )
46 rpre 10313 . . . . . . . . . . . . . . 15  |-  ( x  e.  RR+  ->  x  e.  RR )
4746adantl 454 . . . . . . . . . . . . . 14  |-  ( ( ( ( A  e.  RR  /\  B  e.  RR )  /\  A  e.  ( ( int `  ( topGen `
 ran  (,) )
) `  ( A [,] B ) ) )  /\  x  e.  RR+ )  ->  x  e.  RR )
48 rphalflt 10333 . . . . . . . . . . . . . . 15  |-  ( x  e.  RR+  ->  ( x  /  2 )  < 
x )
4948adantl 454 . . . . . . . . . . . . . 14  |-  ( ( ( ( A  e.  RR  /\  B  e.  RR )  /\  A  e.  ( ( int `  ( topGen `
 ran  (,) )
) `  ( A [,] B ) ) )  /\  x  e.  RR+ )  ->  ( x  / 
2 )  <  x
)
5042, 47, 38, 49ltsub2dd 9339 . . . . . . . . . . . . 13  |-  ( ( ( ( A  e.  RR  /\  B  e.  RR )  /\  A  e.  ( ( int `  ( topGen `
 ran  (,) )
) `  ( A [,] B ) ) )  /\  x  e.  RR+ )  ->  ( A  -  x )  <  ( A  -  ( x  /  2 ) ) )
5138, 47readdcld 8816 . . . . . . . . . . . . . 14  |-  ( ( ( ( A  e.  RR  /\  B  e.  RR )  /\  A  e.  ( ( int `  ( topGen `
 ran  (,) )
) `  ( A [,] B ) ) )  /\  x  e.  RR+ )  ->  ( A  +  x )  e.  RR )
52 ltaddrp 10339 . . . . . . . . . . . . . . 15  |-  ( ( A  e.  RR  /\  x  e.  RR+ )  ->  A  <  ( A  +  x ) )
5338, 52sylancom 651 . . . . . . . . . . . . . 14  |-  ( ( ( ( A  e.  RR  /\  B  e.  RR )  /\  A  e.  ( ( int `  ( topGen `
 ran  (,) )
) `  ( A [,] B ) ) )  /\  x  e.  RR+ )  ->  A  <  ( A  +  x )
)
5443, 38, 51, 41, 53lttrd 8931 . . . . . . . . . . . . 13  |-  ( ( ( ( A  e.  RR  /\  B  e.  RR )  /\  A  e.  ( ( int `  ( topGen `
 ran  (,) )
) `  ( A [,] B ) ) )  /\  x  e.  RR+ )  ->  ( A  -  ( x  /  2
) )  <  ( A  +  x )
)
5538, 47resubcld 9165 . . . . . . . . . . . . . . 15  |-  ( ( ( ( A  e.  RR  /\  B  e.  RR )  /\  A  e.  ( ( int `  ( topGen `
 ran  (,) )
) `  ( A [,] B ) ) )  /\  x  e.  RR+ )  ->  ( A  -  x )  e.  RR )
5655rexrd 8835 . . . . . . . . . . . . . 14  |-  ( ( ( ( A  e.  RR  /\  B  e.  RR )  /\  A  e.  ( ( int `  ( topGen `
 ran  (,) )
) `  ( A [,] B ) ) )  /\  x  e.  RR+ )  ->  ( A  -  x )  e.  RR* )
5751rexrd 8835 . . . . . . . . . . . . . 14  |-  ( ( ( ( A  e.  RR  /\  B  e.  RR )  /\  A  e.  ( ( int `  ( topGen `
 ran  (,) )
) `  ( A [,] B ) ) )  /\  x  e.  RR+ )  ->  ( A  +  x )  e.  RR* )
58 elioo2 10649 . . . . . . . . . . . . . 14  |-  ( ( ( 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
) ) ) )
5956, 57, 58syl2anc 645 . . . . . . . . . . . . 13  |-  ( ( ( ( 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
) ) ) )
6043, 50, 54, 59mpbir3and 1140 . . . . . . . . . . . 12  |-  ( ( ( ( A  e.  RR  /\  B  e.  RR )  /\  A  e.  ( ( int `  ( topGen `
 ran  (,) )
) `  ( A [,] B ) ) )  /\  x  e.  RR+ )  ->  ( A  -  ( x  /  2
) )  e.  ( ( A  -  x
) (,) ( A  +  x ) ) )
6131bl2ioo 18246 . . . . . . . . . . . . 13  |-  ( ( A  e.  RR  /\  x  e.  RR )  ->  ( A ( ball `  ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) ) ) x )  =  ( ( A  -  x ) (,) ( A  +  x )
) )
6238, 47, 61syl2anc 645 . . . . . . . . . . . 12  |-  ( ( ( ( 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 ) ) )
6360, 62eleqtrrd 2333 . . . . . . . . . . 11  |-  ( ( ( ( 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 ) )
64 ssel 3135 . . . . . . . . . . 11  |-  ( ( 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 ) ) ) )
6563, 64syl5com 28 . . . . . . . . . 10  |-  ( ( ( ( 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 ) ) ) )
6617ad2antrr 709 . . . . . . . . . . 11  |-  ( ( ( ( A  e.  RR  /\  B  e.  RR )  /\  A  e.  ( ( int `  ( topGen `
 ran  (,) )
) `  ( A [,] B ) ) )  /\  x  e.  RR+ )  ->  ( ( int `  ( topGen `  ran  (,) )
) `  ( A [,] B ) )  C_  ( A [,] B ) )
6766sseld 3140 . . . . . . . . . 10  |-  ( ( ( ( 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 ) ) )
68 elicc2 10667 . . . . . . . . . . . 12  |-  ( ( 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 )
) )
69 simp2 961 . . . . . . . . . . . 12  |-  ( ( ( A  -  (
x  /  2 ) )  e.  RR  /\  A  <_  ( A  -  ( x  /  2
) )  /\  ( A  -  ( x  /  2 ) )  <_  B )  ->  A  <_  ( A  -  ( x  /  2
) ) )
7068, 69syl6bi 221 . . . . . . . . . . 11  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( ( A  -  ( x  /  2
) )  e.  ( A [,] B )  ->  A  <_  ( A  -  ( x  /  2 ) ) ) )
7170ad2antrr 709 . . . . . . . . . 10  |-  ( ( ( ( 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 ) ) ) )
7265, 67, 713syld 53 . . . . . . . . 9  |-  ( ( ( ( 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 ) ) ) )
7345, 72mtod 170 . . . . . . . 8  |-  ( ( ( ( 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 ) ) )
7473nrexdv 2619 . . . . . . 7  |-  ( ( ( 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 ) ) )
7537, 74pm2.65da 562 . . . . . 6  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  -.  A  e.  ( ( int `  ( topGen `
 ran  (,) )
) `  ( A [,] B ) ) )
7634mopni2 17987 . . . . . . . . 9  |-  ( ( ( ( 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 ) ) )
7732, 76mp3an1 1269 . . . . . . . 8  |-  ( ( ( ( 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 ) ) )
7830, 77sylan 459 . . . . . . 7  |-  ( ( ( 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 ) ) )
7926ad2antrr 709 . . . . . . . . . . 11  |-  ( ( ( ( A  e.  RR  /\  B  e.  RR )  /\  B  e.  ( ( int `  ( topGen `
 ran  (,) )
) `  ( A [,] B ) ) )  /\  x  e.  RR+ )  ->  B  e.  RR )
8039adantl 454 . . . . . . . . . . 11  |-  ( ( ( ( A  e.  RR  /\  B  e.  RR )  /\  B  e.  ( ( int `  ( topGen `
 ran  (,) )
) `  ( A [,] B ) ) )  /\  x  e.  RR+ )  ->  ( x  / 
2 )  e.  RR+ )
8179, 80ltaddrpd 10372 . . . . . . . . . 10  |-  ( ( ( ( A  e.  RR  /\  B  e.  RR )  /\  B  e.  ( ( int `  ( topGen `
 ran  (,) )
) `  ( A [,] B ) ) )  /\  x  e.  RR+ )  ->  B  <  ( B  +  ( x  /  2 ) ) )
8280rpred 10343 . . . . . . . . . . . 12  |-  ( ( ( ( A  e.  RR  /\  B  e.  RR )  /\  B  e.  ( ( int `  ( topGen `
 ran  (,) )
) `  ( A [,] B ) ) )  /\  x  e.  RR+ )  ->  ( x  / 
2 )  e.  RR )
8379, 82readdcld 8816 . . . . . . . . . . 11  |-  ( ( ( ( A  e.  RR  /\  B  e.  RR )  /\  B  e.  ( ( int `  ( topGen `
 ran  (,) )
) `  ( A [,] B ) ) )  /\  x  e.  RR+ )  ->  ( B  +  ( x  /  2
) )  e.  RR )
8479, 83ltnled 8920 . . . . . . . . . 10  |-  ( ( ( ( A  e.  RR  /\  B  e.  RR )  /\  B  e.  ( ( int `  ( topGen `
 ran  (,) )
) `  ( A [,] B ) ) )  /\  x  e.  RR+ )  ->  ( B  < 
( B  +  ( x  /  2 ) )  <->  -.  ( B  +  ( x  / 
2 ) )  <_  B ) )
8581, 84mpbid 203 . . . . . . . . 9  |-  ( ( ( ( A  e.  RR  /\  B  e.  RR )  /\  B  e.  ( ( int `  ( topGen `
 ran  (,) )
) `  ( A [,] B ) ) )  /\  x  e.  RR+ )  ->  -.  ( B  +  ( x  / 
2 ) )  <_  B )
8646adantl 454 . . . . . . . . . . . . . . 15  |-  ( ( ( ( A  e.  RR  /\  B  e.  RR )  /\  B  e.  ( ( int `  ( topGen `
 ran  (,) )
) `  ( A [,] B ) ) )  /\  x  e.  RR+ )  ->  x  e.  RR )
8779, 86resubcld 9165 . . . . . . . . . . . . . 14  |-  ( ( ( ( A  e.  RR  /\  B  e.  RR )  /\  B  e.  ( ( int `  ( topGen `
 ran  (,) )
) `  ( A [,] B ) ) )  /\  x  e.  RR+ )  ->  ( B  -  x )  e.  RR )
88 ltsubrp 10338 . . . . . . . . . . . . . . 15  |-  ( ( B  e.  RR  /\  x  e.  RR+ )  -> 
( B  -  x
)  <  B )
8979, 88sylancom 651 . . . . . . . . . . . . . 14  |-  ( ( ( ( A  e.  RR  /\  B  e.  RR )  /\  B  e.  ( ( int `  ( topGen `
 ran  (,) )
) `  ( A [,] B ) ) )  /\  x  e.  RR+ )  ->  ( B  -  x )  <  B
)
9087, 79, 83, 89, 81lttrd 8931 . . . . . . . . . . . . 13  |-  ( ( ( ( A  e.  RR  /\  B  e.  RR )  /\  B  e.  ( ( int `  ( topGen `
 ran  (,) )
) `  ( A [,] B ) ) )  /\  x  e.  RR+ )  ->  ( B  -  x )  <  ( B  +  ( x  /  2 ) ) )
9148adantl 454 . . . . . . . . . . . . . 14  |-  ( ( ( ( A  e.  RR  /\  B  e.  RR )  /\  B  e.  ( ( int `  ( topGen `
 ran  (,) )
) `  ( A [,] B ) ) )  /\  x  e.  RR+ )  ->  ( x  / 
2 )  <  x
)
9282, 86, 79, 91ltadd2dd 8929 . . . . . . . . . . . . 13  |-  ( ( ( ( A  e.  RR  /\  B  e.  RR )  /\  B  e.  ( ( int `  ( topGen `
 ran  (,) )
) `  ( A [,] B ) ) )  /\  x  e.  RR+ )  ->  ( B  +  ( x  /  2
) )  <  ( B  +  x )
)
9387rexrd 8835 . . . . . . . . . . . . . 14  |-  ( ( ( ( A  e.  RR  /\  B  e.  RR )  /\  B  e.  ( ( int `  ( topGen `
 ran  (,) )
) `  ( A [,] B ) ) )  /\  x  e.  RR+ )  ->  ( B  -  x )  e.  RR* )
9479, 86readdcld 8816 . . . . . . . . . . . . . . 15  |-  ( ( ( ( A  e.  RR  /\  B  e.  RR )  /\  B  e.  ( ( int `  ( topGen `
 ran  (,) )
) `  ( A [,] B ) ) )  /\  x  e.  RR+ )  ->  ( B  +  x )  e.  RR )
9594rexrd 8835 . . . . . . . . . . . . . 14  |-  ( ( ( ( A  e.  RR  /\  B  e.  RR )  /\  B  e.  ( ( int `  ( topGen `
 ran  (,) )
) `  ( A [,] B ) ) )  /\  x  e.  RR+ )  ->  ( B  +  x )  e.  RR* )
96 elioo2 10649 . . . . . . . . . . . . . 14  |-  ( ( ( 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
) ) ) )
9793, 95, 96syl2anc 645 . . . . . . . . . . . . 13  |-  ( ( ( ( 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
) ) ) )
9883, 90, 92, 97mpbir3and 1140 . . . . . . . . . . . 12  |-  ( ( ( ( A  e.  RR  /\  B  e.  RR )  /\  B  e.  ( ( int `  ( topGen `
 ran  (,) )
) `  ( A [,] B ) ) )  /\  x  e.  RR+ )  ->  ( B  +  ( x  /  2
) )  e.  ( ( B  -  x
) (,) ( B  +  x ) ) )
9931bl2ioo 18246 . . . . . . . . . . . . 13  |-  ( ( B  e.  RR  /\  x  e.  RR )  ->  ( B ( ball `  ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) ) ) x )  =  ( ( B  -  x ) (,) ( B  +  x )
) )
10079, 86, 99syl2anc 645 . . . . . . . . . . . 12  |-  ( ( ( ( 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 ) ) )
10198, 100eleqtrrd 2333 . . . . . . . . . . 11  |-  ( ( ( ( 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 ) )
102 ssel 3135 . . . . . . . . . . 11  |-  ( ( 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 ) ) ) )
103101, 102syl5com 28 . . . . . . . . . 10  |-  ( ( ( ( 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 ) ) ) )
10417ad2antrr 709 . . . . . . . . . . 11  |-  ( ( ( ( A  e.  RR  /\  B  e.  RR )  /\  B  e.  ( ( int `  ( topGen `
 ran  (,) )
) `  ( A [,] B ) ) )  /\  x  e.  RR+ )  ->  ( ( int `  ( topGen `  ran  (,) )
) `  ( A [,] B ) )  C_  ( A [,] B ) )
105104sseld 3140 . . . . . . . . . 10  |-  ( ( ( ( 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 ) ) )
106 elicc2 10667 . . . . . . . . . . . 12  |-  ( ( 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 )
) )
107 simp3 962 . . . . . . . . . . . 12  |-  ( ( ( B  +  ( x  /  2 ) )  e.  RR  /\  A  <_  ( B  +  ( x  /  2
) )  /\  ( B  +  ( x  /  2 ) )  <_  B )  -> 
( B  +  ( x  /  2 ) )  <_  B )
108106, 107syl6bi 221 . . . . . . . . . . 11  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( ( B  +  ( x  /  2
) )  e.  ( A [,] B )  ->  ( B  +  ( x  /  2
) )  <_  B
) )
109108ad2antrr 709 . . . . . . . . . 10  |-  ( ( ( ( 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 ) )
110103, 105, 1093syld 53 . . . . . . . . 9  |-  ( ( ( ( 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
) )
11185, 110mtod 170 . . . . . . . 8  |-  ( ( ( ( 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 ) ) )
112111nrexdv 2619 . . . . . . 7  |-  ( ( ( 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 ) ) )
11378, 112pm2.65da 562 . . . . . 6  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  -.  B  e.  ( ( int `  ( topGen `
 ran  (,) )
) `  ( A [,] B ) ) )
114 eleq1 2316 . . . . . . . 8  |-  ( x  =  A  ->  (
x  e.  ( ( int `  ( topGen ` 
ran  (,) ) ) `  ( A [,] B ) )  <->  A  e.  (
( int `  ( topGen `
 ran  (,) )
) `  ( A [,] B ) ) ) )
115114notbid 287 . . . . . . 7  |-  ( x  =  A  ->  ( -.  x  e.  (
( int `  ( topGen `
 ran  (,) )
) `  ( A [,] B ) )  <->  -.  A  e.  ( ( int `  ( topGen `
 ran  (,) )
) `  ( A [,] B ) ) ) )
116 eleq1 2316 . . . . . . . 8  |-  ( x  =  B  ->  (
x  e.  ( ( int `  ( topGen ` 
ran  (,) ) ) `  ( A [,] B ) )  <->  B  e.  (
( int `  ( topGen `
 ran  (,) )
) `  ( A [,] B ) ) ) )
117116notbid 287 . . . . . . 7  |-  ( x  =  B  ->  ( -.  x  e.  (
( int `  ( topGen `
 ran  (,) )
) `  ( A [,] B ) )  <->  -.  B  e.  ( ( int `  ( topGen `
 ran  (,) )
) `  ( A [,] B ) ) ) )
118115, 117ralprg 3642 . . . . . 6  |-  ( ( 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 ) ) ) ) )
11975, 113, 118mpbir2and 893 . . . . 5  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  A. x  e.  { A ,  B }  -.  x  e.  (
( int `  ( topGen `
 ran  (,) )
) `  ( A [,] B ) ) )
120 disjr 3457 . . . . 5  |-  ( ( ( ( int `  ( topGen `
 ran  (,) )
) `  ( A [,] B ) )  i^i 
{ A ,  B } )  =  (/)  <->  A. x  e.  { A ,  B }  -.  x  e.  ( ( int `  ( topGen `
 ran  (,) )
) `  ( A [,] B ) ) )
121119, 120sylibr 205 . . . 4  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( ( ( int `  ( topGen `  ran  (,) )
) `  ( A [,] B ) )  i^i 
{ A ,  B } )  =  (/) )
122 disjssun 3473 . . . 4  |-  ( ( ( ( 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 ) ) )
123121, 122syl 17 . . 3  |-  ( ( 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 ) ) )
12428, 123mpbid 203 . 2  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( ( int `  ( topGen `
 ran  (,) )
) `  ( A [,] B ) )  C_  ( A (,) B ) )
125 iooretop 18223 . . . 4  |-  ( A (,) B )  e.  ( topGen `  ran  (,) )
126 ioossicc 10687 . . . 4  |-  ( A (,) B )  C_  ( A [,] B )
12715ssntr 16743 . . . 4  |-  ( ( ( ( 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 ) ) )
128125, 126, 127mpanr12 669 . . 3  |-  ( ( ( topGen `  ran  (,) )  e.  Top  /\  ( A [,] B )  C_  RR )  ->  ( A (,) B )  C_  ( ( int `  ( topGen `
 ran  (,) )
) `  ( A [,] B ) ) )
1297, 14, 128sylancr 647 . 2  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A (,) B
)  C_  ( ( int `  ( topGen `  ran  (,) ) ) `  ( A [,] B ) ) )
130124, 129eqssd 3157 1  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( ( int `  ( topGen `
 ran  (,) )
) `  ( A [,] B ) )  =  ( A (,) B
) )
Colors of variables: wff set class
Syntax hints:   -. wn 5    -> wi 6    <-> wb 178    /\ wa 360    /\ w3a 939    = wceq 1619    e. wcel 1621   A.wral 2516   E.wrex 2517    u. cun 3111    i^i cin 3112    C_ wss 3113   (/)c0 3416   {cpr 3601   class class class wbr 3983    X. cxp 4645   ran crn 4648    |` cres 4649    o. ccom 4651   ` cfv 4659  (class class class)co 5778   RRcr 8690    + caddc 8694   RR*cxr 8820    < clt 8821    <_ cle 8822    - cmin 8991    / cdiv 9377   2c2 9749   RR+crp 10307   (,)cioo 10608   [,]cicc 10611   abscabs 11670   topGenctg 13290   * Metcxmt 16317   ballcbl 16319   MetOpencmopn 16320   Topctop 16579   intcnt 16702
This theorem is referenced by:  rolle  19285  cmvth  19286  mvth  19287  dvlip  19288  dvlipcn  19289  dvlip2  19290  c1liplem1  19291  dvgt0lem1  19297  dvle  19302  lhop1lem  19308  dvcnvrelem1  19312  dvcvx  19315  dvfsumabs  19318  ftc1cn  19338  ftc2  19339  ftc2ditglem  19340  itgparts  19342  itgsubstlem  19343  efcvx  19773  pige3  19833  logccv  19958  lhe4.4ex1a  26899
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-13 1625  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237  ax-rep 4091  ax-sep 4101  ax-nul 4109  ax-pow 4146  ax-pr 4172  ax-un 4470  ax-cnex 8747  ax-resscn 8748  ax-1cn 8749  ax-icn 8750  ax-addcl 8751  ax-addrcl 8752  ax-mulcl 8753  ax-mulrcl 8754  ax-mulcom 8755  ax-addass 8756  ax-mulass 8757  ax-distr 8758  ax-i2m1 8759  ax-1ne0 8760  ax-1rid 8761  ax-rnegex 8762  ax-rrecex 8763  ax-cnre 8764  ax-pre-lttri 8765  ax-pre-lttrn 8766  ax-pre-ltadd 8767  ax-pre-mulgt0 8768  ax-pre-sup 8769
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 940  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-eu 2121  df-mo 2122  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-ne 2421  df-nel 2422  df-ral 2521  df-rex 2522  df-reu 2523  df-rmo 2524  df-rab 2525  df-v 2759  df-sbc 2953  df-csb 3043  df-dif 3116  df-un 3118  df-in 3120  df-ss 3127  df-pss 3129  df-nul 3417  df-if 3526  df-pw 3587  df-sn 3606  df-pr 3607  df-tp 3608  df-op 3609  df-uni 3788  df-iun 3867  df-br 3984  df-opab 4038  df-mpt 4039  df-tr 4074  df-eprel 4263  df-id 4267  df-po 4272  df-so 4273  df-fr 4310  df-we 4312  df-ord 4353  df-on 4354  df-lim 4355  df-suc 4356  df-om 4615  df-xp 4661  df-rel 4662  df-cnv 4663  df-co 4664  df-dm 4665  df-rn 4666  df-res 4667  df-ima 4668  df-fun 4669  df-fn 4670  df-f 4671  df-f1 4672  df-fo 4673  df-f1o 4674  df-fv 4675  df-ov 5781  df-oprab 5782  df-mpt2 5783  df-1st 6042  df-2nd 6043  df-iota 6211  df-riota 6258  df-recs 6342  df-rdg 6377  df-er 6614  df-map 6728  df-en 6818  df-dom 6819  df-sdom 6820  df-sup 7148  df-pnf 8823  df-mnf 8824  df-xr 8825  df-ltxr 8826  df-le 8827  df-sub 8993  df-neg 8994  df-div 9378  df-n 9701  df-2 9758  df-3 9759  df-n0 9919  df-z 9978  df-uz 10184  df-q 10270  df-rp 10308  df-xneg 10405  df-xadd 10406  df-xmul 10407  df-ioo 10612  df-ico 10614  df-icc 10615  df-seq 10999  df-exp 11057  df-cj 11535  df-re 11536  df-im 11537  df-sqr 11671  df-abs 11672  df-topgen 13292  df-xmet 16321  df-met 16322  df-bl 16323  df-mopn 16324  df-top 16584  df-bases 16586  df-topon 16587  df-ntr 16705
  Copyright terms: Public domain W3C validator