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

Theorem iocopnst 21954
Description: A half-open interval ending at  B is open in the closed interval from  A to  B. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 15-Dec-2013.)
Hypothesis
Ref Expression
iocopnst.1  |-  J  =  ( MetOpen `  ( ( abs  o.  -  )  |`  ( ( A [,] B )  X.  ( A [,] B ) ) ) )
Assertion
Ref Expression
iocopnst  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( C  e.  ( A [,) B )  ->  ( C (,] B )  e.  J
) )

Proof of Theorem iocopnst
Dummy variable  v is distinct from all other variables.
StepHypRef Expression
1 iooretop 21772 . . . . 5  |-  ( C (,) ( B  + 
1 ) )  e.  ( topGen `  ran  (,) )
2 simp1 1005 . . . . . . . . . . 11  |-  ( ( v  e.  RR  /\  C  <  v  /\  v  <_  B )  ->  v  e.  RR )
32a1i 11 . . . . . . . . . 10  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  C  e.  ( A [,) B ) )  ->  ( (
v  e.  RR  /\  C  <  v  /\  v  <_  B )  ->  v  e.  RR ) )
4 simp2 1006 . . . . . . . . . . 11  |-  ( ( v  e.  RR  /\  C  <  v  /\  v  <_  B )  ->  C  <  v )
54a1i 11 . . . . . . . . . 10  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  C  e.  ( A [,) B ) )  ->  ( (
v  e.  RR  /\  C  <  v  /\  v  <_  B )  ->  C  <  v ) )
6 ltp1 10443 . . . . . . . . . . . . . . . 16  |-  ( B  e.  RR  ->  B  <  ( B  +  1 ) )
76adantr 466 . . . . . . . . . . . . . . 15  |-  ( ( B  e.  RR  /\  v  e.  RR )  ->  B  <  ( B  +  1 ) )
8 peano2re 9806 . . . . . . . . . . . . . . . . 17  |-  ( B  e.  RR  ->  ( B  +  1 )  e.  RR )
98adantr 466 . . . . . . . . . . . . . . . 16  |-  ( ( B  e.  RR  /\  v  e.  RR )  ->  ( B  +  1 )  e.  RR )
10 lelttr 9724 . . . . . . . . . . . . . . . . . . 19  |-  ( ( v  e.  RR  /\  B  e.  RR  /\  ( B  +  1 )  e.  RR )  -> 
( ( v  <_  B  /\  B  <  ( B  +  1 ) )  ->  v  <  ( B  +  1 ) ) )
11103expa 1205 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( v  e.  RR  /\  B  e.  RR )  /\  ( B  + 
1 )  e.  RR )  ->  ( ( v  <_  B  /\  B  <  ( B  +  1 ) )  ->  v  <  ( B  +  1 ) ) )
1211ancom1s 812 . . . . . . . . . . . . . . . . 17  |-  ( ( ( B  e.  RR  /\  v  e.  RR )  /\  ( B  + 
1 )  e.  RR )  ->  ( ( v  <_  B  /\  B  <  ( B  +  1 ) )  ->  v  <  ( B  +  1 ) ) )
1312ancomsd 455 . . . . . . . . . . . . . . . 16  |-  ( ( ( B  e.  RR  /\  v  e.  RR )  /\  ( B  + 
1 )  e.  RR )  ->  ( ( B  <  ( B  + 
1 )  /\  v  <_  B )  ->  v  <  ( B  +  1 ) ) )
149, 13mpdan 672 . . . . . . . . . . . . . . 15  |-  ( ( B  e.  RR  /\  v  e.  RR )  ->  ( ( B  < 
( B  +  1 )  /\  v  <_  B )  ->  v  <  ( B  +  1 ) ) )
157, 14mpand 679 . . . . . . . . . . . . . 14  |-  ( ( B  e.  RR  /\  v  e.  RR )  ->  ( v  <_  B  ->  v  <  ( B  +  1 ) ) )
1615impr 623 . . . . . . . . . . . . 13  |-  ( ( B  e.  RR  /\  ( v  e.  RR  /\  v  <_  B )
)  ->  v  <  ( B  +  1 ) )
17163adantr2 1165 . . . . . . . . . . . 12  |-  ( ( B  e.  RR  /\  ( v  e.  RR  /\  C  <  v  /\  v  <_  B ) )  ->  v  <  ( B  +  1 ) )
1817ex 435 . . . . . . . . . . 11  |-  ( B  e.  RR  ->  (
( v  e.  RR  /\  C  <  v  /\  v  <_  B )  -> 
v  <  ( B  +  1 ) ) )
1918ad2antlr 731 . . . . . . . . . 10  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  C  e.  ( A [,) B ) )  ->  ( (
v  e.  RR  /\  C  <  v  /\  v  <_  B )  ->  v  <  ( B  +  1 ) ) )
203, 5, 193jcad 1186 . . . . . . . . 9  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  C  e.  ( A [,) B ) )  ->  ( (
v  e.  RR  /\  C  <  v  /\  v  <_  B )  ->  (
v  e.  RR  /\  C  <  v  /\  v  <  ( B  +  1 ) ) ) )
21 rexr 9686 . . . . . . . . . . . . 13  |-  ( B  e.  RR  ->  B  e.  RR* )
22 elico2 11698 . . . . . . . . . . . . 13  |-  ( ( A  e.  RR  /\  B  e.  RR* )  -> 
( C  e.  ( A [,) B )  <-> 
( C  e.  RR  /\  A  <_  C  /\  C  <  B ) ) )
2321, 22sylan2 476 . . . . . . . . . . . 12  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( C  e.  ( A [,) B )  <-> 
( C  e.  RR  /\  A  <_  C  /\  C  <  B ) ) )
2423biimpa 486 . . . . . . . . . . 11  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  C  e.  ( A [,) B ) )  ->  ( C  e.  RR  /\  A  <_  C  /\  C  <  B
) )
25 lelttr 9724 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( A  e.  RR  /\  C  e.  RR  /\  v  e.  RR )  ->  (
( A  <_  C  /\  C  <  v )  ->  A  <  v
) )
26 ltle 9722 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( A  e.  RR  /\  v  e.  RR )  ->  ( A  <  v  ->  A  <_  v )
)
27263adant2 1024 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( A  e.  RR  /\  C  e.  RR  /\  v  e.  RR )  ->  ( A  <  v  ->  A  <_  v ) )
2825, 27syld 45 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A  e.  RR  /\  C  e.  RR  /\  v  e.  RR )  ->  (
( A  <_  C  /\  C  <  v )  ->  A  <_  v
) )
29283expa 1205 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( A  e.  RR  /\  C  e.  RR )  /\  v  e.  RR )  ->  ( ( A  <_  C  /\  C  <  v )  ->  A  <_  v ) )
3029imp 430 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( A  e.  RR  /\  C  e.  RR )  /\  v  e.  RR )  /\  ( A  <_  C  /\  C  <  v ) )  ->  A  <_  v )
3130an4s 833 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( A  e.  RR  /\  C  e.  RR )  /\  A  <_  C )  /\  (
v  e.  RR  /\  C  <  v ) )  ->  A  <_  v
)
32313adantr3 1166 . . . . . . . . . . . . . . 15  |-  ( ( ( ( A  e.  RR  /\  C  e.  RR )  /\  A  <_  C )  /\  (
v  e.  RR  /\  C  <  v  /\  v  <_  B ) )  ->  A  <_  v )
3332ex 435 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  RR  /\  C  e.  RR )  /\  A  <_  C
)  ->  ( (
v  e.  RR  /\  C  <  v  /\  v  <_  B )  ->  A  <_  v ) )
3433anasss 651 . . . . . . . . . . . . 13  |-  ( ( A  e.  RR  /\  ( C  e.  RR  /\  A  <_  C )
)  ->  ( (
v  e.  RR  /\  C  <  v  /\  v  <_  B )  ->  A  <_  v ) )
35343adantr3 1166 . . . . . . . . . . . 12  |-  ( ( A  e.  RR  /\  ( C  e.  RR  /\  A  <_  C  /\  C  <  B ) )  ->  ( ( v  e.  RR  /\  C  <  v  /\  v  <_  B )  ->  A  <_  v ) )
3635adantlr 719 . . . . . . . . . . 11  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  ( C  e.  RR  /\  A  <_  C  /\  C  <  B
) )  ->  (
( v  e.  RR  /\  C  <  v  /\  v  <_  B )  ->  A  <_  v ) )
3724, 36syldan 472 . . . . . . . . . 10  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  C  e.  ( A [,) B ) )  ->  ( (
v  e.  RR  /\  C  <  v  /\  v  <_  B )  ->  A  <_  v ) )
38 simp3 1007 . . . . . . . . . . 11  |-  ( ( v  e.  RR  /\  C  <  v  /\  v  <_  B )  ->  v  <_  B )
3938a1i 11 . . . . . . . . . 10  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  C  e.  ( A [,) B ) )  ->  ( (
v  e.  RR  /\  C  <  v  /\  v  <_  B )  ->  v  <_  B ) )
403, 37, 393jcad 1186 . . . . . . . . 9  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  C  e.  ( A [,) B ) )  ->  ( (
v  e.  RR  /\  C  <  v  /\  v  <_  B )  ->  (
v  e.  RR  /\  A  <_  v  /\  v  <_  B ) ) )
4120, 40jcad 535 . . . . . . . 8  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  C  e.  ( A [,) B ) )  ->  ( (
v  e.  RR  /\  C  <  v  /\  v  <_  B )  ->  (
( v  e.  RR  /\  C  <  v  /\  v  <  ( B  + 
1 ) )  /\  ( v  e.  RR  /\  A  <_  v  /\  v  <_  B ) ) ) )
42 simpl1 1008 . . . . . . . . 9  |-  ( ( ( v  e.  RR  /\  C  <  v  /\  v  <  ( B  + 
1 ) )  /\  ( v  e.  RR  /\  A  <_  v  /\  v  <_  B ) )  ->  v  e.  RR )
43 simpl2 1009 . . . . . . . . 9  |-  ( ( ( v  e.  RR  /\  C  <  v  /\  v  <  ( B  + 
1 ) )  /\  ( v  e.  RR  /\  A  <_  v  /\  v  <_  B ) )  ->  C  <  v
)
44 simpr3 1013 . . . . . . . . 9  |-  ( ( ( v  e.  RR  /\  C  <  v  /\  v  <  ( B  + 
1 ) )  /\  ( v  e.  RR  /\  A  <_  v  /\  v  <_  B ) )  ->  v  <_  B
)
4542, 43, 443jca 1185 . . . . . . . 8  |-  ( ( ( v  e.  RR  /\  C  <  v  /\  v  <  ( B  + 
1 ) )  /\  ( v  e.  RR  /\  A  <_  v  /\  v  <_  B ) )  ->  ( v  e.  RR  /\  C  < 
v  /\  v  <_  B ) )
4641, 45impbid1 206 . . . . . . 7  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  C  e.  ( A [,) B ) )  ->  ( (
v  e.  RR  /\  C  <  v  /\  v  <_  B )  <->  ( (
v  e.  RR  /\  C  <  v  /\  v  <  ( B  +  1 ) )  /\  (
v  e.  RR  /\  A  <_  v  /\  v  <_  B ) ) ) )
4724simp1d 1017 . . . . . . . . 9  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  C  e.  ( A [,) B ) )  ->  C  e.  RR )
48 rexr 9686 . . . . . . . . 9  |-  ( C  e.  RR  ->  C  e.  RR* )
4947, 48syl 17 . . . . . . . 8  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  C  e.  ( A [,) B ) )  ->  C  e.  RR* )
50 simplr 760 . . . . . . . 8  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  C  e.  ( A [,) B ) )  ->  B  e.  RR )
51 elioc2 11697 . . . . . . . 8  |-  ( ( C  e.  RR*  /\  B  e.  RR )  ->  (
v  e.  ( C (,] B )  <->  ( v  e.  RR  /\  C  < 
v  /\  v  <_  B ) ) )
5249, 50, 51syl2anc 665 . . . . . . 7  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  C  e.  ( A [,) B ) )  ->  ( v  e.  ( C (,] B
)  <->  ( v  e.  RR  /\  C  < 
v  /\  v  <_  B ) ) )
53 elin 3649 . . . . . . . 8  |-  ( v  e.  ( ( C (,) ( B  + 
1 ) )  i^i  ( A [,] B
) )  <->  ( v  e.  ( C (,) ( B  +  1 ) )  /\  v  e.  ( A [,] B
) ) )
54 rexr 9686 . . . . . . . . . . . 12  |-  ( ( B  +  1 )  e.  RR  ->  ( B  +  1 )  e.  RR* )
558, 54syl 17 . . . . . . . . . . 11  |-  ( B  e.  RR  ->  ( B  +  1 )  e.  RR* )
5655ad2antlr 731 . . . . . . . . . 10  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  C  e.  ( A [,) B ) )  ->  ( B  +  1 )  e. 
RR* )
57 elioo2 11677 . . . . . . . . . 10  |-  ( ( C  e.  RR*  /\  ( B  +  1 )  e.  RR* )  ->  (
v  e.  ( C (,) ( B  + 
1 ) )  <->  ( v  e.  RR  /\  C  < 
v  /\  v  <  ( B  +  1 ) ) ) )
5849, 56, 57syl2anc 665 . . . . . . . . 9  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  C  e.  ( A [,) B ) )  ->  ( v  e.  ( C (,) ( B  +  1 ) )  <->  ( v  e.  RR  /\  C  < 
v  /\  v  <  ( B  +  1 ) ) ) )
59 elicc2 11699 . . . . . . . . . 10  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( v  e.  ( A [,] B )  <-> 
( v  e.  RR  /\  A  <_  v  /\  v  <_  B ) ) )
6059adantr 466 . . . . . . . . 9  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  C  e.  ( A [,) B ) )  ->  ( v  e.  ( A [,] B
)  <->  ( v  e.  RR  /\  A  <_ 
v  /\  v  <_  B ) ) )
6158, 60anbi12d 715 . . . . . . . 8  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  C  e.  ( A [,) B ) )  ->  ( (
v  e.  ( C (,) ( B  + 
1 ) )  /\  v  e.  ( A [,] B ) )  <->  ( (
v  e.  RR  /\  C  <  v  /\  v  <  ( B  +  1 ) )  /\  (
v  e.  RR  /\  A  <_  v  /\  v  <_  B ) ) ) )
6253, 61syl5bb 260 . . . . . . 7  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  C  e.  ( A [,) B ) )  ->  ( v  e.  ( ( C (,) ( B  +  1
) )  i^i  ( A [,] B ) )  <-> 
( ( v  e.  RR  /\  C  < 
v  /\  v  <  ( B  +  1 ) )  /\  ( v  e.  RR  /\  A  <_  v  /\  v  <_  B ) ) ) )
6346, 52, 623bitr4d 288 . . . . . 6  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  C  e.  ( A [,) B ) )  ->  ( v  e.  ( C (,] B
)  <->  v  e.  ( ( C (,) ( B  +  1 ) )  i^i  ( A [,] B ) ) ) )
6463eqrdv 2419 . . . . 5  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  C  e.  ( A [,) B ) )  ->  ( C (,] B )  =  ( ( C (,) ( B  +  1 ) )  i^i  ( A [,] B ) ) )
65 ineq1 3657 . . . . . . 7  |-  ( v  =  ( C (,) ( B  +  1
) )  ->  (
v  i^i  ( A [,] B ) )  =  ( ( C (,) ( B  +  1
) )  i^i  ( A [,] B ) ) )
6665eqeq2d 2436 . . . . . 6  |-  ( v  =  ( C (,) ( B  +  1
) )  ->  (
( C (,] B
)  =  ( v  i^i  ( A [,] B ) )  <->  ( C (,] B )  =  ( ( C (,) ( B  +  1 ) )  i^i  ( A [,] B ) ) ) )
6766rspcev 3182 . . . . 5  |-  ( ( ( C (,) ( B  +  1 ) )  e.  ( topGen ` 
ran  (,) )  /\  ( C (,] B )  =  ( ( C (,) ( B  +  1
) )  i^i  ( A [,] B ) ) )  ->  E. v  e.  ( topGen `  ran  (,) )
( C (,] B
)  =  ( v  i^i  ( A [,] B ) ) )
681, 64, 67sylancr 667 . . . 4  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  C  e.  ( A [,) B ) )  ->  E. v  e.  ( topGen `  ran  (,) )
( C (,] B
)  =  ( v  i^i  ( A [,] B ) ) )
69 retop 21768 . . . . 5  |-  ( topGen ` 
ran  (,) )  e.  Top
70 ovex 6329 . . . . 5  |-  ( A [,] B )  e. 
_V
71 elrest 15313 . . . . 5  |-  ( ( ( topGen `  ran  (,) )  e.  Top  /\  ( A [,] B )  e. 
_V )  ->  (
( C (,] B
)  e.  ( (
topGen `  ran  (,) )t  ( A [,] B ) )  <->  E. v  e.  ( topGen `
 ran  (,) )
( C (,] B
)  =  ( v  i^i  ( A [,] B ) ) ) )
7269, 70, 71mp2an 676 . . . 4  |-  ( ( C (,] B )  e.  ( ( topGen ` 
ran  (,) )t  ( A [,] B ) )  <->  E. v  e.  ( topGen `  ran  (,) )
( C (,] B
)  =  ( v  i^i  ( A [,] B ) ) )
7368, 72sylibr 215 . . 3  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  C  e.  ( A [,) B ) )  ->  ( C (,] B )  e.  ( ( topGen `  ran  (,) )t  ( A [,] B ) ) )
74 iccssre 11716 . . . . 5  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A [,] B
)  C_  RR )
7574adantr 466 . . . 4  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  C  e.  ( A [,) B ) )  ->  ( A [,] B )  C_  RR )
76 eqid 2422 . . . . 5  |-  ( topGen ` 
ran  (,) )  =  (
topGen `  ran  (,) )
77 iocopnst.1 . . . . 5  |-  J  =  ( MetOpen `  ( ( abs  o.  -  )  |`  ( ( A [,] B )  X.  ( A [,] B ) ) ) )
7876, 77resubmet 21806 . . . 4  |-  ( ( A [,] B ) 
C_  RR  ->  J  =  ( ( topGen `  ran  (,) )t  ( A [,] B
) ) )
7975, 78syl 17 . . 3  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  C  e.  ( A [,) B ) )  ->  J  =  ( ( topGen `  ran  (,) )t  ( A [,] B
) ) )
8073, 79eleqtrrd 2513 . 2  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  C  e.  ( A [,) B ) )  ->  ( C (,] B )  e.  J
)
8180ex 435 1  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( C  e.  ( A [,) B )  ->  ( C (,] B )  e.  J
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    /\ wa 370    /\ w3a 982    = wceq 1437    e. wcel 1868   E.wrex 2776   _Vcvv 3081    i^i cin 3435    C_ wss 3436   class class class wbr 4420    X. cxp 4847   ran crn 4850    |` cres 4851    o. ccom 4853   ` cfv 5597  (class class class)co 6301   RRcr 9538   1c1 9540    + caddc 9542   RR*cxr 9674    < clt 9675    <_ cle 9676    - cmin 9860   (,)cioo 11635   (,]cioc 11636   [,)cico 11637   [,]cicc 11638   abscabs 13285   ↾t crest 15306   topGenctg 15323   MetOpencmopn 18947   Topctop 19903
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-rep 4533  ax-sep 4543  ax-nul 4551  ax-pow 4598  ax-pr 4656  ax-un 6593  ax-cnex 9595  ax-resscn 9596  ax-1cn 9597  ax-icn 9598  ax-addcl 9599  ax-addrcl 9600  ax-mulcl 9601  ax-mulrcl 9602  ax-mulcom 9603  ax-addass 9604  ax-mulass 9605  ax-distr 9606  ax-i2m1 9607  ax-1ne0 9608  ax-1rid 9609  ax-rnegex 9610  ax-rrecex 9611  ax-cnre 9612  ax-pre-lttri 9613  ax-pre-lttrn 9614  ax-pre-ltadd 9615  ax-pre-mulgt0 9616  ax-pre-sup 9617
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-nel 2621  df-ral 2780  df-rex 2781  df-reu 2782  df-rmo 2783  df-rab 2784  df-v 3083  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-tp 4001  df-op 4003  df-uni 4217  df-iun 4298  df-br 4421  df-opab 4480  df-mpt 4481  df-tr 4516  df-eprel 4760  df-id 4764  df-po 4770  df-so 4771  df-fr 4808  df-we 4810  df-xp 4855  df-rel 4856  df-cnv 4857  df-co 4858  df-dm 4859  df-rn 4860  df-res 4861  df-ima 4862  df-pred 5395  df-ord 5441  df-on 5442  df-lim 5443  df-suc 5444  df-iota 5561  df-fun 5599  df-fn 5600  df-f 5601  df-f1 5602  df-fo 5603  df-f1o 5604  df-fv 5605  df-riota 6263  df-ov 6304  df-oprab 6305  df-mpt2 6306  df-om 6703  df-1st 6803  df-2nd 6804  df-wrecs 7032  df-recs 7094  df-rdg 7132  df-er 7367  df-map 7478  df-en 7574  df-dom 7575  df-sdom 7576  df-sup 7958  df-inf 7959  df-pnf 9677  df-mnf 9678  df-xr 9679  df-ltxr 9680  df-le 9681  df-sub 9862  df-neg 9863  df-div 10270  df-nn 10610  df-2 10668  df-3 10669  df-n0 10870  df-z 10938  df-uz 11160  df-q 11265  df-rp 11303  df-xneg 11409  df-xadd 11410  df-xmul 11411  df-ioo 11639  df-ioc 11640  df-ico 11641  df-icc 11642  df-seq 12213  df-exp 12272  df-cj 13150  df-re 13151  df-im 13152  df-sqrt 13286  df-abs 13287  df-rest 15308  df-topgen 15329  df-psmet 18949  df-xmet 18950  df-met 18951  df-bl 18952  df-mopn 18953  df-top 19907  df-bases 19908  df-topon 19909
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator