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

Theorem nllytop 17459
Description: A locally  A space is a topological space. (Contributed by Mario Carneiro, 2-Mar-2015.)
Assertion
Ref Expression
nllytop  |-  ( J  e. 𝑛Locally  A  ->  J  e.  Top )

Proof of Theorem nllytop
Dummy variables  u  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 isnlly 17455 . 2  |-  ( J  e. 𝑛Locally  A  <->  ( J  e. 
Top  /\  A. x  e.  J  A. y  e.  x  E. u  e.  ( ( ( nei `  J ) `  {
y } )  i^i 
~P x ) ( Jt  u )  e.  A
) )
21simplbi 447 1  |-  ( J  e. 𝑛Locally  A  ->  J  e.  Top )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1717   A.wral 2651   E.wrex 2652    i^i cin 3264   ~Pcpw 3744   {csn 3759   ` cfv 5396  (class class class)co 6022   ↾t crest 13577   Topctop 16883   neicnei 17086  𝑛Locally cnlly 17451
This theorem is referenced by:  nlly2i  17462  restnlly  17468  nllyrest  17472  nllyidm  17475  cldllycmp  17481  llycmpkgen  17507  txnlly  17592  txkgen  17607  xkococnlem  17614  xkococn  17615  cnmptkk  17638  xkofvcn  17639  cnmptk1p  17640  cnmptk2  17641  xkocnv  17769  xkohmeo  17770
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2370
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2376  df-cleq 2382  df-clel 2385  df-nfc 2514  df-ral 2656  df-rex 2657  df-rab 2660  df-v 2903  df-dif 3268  df-un 3270  df-in 3272  df-ss 3279  df-nul 3574  df-if 3685  df-sn 3765  df-pr 3766  df-op 3768  df-uni 3960  df-br 4156  df-iota 5360  df-fv 5404  df-ov 6025  df-nlly 17453
  Copyright terms: Public domain W3C validator