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

Theorem tgqioo 21811
Description: The topology generated by open intervals of reals with rational endpoints is the same as the open sets of the standard metric space on the reals. In particular, this proves that the standard topology on the reals is second-countable. (Contributed by Mario Carneiro, 17-Jun-2014.)
Hypothesis
Ref Expression
tgqioo.1  |-  Q  =  ( topGen `  ( (,) " ( QQ  X.  QQ ) ) )
Assertion
Ref Expression
tgqioo  |-  ( topGen ` 
ran  (,) )  =  Q

Proof of Theorem tgqioo
Dummy variables  v  u  w  x  y 
z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 tgqioo.1 . 2  |-  Q  =  ( topGen `  ( (,) " ( QQ  X.  QQ ) ) )
2 imassrn 5178 . . 3  |-  ( (,) " ( QQ  X.  QQ ) )  C_  ran  (,)
3 ioof 11729 . . . . . 6  |-  (,) :
( RR*  X.  RR* ) --> ~P RR
4 ffn 5726 . . . . . 6  |-  ( (,)
: ( RR*  X.  RR* )
--> ~P RR  ->  (,)  Fn  ( RR*  X.  RR* )
)
53, 4ax-mp 5 . . . . 5  |-  (,)  Fn  ( RR*  X.  RR* )
6 simpll 759 . . . . . . . . . 10  |-  ( ( ( x  e.  RR*  /\  y  e.  RR* )  /\  z  e.  (
x (,) y ) )  ->  x  e.  RR* )
7 elioo1 11673 . . . . . . . . . . . 12  |-  ( ( x  e.  RR*  /\  y  e.  RR* )  ->  (
z  e.  ( x (,) y )  <->  ( z  e.  RR*  /\  x  < 
z  /\  z  <  y ) ) )
87biimpa 487 . . . . . . . . . . 11  |-  ( ( ( x  e.  RR*  /\  y  e.  RR* )  /\  z  e.  (
x (,) y ) )  ->  ( z  e.  RR*  /\  x  < 
z  /\  z  <  y ) )
98simp1d 1019 . . . . . . . . . 10  |-  ( ( ( x  e.  RR*  /\  y  e.  RR* )  /\  z  e.  (
x (,) y ) )  ->  z  e.  RR* )
108simp2d 1020 . . . . . . . . . 10  |-  ( ( ( x  e.  RR*  /\  y  e.  RR* )  /\  z  e.  (
x (,) y ) )  ->  x  <  z )
11 qbtwnxr 11490 . . . . . . . . . 10  |-  ( ( x  e.  RR*  /\  z  e.  RR*  /\  x  < 
z )  ->  E. u  e.  QQ  ( x  < 
u  /\  u  <  z ) )
126, 9, 10, 11syl3anc 1267 . . . . . . . . 9  |-  ( ( ( x  e.  RR*  /\  y  e.  RR* )  /\  z  e.  (
x (,) y ) )  ->  E. u  e.  QQ  ( x  < 
u  /\  u  <  z ) )
13 simplr 761 . . . . . . . . . 10  |-  ( ( ( x  e.  RR*  /\  y  e.  RR* )  /\  z  e.  (
x (,) y ) )  ->  y  e.  RR* )
148simp3d 1021 . . . . . . . . . 10  |-  ( ( ( x  e.  RR*  /\  y  e.  RR* )  /\  z  e.  (
x (,) y ) )  ->  z  <  y )
15 qbtwnxr 11490 . . . . . . . . . 10  |-  ( ( z  e.  RR*  /\  y  e.  RR*  /\  z  < 
y )  ->  E. v  e.  QQ  ( z  < 
v  /\  v  <  y ) )
169, 13, 14, 15syl3anc 1267 . . . . . . . . 9  |-  ( ( ( x  e.  RR*  /\  y  e.  RR* )  /\  z  e.  (
x (,) y ) )  ->  E. v  e.  QQ  ( z  < 
v  /\  v  <  y ) )
17 reeanv 2957 . . . . . . . . . 10  |-  ( E. u  e.  QQ  E. v  e.  QQ  (
( x  <  u  /\  u  <  z )  /\  ( z  < 
v  /\  v  <  y ) )  <->  ( E. u  e.  QQ  (
x  <  u  /\  u  <  z )  /\  E. v  e.  QQ  (
z  <  v  /\  v  <  y ) ) )
18 df-ov 6291 . . . . . . . . . . . . . 14  |-  ( u (,) v )  =  ( (,) `  <. u ,  v >. )
19 opelxpi 4865 . . . . . . . . . . . . . . . 16  |-  ( ( u  e.  QQ  /\  v  e.  QQ )  -> 
<. u ,  v >.  e.  ( QQ  X.  QQ ) )
20193ad2ant2 1029 . . . . . . . . . . . . . . 15  |-  ( ( ( ( x  e. 
RR*  /\  y  e.  RR* )  /\  z  e.  ( x (,) y
) )  /\  (
u  e.  QQ  /\  v  e.  QQ )  /\  ( ( x  < 
u  /\  u  <  z )  /\  ( z  <  v  /\  v  <  y ) ) )  ->  <. u ,  v
>.  e.  ( QQ  X.  QQ ) )
21 ffun 5729 . . . . . . . . . . . . . . . . 17  |-  ( (,)
: ( RR*  X.  RR* )
--> ~P RR  ->  Fun  (,) )
223, 21ax-mp 5 . . . . . . . . . . . . . . . 16  |-  Fun  (,)
23 qssre 11271 . . . . . . . . . . . . . . . . . . 19  |-  QQ  C_  RR
24 ressxr 9681 . . . . . . . . . . . . . . . . . . 19  |-  RR  C_  RR*
2523, 24sstri 3440 . . . . . . . . . . . . . . . . . 18  |-  QQ  C_  RR*
26 xpss12 4939 . . . . . . . . . . . . . . . . . 18  |-  ( ( QQ  C_  RR*  /\  QQ  C_ 
RR* )  ->  ( QQ  X.  QQ )  C_  ( RR*  X.  RR* )
)
2725, 25, 26mp2an 677 . . . . . . . . . . . . . . . . 17  |-  ( QQ 
X.  QQ )  C_  ( RR*  X.  RR* )
283fdmi 5732 . . . . . . . . . . . . . . . . 17  |-  dom  (,)  =  ( RR*  X.  RR* )
2927, 28sseqtr4i 3464 . . . . . . . . . . . . . . . 16  |-  ( QQ 
X.  QQ )  C_  dom  (,)
30 funfvima2 6139 . . . . . . . . . . . . . . . 16  |-  ( ( Fun  (,)  /\  ( QQ  X.  QQ )  C_  dom  (,) )  ->  ( <. u ,  v >.  e.  ( QQ  X.  QQ )  ->  ( (,) `  <. u ,  v >. )  e.  ( (,) " ( QQ  X.  QQ ) ) ) )
3122, 29, 30mp2an 677 . . . . . . . . . . . . . . 15  |-  ( <.
u ,  v >.  e.  ( QQ  X.  QQ )  ->  ( (,) `  <. u ,  v >. )  e.  ( (,) " ( QQ  X.  QQ ) ) )
3220, 31syl 17 . . . . . . . . . . . . . 14  |-  ( ( ( ( x  e. 
RR*  /\  y  e.  RR* )  /\  z  e.  ( x (,) y
) )  /\  (
u  e.  QQ  /\  v  e.  QQ )  /\  ( ( x  < 
u  /\  u  <  z )  /\  ( z  <  v  /\  v  <  y ) ) )  ->  ( (,) `  <. u ,  v >. )  e.  ( (,) " ( QQ  X.  QQ ) ) )
3318, 32syl5eqel 2532 . . . . . . . . . . . . 13  |-  ( ( ( ( x  e. 
RR*  /\  y  e.  RR* )  /\  z  e.  ( x (,) y
) )  /\  (
u  e.  QQ  /\  v  e.  QQ )  /\  ( ( x  < 
u  /\  u  <  z )  /\  ( z  <  v  /\  v  <  y ) ) )  ->  ( u (,) v )  e.  ( (,) " ( QQ 
X.  QQ ) ) )
3493ad2ant1 1028 . . . . . . . . . . . . . 14  |-  ( ( ( ( x  e. 
RR*  /\  y  e.  RR* )  /\  z  e.  ( x (,) y
) )  /\  (
u  e.  QQ  /\  v  e.  QQ )  /\  ( ( x  < 
u  /\  u  <  z )  /\  ( z  <  v  /\  v  <  y ) ) )  ->  z  e.  RR* )
35 simp3lr 1079 . . . . . . . . . . . . . 14  |-  ( ( ( ( x  e. 
RR*  /\  y  e.  RR* )  /\  z  e.  ( x (,) y
) )  /\  (
u  e.  QQ  /\  v  e.  QQ )  /\  ( ( x  < 
u  /\  u  <  z )  /\  ( z  <  v  /\  v  <  y ) ) )  ->  u  <  z
)
36 simp3rl 1080 . . . . . . . . . . . . . 14  |-  ( ( ( ( x  e. 
RR*  /\  y  e.  RR* )  /\  z  e.  ( x (,) y
) )  /\  (
u  e.  QQ  /\  v  e.  QQ )  /\  ( ( x  < 
u  /\  u  <  z )  /\  ( z  <  v  /\  v  <  y ) ) )  ->  z  <  v
)
37 simp2l 1033 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( x  e. 
RR*  /\  y  e.  RR* )  /\  z  e.  ( x (,) y
) )  /\  (
u  e.  QQ  /\  v  e.  QQ )  /\  ( ( x  < 
u  /\  u  <  z )  /\  ( z  <  v  /\  v  <  y ) ) )  ->  u  e.  QQ )
3825, 37sseldi 3429 . . . . . . . . . . . . . . 15  |-  ( ( ( ( x  e. 
RR*  /\  y  e.  RR* )  /\  z  e.  ( x (,) y
) )  /\  (
u  e.  QQ  /\  v  e.  QQ )  /\  ( ( x  < 
u  /\  u  <  z )  /\  ( z  <  v  /\  v  <  y ) ) )  ->  u  e.  RR* )
39 simp2r 1034 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( x  e. 
RR*  /\  y  e.  RR* )  /\  z  e.  ( x (,) y
) )  /\  (
u  e.  QQ  /\  v  e.  QQ )  /\  ( ( x  < 
u  /\  u  <  z )  /\  ( z  <  v  /\  v  <  y ) ) )  ->  v  e.  QQ )
4025, 39sseldi 3429 . . . . . . . . . . . . . . 15  |-  ( ( ( ( x  e. 
RR*  /\  y  e.  RR* )  /\  z  e.  ( x (,) y
) )  /\  (
u  e.  QQ  /\  v  e.  QQ )  /\  ( ( x  < 
u  /\  u  <  z )  /\  ( z  <  v  /\  v  <  y ) ) )  ->  v  e.  RR* )
41 elioo1 11673 . . . . . . . . . . . . . . 15  |-  ( ( u  e.  RR*  /\  v  e.  RR* )  ->  (
z  e.  ( u (,) v )  <->  ( z  e.  RR*  /\  u  < 
z  /\  z  <  v ) ) )
4238, 40, 41syl2anc 666 . . . . . . . . . . . . . 14  |-  ( ( ( ( x  e. 
RR*  /\  y  e.  RR* )  /\  z  e.  ( x (,) y
) )  /\  (
u  e.  QQ  /\  v  e.  QQ )  /\  ( ( x  < 
u  /\  u  <  z )  /\  ( z  <  v  /\  v  <  y ) ) )  ->  ( z  e.  ( u (,) v
)  <->  ( z  e. 
RR*  /\  u  <  z  /\  z  <  v
) ) )
4334, 35, 36, 42mpbir3and 1190 . . . . . . . . . . . . 13  |-  ( ( ( ( x  e. 
RR*  /\  y  e.  RR* )  /\  z  e.  ( x (,) y
) )  /\  (
u  e.  QQ  /\  v  e.  QQ )  /\  ( ( x  < 
u  /\  u  <  z )  /\  ( z  <  v  /\  v  <  y ) ) )  ->  z  e.  ( u (,) v ) )
4463ad2ant1 1028 . . . . . . . . . . . . . . 15  |-  ( ( ( ( x  e. 
RR*  /\  y  e.  RR* )  /\  z  e.  ( x (,) y
) )  /\  (
u  e.  QQ  /\  v  e.  QQ )  /\  ( ( x  < 
u  /\  u  <  z )  /\  ( z  <  v  /\  v  <  y ) ) )  ->  x  e.  RR* )
45 simp3ll 1078 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( x  e. 
RR*  /\  y  e.  RR* )  /\  z  e.  ( x (,) y
) )  /\  (
u  e.  QQ  /\  v  e.  QQ )  /\  ( ( x  < 
u  /\  u  <  z )  /\  ( z  <  v  /\  v  <  y ) ) )  ->  x  <  u
)
46 xrltle 11445 . . . . . . . . . . . . . . . . 17  |-  ( ( x  e.  RR*  /\  u  e.  RR* )  ->  (
x  <  u  ->  x  <_  u ) )
4744, 38, 46syl2anc 666 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( x  e. 
RR*  /\  y  e.  RR* )  /\  z  e.  ( x (,) y
) )  /\  (
u  e.  QQ  /\  v  e.  QQ )  /\  ( ( x  < 
u  /\  u  <  z )  /\  ( z  <  v  /\  v  <  y ) ) )  ->  ( x  < 
u  ->  x  <_  u ) )
4845, 47mpd 15 . . . . . . . . . . . . . . 15  |-  ( ( ( ( x  e. 
RR*  /\  y  e.  RR* )  /\  z  e.  ( x (,) y
) )  /\  (
u  e.  QQ  /\  v  e.  QQ )  /\  ( ( x  < 
u  /\  u  <  z )  /\  ( z  <  v  /\  v  <  y ) ) )  ->  x  <_  u
)
49 iooss1 11668 . . . . . . . . . . . . . . 15  |-  ( ( x  e.  RR*  /\  x  <_  u )  ->  (
u (,) v ) 
C_  ( x (,) v ) )
5044, 48, 49syl2anc 666 . . . . . . . . . . . . . 14  |-  ( ( ( ( x  e. 
RR*  /\  y  e.  RR* )  /\  z  e.  ( x (,) y
) )  /\  (
u  e.  QQ  /\  v  e.  QQ )  /\  ( ( x  < 
u  /\  u  <  z )  /\  ( z  <  v  /\  v  <  y ) ) )  ->  ( u (,) v )  C_  (
x (,) v ) )
51133ad2ant1 1028 . . . . . . . . . . . . . . 15  |-  ( ( ( ( x  e. 
RR*  /\  y  e.  RR* )  /\  z  e.  ( x (,) y
) )  /\  (
u  e.  QQ  /\  v  e.  QQ )  /\  ( ( x  < 
u  /\  u  <  z )  /\  ( z  <  v  /\  v  <  y ) ) )  ->  y  e.  RR* )
52 simp3rr 1081 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( x  e. 
RR*  /\  y  e.  RR* )  /\  z  e.  ( x (,) y
) )  /\  (
u  e.  QQ  /\  v  e.  QQ )  /\  ( ( x  < 
u  /\  u  <  z )  /\  ( z  <  v  /\  v  <  y ) ) )  ->  v  <  y
)
53 xrltle 11445 . . . . . . . . . . . . . . . . 17  |-  ( ( v  e.  RR*  /\  y  e.  RR* )  ->  (
v  <  y  ->  v  <_  y ) )
5440, 51, 53syl2anc 666 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( x  e. 
RR*  /\  y  e.  RR* )  /\  z  e.  ( x (,) y
) )  /\  (
u  e.  QQ  /\  v  e.  QQ )  /\  ( ( x  < 
u  /\  u  <  z )  /\  ( z  <  v  /\  v  <  y ) ) )  ->  ( v  < 
y  ->  v  <_  y ) )
5552, 54mpd 15 . . . . . . . . . . . . . . 15  |-  ( ( ( ( x  e. 
RR*  /\  y  e.  RR* )  /\  z  e.  ( x (,) y
) )  /\  (
u  e.  QQ  /\  v  e.  QQ )  /\  ( ( x  < 
u  /\  u  <  z )  /\  ( z  <  v  /\  v  <  y ) ) )  ->  v  <_  y
)
56 iooss2 11669 . . . . . . . . . . . . . . 15  |-  ( ( y  e.  RR*  /\  v  <_  y )  ->  (
x (,) v ) 
C_  ( x (,) y ) )
5751, 55, 56syl2anc 666 . . . . . . . . . . . . . 14  |-  ( ( ( ( x  e. 
RR*  /\  y  e.  RR* )  /\  z  e.  ( x (,) y
) )  /\  (
u  e.  QQ  /\  v  e.  QQ )  /\  ( ( x  < 
u  /\  u  <  z )  /\  ( z  <  v  /\  v  <  y ) ) )  ->  ( x (,) v )  C_  (
x (,) y ) )
5850, 57sstrd 3441 . . . . . . . . . . . . 13  |-  ( ( ( ( x  e. 
RR*  /\  y  e.  RR* )  /\  z  e.  ( x (,) y
) )  /\  (
u  e.  QQ  /\  v  e.  QQ )  /\  ( ( x  < 
u  /\  u  <  z )  /\  ( z  <  v  /\  v  <  y ) ) )  ->  ( u (,) v )  C_  (
x (,) y ) )
59 eleq2 2517 . . . . . . . . . . . . . . 15  |-  ( w  =  ( u (,) v )  ->  (
z  e.  w  <->  z  e.  ( u (,) v
) ) )
60 sseq1 3452 . . . . . . . . . . . . . . 15  |-  ( w  =  ( u (,) v )  ->  (
w  C_  ( x (,) y )  <->  ( u (,) v )  C_  (
x (,) y ) ) )
6159, 60anbi12d 716 . . . . . . . . . . . . . 14  |-  ( w  =  ( u (,) v )  ->  (
( z  e.  w  /\  w  C_  ( x (,) y ) )  <-> 
( z  e.  ( u (,) v )  /\  ( u (,) v )  C_  (
x (,) y ) ) ) )
6261rspcev 3149 . . . . . . . . . . . . 13  |-  ( ( ( u (,) v
)  e.  ( (,) " ( QQ  X.  QQ ) )  /\  (
z  e.  ( u (,) v )  /\  ( u (,) v
)  C_  ( x (,) y ) ) )  ->  E. w  e.  ( (,) " ( QQ 
X.  QQ ) ) ( z  e.  w  /\  w  C_  ( x (,) y ) ) )
6333, 43, 58, 62syl12anc 1265 . . . . . . . . . . . 12  |-  ( ( ( ( x  e. 
RR*  /\  y  e.  RR* )  /\  z  e.  ( x (,) y
) )  /\  (
u  e.  QQ  /\  v  e.  QQ )  /\  ( ( x  < 
u  /\  u  <  z )  /\  ( z  <  v  /\  v  <  y ) ) )  ->  E. w  e.  ( (,) " ( QQ 
X.  QQ ) ) ( z  e.  w  /\  w  C_  ( x (,) y ) ) )
64633exp 1206 . . . . . . . . . . 11  |-  ( ( ( x  e.  RR*  /\  y  e.  RR* )  /\  z  e.  (
x (,) y ) )  ->  ( (
u  e.  QQ  /\  v  e.  QQ )  ->  ( ( ( x  <  u  /\  u  <  z )  /\  (
z  <  v  /\  v  <  y ) )  ->  E. w  e.  ( (,) " ( QQ 
X.  QQ ) ) ( z  e.  w  /\  w  C_  ( x (,) y ) ) ) ) )
6564rexlimdvv 2884 . . . . . . . . . 10  |-  ( ( ( x  e.  RR*  /\  y  e.  RR* )  /\  z  e.  (
x (,) y ) )  ->  ( E. u  e.  QQ  E. v  e.  QQ  ( ( x  <  u  /\  u  <  z )  /\  (
z  <  v  /\  v  <  y ) )  ->  E. w  e.  ( (,) " ( QQ 
X.  QQ ) ) ( z  e.  w  /\  w  C_  ( x (,) y ) ) ) )
6617, 65syl5bir 222 . . . . . . . . 9  |-  ( ( ( x  e.  RR*  /\  y  e.  RR* )  /\  z  e.  (
x (,) y ) )  ->  ( ( E. u  e.  QQ  ( x  <  u  /\  u  <  z )  /\  E. v  e.  QQ  (
z  <  v  /\  v  <  y ) )  ->  E. w  e.  ( (,) " ( QQ 
X.  QQ ) ) ( z  e.  w  /\  w  C_  ( x (,) y ) ) ) )
6712, 16, 66mp2and 684 . . . . . . . 8  |-  ( ( ( x  e.  RR*  /\  y  e.  RR* )  /\  z  e.  (
x (,) y ) )  ->  E. w  e.  ( (,) " ( QQ  X.  QQ ) ) ( z  e.  w  /\  w  C_  ( x (,) y ) ) )
6867ralrimiva 2801 . . . . . . 7  |-  ( ( x  e.  RR*  /\  y  e.  RR* )  ->  A. z  e.  ( x (,) y
) E. w  e.  ( (,) " ( QQ  X.  QQ ) ) ( z  e.  w  /\  w  C_  ( x (,) y ) ) )
69 qtopbas 21773 . . . . . . . 8  |-  ( (,) " ( QQ  X.  QQ ) )  e.  TopBases
70 eltg2b 19967 . . . . . . . 8  |-  ( ( (,) " ( QQ 
X.  QQ ) )  e.  TopBases  ->  ( ( x (,) y )  e.  ( topGen `  ( (,) " ( QQ  X.  QQ ) ) )  <->  A. z  e.  ( x (,) y
) E. w  e.  ( (,) " ( QQ  X.  QQ ) ) ( z  e.  w  /\  w  C_  ( x (,) y ) ) ) )
7169, 70ax-mp 5 . . . . . . 7  |-  ( ( x (,) y )  e.  ( topGen `  ( (,) " ( QQ  X.  QQ ) ) )  <->  A. z  e.  ( x (,) y
) E. w  e.  ( (,) " ( QQ  X.  QQ ) ) ( z  e.  w  /\  w  C_  ( x (,) y ) ) )
7268, 71sylibr 216 . . . . . 6  |-  ( ( x  e.  RR*  /\  y  e.  RR* )  ->  (
x (,) y )  e.  ( topGen `  ( (,) " ( QQ  X.  QQ ) ) ) )
7372rgen2a 2814 . . . . 5  |-  A. x  e.  RR*  A. y  e. 
RR*  ( x (,) y )  e.  (
topGen `  ( (,) " ( QQ  X.  QQ ) ) )
74 ffnov 6397 . . . . 5  |-  ( (,)
: ( RR*  X.  RR* )
--> ( topGen `  ( (,) " ( QQ  X.  QQ ) ) )  <->  ( (,)  Fn  ( RR*  X.  RR* )  /\  A. x  e.  RR*  A. y  e.  RR*  (
x (,) y )  e.  ( topGen `  ( (,) " ( QQ  X.  QQ ) ) ) ) )
755, 73, 74mpbir2an 930 . . . 4  |-  (,) :
( RR*  X.  RR* ) --> ( topGen `  ( (,) " ( QQ  X.  QQ ) ) )
76 frn 5733 . . . 4  |-  ( (,)
: ( RR*  X.  RR* )
--> ( topGen `  ( (,) " ( QQ  X.  QQ ) ) )  ->  ran  (,)  C_  ( topGen `  ( (,) " ( QQ  X.  QQ ) ) ) )
7775, 76ax-mp 5 . . 3  |-  ran  (,)  C_  ( topGen `  ( (,) " ( QQ  X.  QQ ) ) )
78 2basgen 19999 . . 3  |-  ( ( ( (,) " ( QQ  X.  QQ ) ) 
C_  ran  (,)  /\  ran  (,)  C_  ( topGen `  ( (,) " ( QQ  X.  QQ ) ) ) )  ->  ( topGen `  ( (,) " ( QQ  X.  QQ ) ) )  =  ( topGen `  ran  (,) )
)
792, 77, 78mp2an 677 . 2  |-  ( topGen `  ( (,) " ( QQ  X.  QQ ) ) )  =  ( topGen ` 
ran  (,) )
801, 79eqtr2i 2473 1  |-  ( topGen ` 
ran  (,) )  =  Q
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188    /\ wa 371    /\ w3a 984    = wceq 1443    e. wcel 1886   A.wral 2736   E.wrex 2737    C_ wss 3403   ~Pcpw 3950   <.cop 3973   class class class wbr 4401    X. cxp 4831   dom cdm 4833   ran crn 4834   "cima 4836   Fun wfun 5575    Fn wfn 5576   -->wf 5577   ` cfv 5581  (class class class)co 6288   RRcr 9535   RR*cxr 9671    < clt 9672    <_ cle 9673   QQcq 11261   (,)cioo 11632   topGenctg 15329   TopBasesctb 19913
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-8 1888  ax-9 1895  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430  ax-sep 4524  ax-nul 4533  ax-pow 4580  ax-pr 4638  ax-un 6580  ax-cnex 9592  ax-resscn 9593  ax-1cn 9594  ax-icn 9595  ax-addcl 9596  ax-addrcl 9597  ax-mulcl 9598  ax-mulrcl 9599  ax-mulcom 9600  ax-addass 9601  ax-mulass 9602  ax-distr 9603  ax-i2m1 9604  ax-1ne0 9605  ax-1rid 9606  ax-rnegex 9607  ax-rrecex 9608  ax-cnre 9609  ax-pre-lttri 9610  ax-pre-lttrn 9611  ax-pre-ltadd 9612  ax-pre-mulgt0 9613  ax-pre-sup 9614
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 985  df-3an 986  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-eu 2302  df-mo 2303  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-nel 2624  df-ral 2741  df-rex 2742  df-reu 2743  df-rmo 2744  df-rab 2745  df-v 3046  df-sbc 3267  df-csb 3363  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-pss 3419  df-nul 3731  df-if 3881  df-pw 3952  df-sn 3968  df-pr 3970  df-tp 3972  df-op 3974  df-uni 4198  df-iun 4279  df-br 4402  df-opab 4461  df-mpt 4462  df-tr 4497  df-eprel 4744  df-id 4748  df-po 4754  df-so 4755  df-fr 4792  df-we 4794  df-xp 4839  df-rel 4840  df-cnv 4841  df-co 4842  df-dm 4843  df-rn 4844  df-res 4845  df-ima 4846  df-pred 5379  df-ord 5425  df-on 5426  df-lim 5427  df-suc 5428  df-iota 5545  df-fun 5583  df-fn 5584  df-f 5585  df-f1 5586  df-fo 5587  df-f1o 5588  df-fv 5589  df-riota 6250  df-ov 6291  df-oprab 6292  df-mpt2 6293  df-om 6690  df-1st 6790  df-2nd 6791  df-wrecs 7025  df-recs 7087  df-rdg 7125  df-er 7360  df-en 7567  df-dom 7568  df-sdom 7569  df-sup 7953  df-inf 7954  df-pnf 9674  df-mnf 9675  df-xr 9676  df-ltxr 9677  df-le 9678  df-sub 9859  df-neg 9860  df-div 10267  df-nn 10607  df-n0 10867  df-z 10935  df-uz 11157  df-q 11262  df-ioo 11636  df-topgen 15335  df-bases 19915
This theorem is referenced by:  re2ndc  21812  opnmblALT  22554  mbfimaopnlem  22604
  Copyright terms: Public domain W3C validator