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

Theorem neipcfilu 21322
Description: In an uniform space, a neighboring filter is a Cauchy filter base. (Contributed by Thierry Arnoux, 24-Jan-2018.)
Hypotheses
Ref Expression
neipcfilu.x  |-  X  =  ( Base `  W
)
neipcfilu.j  |-  J  =  ( TopOpen `  W )
neipcfilu.u  |-  U  =  (UnifSt `  W )
Assertion
Ref Expression
neipcfilu  |-  ( ( W  e. UnifSp  /\  W  e. 
TopSp  /\  P  e.  X
)  ->  ( ( nei `  J ) `  { P } )  e.  (CauFilu `  U ) )

Proof of Theorem neipcfilu
Dummy variables  v 
a  w  u are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simp2 1010 . . . . 5  |-  ( ( W  e. UnifSp  /\  W  e. 
TopSp  /\  P  e.  X
)  ->  W  e.  TopSp
)
2 neipcfilu.x . . . . . 6  |-  X  =  ( Base `  W
)
3 neipcfilu.j . . . . . 6  |-  J  =  ( TopOpen `  W )
42, 3istps 19962 . . . . 5  |-  ( W  e.  TopSp 
<->  J  e.  (TopOn `  X ) )
51, 4sylib 201 . . . 4  |-  ( ( W  e. UnifSp  /\  W  e. 
TopSp  /\  P  e.  X
)  ->  J  e.  (TopOn `  X ) )
6 simp3 1011 . . . . 5  |-  ( ( W  e. UnifSp  /\  W  e. 
TopSp  /\  P  e.  X
)  ->  P  e.  X )
76snssd 4086 . . . 4  |-  ( ( W  e. UnifSp  /\  W  e. 
TopSp  /\  P  e.  X
)  ->  { P }  C_  X )
8 snnzg 4058 . . . . 5  |-  ( P  e.  X  ->  { P }  =/=  (/) )
96, 8syl 17 . . . 4  |-  ( ( W  e. UnifSp  /\  W  e. 
TopSp  /\  P  e.  X
)  ->  { P }  =/=  (/) )
10 neifil 20906 . . . 4  |-  ( ( J  e.  (TopOn `  X )  /\  { P }  C_  X  /\  { P }  =/=  (/) )  -> 
( ( nei `  J
) `  { P } )  e.  ( Fil `  X ) )
115, 7, 9, 10syl3anc 1271 . . 3  |-  ( ( W  e. UnifSp  /\  W  e. 
TopSp  /\  P  e.  X
)  ->  ( ( nei `  J ) `  { P } )  e.  ( Fil `  X
) )
12 filfbas 20874 . . 3  |-  ( ( ( nei `  J
) `  { P } )  e.  ( Fil `  X )  ->  ( ( nei `  J ) `  { P } )  e.  (
fBas `  X )
)
1311, 12syl 17 . 2  |-  ( ( W  e. UnifSp  /\  W  e. 
TopSp  /\  P  e.  X
)  ->  ( ( nei `  J ) `  { P } )  e.  ( fBas `  X
) )
14 eqid 2452 . . . . . . . . . 10  |-  ( w
" { P }
)  =  ( w
" { P }
)
15 imaeq1 5141 . . . . . . . . . . . 12  |-  ( v  =  w  ->  (
v " { P } )  =  ( w " { P } ) )
1615eqeq2d 2462 . . . . . . . . . . 11  |-  ( v  =  w  ->  (
( w " { P } )  =  ( v " { P } )  <->  ( w " { P } )  =  ( w " { P } ) ) )
1716rspcev 3118 . . . . . . . . . 10  |-  ( ( w  e.  U  /\  ( w " { P } )  =  ( w " { P } ) )  ->  E. v  e.  U  ( w " { P } )  =  ( v " { P } ) )
1814, 17mpan2 682 . . . . . . . . 9  |-  ( w  e.  U  ->  E. v  e.  U  ( w " { P } )  =  ( v " { P } ) )
19 vex 3016 . . . . . . . . . 10  |-  w  e. 
_V
20 imaexg 6718 . . . . . . . . . 10  |-  ( w  e.  _V  ->  (
w " { P } )  e.  _V )
21 eqid 2452 . . . . . . . . . . 11  |-  ( v  e.  U  |->  ( v
" { P }
) )  =  ( v  e.  U  |->  ( v " { P } ) )
2221elrnmpt 5059 . . . . . . . . . 10  |-  ( ( w " { P } )  e.  _V  ->  ( ( w " { P } )  e. 
ran  ( v  e.  U  |->  ( v " { P } ) )  <->  E. v  e.  U  ( w " { P } )  =  ( v " { P } ) ) )
2319, 20, 22mp2b 10 . . . . . . . . 9  |-  ( ( w " { P } )  e.  ran  ( v  e.  U  |->  ( v " { P } ) )  <->  E. v  e.  U  ( w " { P } )  =  ( v " { P } ) )
2418, 23sylibr 217 . . . . . . . 8  |-  ( w  e.  U  ->  (
w " { P } )  e.  ran  ( v  e.  U  |->  ( v " { P } ) ) )
2524ad2antlr 738 . . . . . . 7  |-  ( ( ( ( ( W  e. UnifSp  /\  W  e.  TopSp  /\  P  e.  X )  /\  v  e.  U
)  /\  w  e.  U )  /\  (
( w " { P } )  X.  (
w " { P } ) )  C_  v )  ->  (
w " { P } )  e.  ran  ( v  e.  U  |->  ( v " { P } ) ) )
26 neipcfilu.u . . . . . . . . . . . . 13  |-  U  =  (UnifSt `  W )
272, 26, 3isusp 21287 . . . . . . . . . . . 12  |-  ( W  e. UnifSp 
<->  ( U  e.  (UnifOn `  X )  /\  J  =  (unifTop `  U )
) )
2827simplbi 466 . . . . . . . . . . 11  |-  ( W  e. UnifSp  ->  U  e.  (UnifOn `  X ) )
29283ad2ant1 1030 . . . . . . . . . 10  |-  ( ( W  e. UnifSp  /\  W  e. 
TopSp  /\  P  e.  X
)  ->  U  e.  (UnifOn `  X ) )
30 eqid 2452 . . . . . . . . . . 11  |-  (unifTop `  U
)  =  (unifTop `  U
)
3130utopsnneip 21274 . . . . . . . . . 10  |-  ( ( U  e.  (UnifOn `  X )  /\  P  e.  X )  ->  (
( nei `  (unifTop `  U ) ) `  { P } )  =  ran  ( v  e.  U  |->  ( v " { P } ) ) )
3229, 6, 31syl2anc 671 . . . . . . . . 9  |-  ( ( W  e. UnifSp  /\  W  e. 
TopSp  /\  P  e.  X
)  ->  ( ( nei `  (unifTop `  U
) ) `  { P } )  =  ran  ( v  e.  U  |->  ( v " { P } ) ) )
3332eleq2d 2515 . . . . . . . 8  |-  ( ( W  e. UnifSp  /\  W  e. 
TopSp  /\  P  e.  X
)  ->  ( (
w " { P } )  e.  ( ( nei `  (unifTop `  U ) ) `  { P } )  <->  ( w " { P } )  e.  ran  ( v  e.  U  |->  ( v
" { P }
) ) ) )
3433ad3antrrr 741 . . . . . . 7  |-  ( ( ( ( ( W  e. UnifSp  /\  W  e.  TopSp  /\  P  e.  X )  /\  v  e.  U
)  /\  w  e.  U )  /\  (
( w " { P } )  X.  (
w " { P } ) )  C_  v )  ->  (
( w " { P } )  e.  ( ( nei `  (unifTop `  U ) ) `  { P } )  <->  ( w " { P } )  e.  ran  ( v  e.  U  |->  ( v
" { P }
) ) ) )
3525, 34mpbird 240 . . . . . 6  |-  ( ( ( ( ( W  e. UnifSp  /\  W  e.  TopSp  /\  P  e.  X )  /\  v  e.  U
)  /\  w  e.  U )  /\  (
( w " { P } )  X.  (
w " { P } ) )  C_  v )  ->  (
w " { P } )  e.  ( ( nei `  (unifTop `  U ) ) `  { P } ) )
36 simpl1 1012 . . . . . . . . . 10  |-  ( ( ( W  e. UnifSp  /\  W  e.  TopSp  /\  P  e.  X )  /\  (
v  e.  U  /\  w  e.  U  /\  ( ( w " { P } )  X.  ( w " { P } ) )  C_  v ) )  ->  W  e. UnifSp )
37363anassrs 1235 . . . . . . . . 9  |-  ( ( ( ( ( W  e. UnifSp  /\  W  e.  TopSp  /\  P  e.  X )  /\  v  e.  U
)  /\  w  e.  U )  /\  (
( w " { P } )  X.  (
w " { P } ) )  C_  v )  ->  W  e. UnifSp )
3827simprbi 470 . . . . . . . . 9  |-  ( W  e. UnifSp  ->  J  =  (unifTop `  U ) )
3937, 38syl 17 . . . . . . . 8  |-  ( ( ( ( ( W  e. UnifSp  /\  W  e.  TopSp  /\  P  e.  X )  /\  v  e.  U
)  /\  w  e.  U )  /\  (
( w " { P } )  X.  (
w " { P } ) )  C_  v )  ->  J  =  (unifTop `  U )
)
4039fveq2d 5852 . . . . . . 7  |-  ( ( ( ( ( W  e. UnifSp  /\  W  e.  TopSp  /\  P  e.  X )  /\  v  e.  U
)  /\  w  e.  U )  /\  (
( w " { P } )  X.  (
w " { P } ) )  C_  v )  ->  ( nei `  J )  =  ( nei `  (unifTop `  U ) ) )
4140fveq1d 5850 . . . . . 6  |-  ( ( ( ( ( W  e. UnifSp  /\  W  e.  TopSp  /\  P  e.  X )  /\  v  e.  U
)  /\  w  e.  U )  /\  (
( w " { P } )  X.  (
w " { P } ) )  C_  v )  ->  (
( nei `  J
) `  { P } )  =  ( ( nei `  (unifTop `  U ) ) `  { P } ) )
4235, 41eleqtrrd 2533 . . . . 5  |-  ( ( ( ( ( W  e. UnifSp  /\  W  e.  TopSp  /\  P  e.  X )  /\  v  e.  U
)  /\  w  e.  U )  /\  (
( w " { P } )  X.  (
w " { P } ) )  C_  v )  ->  (
w " { P } )  e.  ( ( nei `  J
) `  { P } ) )
43 simpr 467 . . . . 5  |-  ( ( ( ( ( W  e. UnifSp  /\  W  e.  TopSp  /\  P  e.  X )  /\  v  e.  U
)  /\  w  e.  U )  /\  (
( w " { P } )  X.  (
w " { P } ) )  C_  v )  ->  (
( w " { P } )  X.  (
w " { P } ) )  C_  v )
44 id 22 . . . . . . . 8  |-  ( a  =  ( w " { P } )  -> 
a  =  ( w
" { P }
) )
4544sqxpeqd 4838 . . . . . . 7  |-  ( a  =  ( w " { P } )  -> 
( a  X.  a
)  =  ( ( w " { P } )  X.  (
w " { P } ) ) )
4645sseq1d 3427 . . . . . 6  |-  ( a  =  ( w " { P } )  -> 
( ( a  X.  a )  C_  v  <->  ( ( w " { P } )  X.  (
w " { P } ) )  C_  v ) )
4746rspcev 3118 . . . . 5  |-  ( ( ( w " { P } )  e.  ( ( nei `  J
) `  { P } )  /\  (
( w " { P } )  X.  (
w " { P } ) )  C_  v )  ->  E. a  e.  ( ( nei `  J
) `  { P } ) ( a  X.  a )  C_  v )
4842, 43, 47syl2anc 671 . . . 4  |-  ( ( ( ( ( W  e. UnifSp  /\  W  e.  TopSp  /\  P  e.  X )  /\  v  e.  U
)  /\  w  e.  U )  /\  (
( w " { P } )  X.  (
w " { P } ) )  C_  v )  ->  E. a  e.  ( ( nei `  J
) `  { P } ) ( a  X.  a )  C_  v )
4929adantr 471 . . . . 5  |-  ( ( ( W  e. UnifSp  /\  W  e.  TopSp  /\  P  e.  X )  /\  v  e.  U )  ->  U  e.  (UnifOn `  X )
)
506adantr 471 . . . . 5  |-  ( ( ( W  e. UnifSp  /\  W  e.  TopSp  /\  P  e.  X )  /\  v  e.  U )  ->  P  e.  X )
51 simpr 467 . . . . 5  |-  ( ( ( W  e. UnifSp  /\  W  e.  TopSp  /\  P  e.  X )  /\  v  e.  U )  ->  v  e.  U )
52 simpll1 1048 . . . . . . . 8  |-  ( ( ( ( U  e.  (UnifOn `  X )  /\  P  e.  X  /\  v  e.  U
)  /\  u  e.  U )  /\  (
u  o.  u ) 
C_  v )  ->  U  e.  (UnifOn `  X
) )
53 simplr 767 . . . . . . . 8  |-  ( ( ( ( U  e.  (UnifOn `  X )  /\  P  e.  X  /\  v  e.  U
)  /\  u  e.  U )  /\  (
u  o.  u ) 
C_  v )  ->  u  e.  U )
54 ustexsym 21241 . . . . . . . 8  |-  ( ( U  e.  (UnifOn `  X )  /\  u  e.  U )  ->  E. w  e.  U  ( `' w  =  w  /\  w  C_  u ) )
5552, 53, 54syl2anc 671 . . . . . . 7  |-  ( ( ( ( U  e.  (UnifOn `  X )  /\  P  e.  X  /\  v  e.  U
)  /\  u  e.  U )  /\  (
u  o.  u ) 
C_  v )  ->  E. w  e.  U  ( `' w  =  w  /\  w  C_  u ) )
5652ad2antrr 737 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( U  e.  (UnifOn `  X )  /\  P  e.  X  /\  v  e.  U )  /\  u  e.  U )  /\  (
u  o.  u ) 
C_  v )  /\  w  e.  U )  /\  ( `' w  =  w  /\  w  C_  u ) )  ->  U  e.  (UnifOn `  X
) )
57 simplr 767 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( U  e.  (UnifOn `  X )  /\  P  e.  X  /\  v  e.  U )  /\  u  e.  U )  /\  (
u  o.  u ) 
C_  v )  /\  w  e.  U )  /\  ( `' w  =  w  /\  w  C_  u ) )  ->  w  e.  U )
58 ustssxp 21230 . . . . . . . . . . . 12  |-  ( ( U  e.  (UnifOn `  X )  /\  w  e.  U )  ->  w  C_  ( X  X.  X
) )
5956, 57, 58syl2anc 671 . . . . . . . . . . 11  |-  ( ( ( ( ( ( U  e.  (UnifOn `  X )  /\  P  e.  X  /\  v  e.  U )  /\  u  e.  U )  /\  (
u  o.  u ) 
C_  v )  /\  w  e.  U )  /\  ( `' w  =  w  /\  w  C_  u ) )  ->  w  C_  ( X  X.  X ) )
60 simpll2 1049 . . . . . . . . . . . 12  |-  ( ( ( ( U  e.  (UnifOn `  X )  /\  P  e.  X  /\  v  e.  U
)  /\  u  e.  U )  /\  (
( u  o.  u
)  C_  v  /\  w  e.  U  /\  ( `' w  =  w  /\  w  C_  u ) ) )  ->  P  e.  X )
61603anassrs 1235 . . . . . . . . . . 11  |-  ( ( ( ( ( ( U  e.  (UnifOn `  X )  /\  P  e.  X  /\  v  e.  U )  /\  u  e.  U )  /\  (
u  o.  u ) 
C_  v )  /\  w  e.  U )  /\  ( `' w  =  w  /\  w  C_  u ) )  ->  P  e.  X )
62 ustneism 21249 . . . . . . . . . . 11  |-  ( ( w  C_  ( X  X.  X )  /\  P  e.  X )  ->  (
( w " { P } )  X.  (
w " { P } ) )  C_  ( w  o.  `' w ) )
6359, 61, 62syl2anc 671 . . . . . . . . . 10  |-  ( ( ( ( ( ( U  e.  (UnifOn `  X )  /\  P  e.  X  /\  v  e.  U )  /\  u  e.  U )  /\  (
u  o.  u ) 
C_  v )  /\  w  e.  U )  /\  ( `' w  =  w  /\  w  C_  u ) )  -> 
( ( w " { P } )  X.  ( w " { P } ) )  C_  ( w  o.  `' w ) )
64 simprl 769 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( U  e.  (UnifOn `  X )  /\  P  e.  X  /\  v  e.  U )  /\  u  e.  U )  /\  (
u  o.  u ) 
C_  v )  /\  w  e.  U )  /\  ( `' w  =  w  /\  w  C_  u ) )  ->  `' w  =  w
)
6564coeq2d 4975 . . . . . . . . . . 11  |-  ( ( ( ( ( ( U  e.  (UnifOn `  X )  /\  P  e.  X  /\  v  e.  U )  /\  u  e.  U )  /\  (
u  o.  u ) 
C_  v )  /\  w  e.  U )  /\  ( `' w  =  w  /\  w  C_  u ) )  -> 
( w  o.  `' w )  =  ( w  o.  w ) )
66 coss1 4968 . . . . . . . . . . . . . 14  |-  ( w 
C_  u  ->  (
w  o.  w ) 
C_  ( u  o.  w ) )
67 coss2 4969 . . . . . . . . . . . . . 14  |-  ( w 
C_  u  ->  (
u  o.  w ) 
C_  ( u  o.  u ) )
6866, 67sstrd 3410 . . . . . . . . . . . . 13  |-  ( w 
C_  u  ->  (
w  o.  w ) 
C_  ( u  o.  u ) )
6968ad2antll 740 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( U  e.  (UnifOn `  X )  /\  P  e.  X  /\  v  e.  U )  /\  u  e.  U )  /\  (
u  o.  u ) 
C_  v )  /\  w  e.  U )  /\  ( `' w  =  w  /\  w  C_  u ) )  -> 
( w  o.  w
)  C_  ( u  o.  u ) )
70 simpllr 774 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( U  e.  (UnifOn `  X )  /\  P  e.  X  /\  v  e.  U )  /\  u  e.  U )  /\  (
u  o.  u ) 
C_  v )  /\  w  e.  U )  /\  ( `' w  =  w  /\  w  C_  u ) )  -> 
( u  o.  u
)  C_  v )
7169, 70sstrd 3410 . . . . . . . . . . 11  |-  ( ( ( ( ( ( U  e.  (UnifOn `  X )  /\  P  e.  X  /\  v  e.  U )  /\  u  e.  U )  /\  (
u  o.  u ) 
C_  v )  /\  w  e.  U )  /\  ( `' w  =  w  /\  w  C_  u ) )  -> 
( w  o.  w
)  C_  v )
7265, 71eqsstrd 3434 . . . . . . . . . 10  |-  ( ( ( ( ( ( U  e.  (UnifOn `  X )  /\  P  e.  X  /\  v  e.  U )  /\  u  e.  U )  /\  (
u  o.  u ) 
C_  v )  /\  w  e.  U )  /\  ( `' w  =  w  /\  w  C_  u ) )  -> 
( w  o.  `' w )  C_  v
)
7363, 72sstrd 3410 . . . . . . . . 9  |-  ( ( ( ( ( ( U  e.  (UnifOn `  X )  /\  P  e.  X  /\  v  e.  U )  /\  u  e.  U )  /\  (
u  o.  u ) 
C_  v )  /\  w  e.  U )  /\  ( `' w  =  w  /\  w  C_  u ) )  -> 
( ( w " { P } )  X.  ( w " { P } ) )  C_  v )
7473ex 440 . . . . . . . 8  |-  ( ( ( ( ( U  e.  (UnifOn `  X
)  /\  P  e.  X  /\  v  e.  U
)  /\  u  e.  U )  /\  (
u  o.  u ) 
C_  v )  /\  w  e.  U )  ->  ( ( `' w  =  w  /\  w  C_  u )  ->  (
( w " { P } )  X.  (
w " { P } ) )  C_  v ) )
7574reximdva 2839 . . . . . . 7  |-  ( ( ( ( U  e.  (UnifOn `  X )  /\  P  e.  X  /\  v  e.  U
)  /\  u  e.  U )  /\  (
u  o.  u ) 
C_  v )  -> 
( E. w  e.  U  ( `' w  =  w  /\  w  C_  u )  ->  E. w  e.  U  ( (
w " { P } )  X.  (
w " { P } ) )  C_  v ) )
7655, 75mpd 15 . . . . . 6  |-  ( ( ( ( U  e.  (UnifOn `  X )  /\  P  e.  X  /\  v  e.  U
)  /\  u  e.  U )  /\  (
u  o.  u ) 
C_  v )  ->  E. w  e.  U  ( ( w " { P } )  X.  ( w " { P } ) )  C_  v )
77 ustexhalf 21236 . . . . . . 7  |-  ( ( U  e.  (UnifOn `  X )  /\  v  e.  U )  ->  E. u  e.  U  ( u  o.  u )  C_  v
)
78773adant2 1028 . . . . . 6  |-  ( ( U  e.  (UnifOn `  X )  /\  P  e.  X  /\  v  e.  U )  ->  E. u  e.  U  ( u  o.  u )  C_  v
)
7976, 78r19.29a 2900 . . . . 5  |-  ( ( U  e.  (UnifOn `  X )  /\  P  e.  X  /\  v  e.  U )  ->  E. w  e.  U  ( (
w " { P } )  X.  (
w " { P } ) )  C_  v )
8049, 50, 51, 79syl3anc 1271 . . . 4  |-  ( ( ( W  e. UnifSp  /\  W  e.  TopSp  /\  P  e.  X )  /\  v  e.  U )  ->  E. w  e.  U  ( (
w " { P } )  X.  (
w " { P } ) )  C_  v )
8148, 80r19.29a 2900 . . 3  |-  ( ( ( W  e. UnifSp  /\  W  e.  TopSp  /\  P  e.  X )  /\  v  e.  U )  ->  E. a  e.  ( ( nei `  J
) `  { P } ) ( a  X.  a )  C_  v )
8281ralrimiva 2790 . 2  |-  ( ( W  e. UnifSp  /\  W  e. 
TopSp  /\  P  e.  X
)  ->  A. v  e.  U  E. a  e.  ( ( nei `  J
) `  { P } ) ( a  X.  a )  C_  v )
83 iscfilu 21314 . . 3  |-  ( U  e.  (UnifOn `  X
)  ->  ( (
( nei `  J
) `  { P } )  e.  (CauFilu `  U )  <->  ( (
( nei `  J
) `  { P } )  e.  (
fBas `  X )  /\  A. v  e.  U  E. a  e.  (
( nei `  J
) `  { P } ) ( a  X.  a )  C_  v ) ) )
8429, 83syl 17 . 2  |-  ( ( W  e. UnifSp  /\  W  e. 
TopSp  /\  P  e.  X
)  ->  ( (
( nei `  J
) `  { P } )  e.  (CauFilu `  U )  <->  ( (
( nei `  J
) `  { P } )  e.  (
fBas `  X )  /\  A. v  e.  U  E. a  e.  (
( nei `  J
) `  { P } ) ( a  X.  a )  C_  v ) ) )
8513, 82, 84mpbir2and 933 1  |-  ( ( W  e. UnifSp  /\  W  e. 
TopSp  /\  P  e.  X
)  ->  ( ( nei `  J ) `  { P } )  e.  (CauFilu `  U ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    /\ wa 375    /\ w3a 986    = wceq 1448    e. wcel 1891    =/= wne 2622   A.wral 2737   E.wrex 2738   _Vcvv 3013    C_ wss 3372   (/)c0 3699   {csn 3936    |-> cmpt 4433    X. cxp 4810   `'ccnv 4811   ran crn 4813   "cima 4815    o. ccom 4816   ` cfv 5561   Basecbs 15132   TopOpenctopn 15331   fBascfbas 18969  TopOnctopon 19929   TopSpctps 19930   neicnei 20124   Filcfil 20871  UnifOncust 21225  unifTopcutop 21256  UnifStcuss 21279  UnifSpcusp 21280  CauFiluccfilu 21312
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1673  ax-4 1686  ax-5 1762  ax-6 1809  ax-7 1855  ax-8 1893  ax-9 1900  ax-10 1919  ax-11 1924  ax-12 1937  ax-13 2092  ax-ext 2432  ax-rep 4487  ax-sep 4497  ax-nul 4506  ax-pow 4554  ax-pr 4612  ax-un 6571
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 987  df-3an 988  df-tru 1451  df-ex 1668  df-nf 1672  df-sb 1802  df-eu 2304  df-mo 2305  df-clab 2439  df-cleq 2445  df-clel 2448  df-nfc 2582  df-ne 2624  df-nel 2625  df-ral 2742  df-rex 2743  df-reu 2744  df-rab 2746  df-v 3015  df-sbc 3236  df-csb 3332  df-dif 3375  df-un 3377  df-in 3379  df-ss 3386  df-pss 3388  df-nul 3700  df-if 3850  df-pw 3921  df-sn 3937  df-pr 3939  df-tp 3941  df-op 3943  df-uni 4169  df-int 4205  df-iun 4250  df-br 4375  df-opab 4434  df-mpt 4435  df-tr 4470  df-eprel 4723  df-id 4727  df-po 4733  df-so 4734  df-fr 4771  df-we 4773  df-xp 4818  df-rel 4819  df-cnv 4820  df-co 4821  df-dm 4822  df-rn 4823  df-res 4824  df-ima 4825  df-pred 5359  df-ord 5405  df-on 5406  df-lim 5407  df-suc 5408  df-iota 5525  df-fun 5563  df-fn 5564  df-f 5565  df-f1 5566  df-fo 5567  df-f1o 5568  df-fv 5569  df-ov 6279  df-oprab 6280  df-mpt2 6281  df-om 6681  df-wrecs 7015  df-recs 7077  df-rdg 7115  df-1o 7169  df-oadd 7173  df-er 7350  df-en 7557  df-fin 7560  df-fi 7912  df-fbas 18978  df-top 19932  df-topon 19934  df-topsp 19935  df-nei 20125  df-fil 20872  df-ust 21226  df-utop 21257  df-usp 21283  df-cfilu 21313
This theorem is referenced by:  ucnextcn  21330
  Copyright terms: Public domain W3C validator