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

Theorem nllytop 23497
Description: A locally 𝐴 space is a topological space. (Contributed by Mario Carneiro, 2-Mar-2015.)
Assertion
Ref Expression
nllytop (𝐽 ∈ 𝑛-Locally 𝐴𝐽 ∈ Top)

Proof of Theorem nllytop
Dummy variables 𝑢 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 isnlly 23493 . 2 (𝐽 ∈ 𝑛-Locally 𝐴 ↔ (𝐽 ∈ Top ∧ ∀𝑥𝐽𝑦𝑥𝑢 ∈ (((nei‘𝐽)‘{𝑦}) ∩ 𝒫 𝑥)(𝐽t 𝑢) ∈ 𝐴))
21simplbi 497 1 (𝐽 ∈ 𝑛-Locally 𝐴𝐽 ∈ Top)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2106  wral 3059  wrex 3068  cin 3962  𝒫 cpw 4605  {csn 4631  cfv 6563  (class class class)co 7431  t crest 17467  Topctop 22915  neicnei 23121  𝑛-Locally cnlly 23489
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-iota 6516  df-fv 6571  df-ov 7434  df-nlly 23491
This theorem is referenced by:  nlly2i  23500  restnlly  23506  nllyrest  23510  nllyidm  23513  cldllycmp  23519  llycmpkgen  23576  txnlly  23661  txkgen  23676  xkococnlem  23683  xkococn  23684  cnmptkk  23707  xkofvcn  23708  cnmptk1p  23709  cnmptk2  23710  xkocnv  23838  xkohmeo  23839
  Copyright terms: Public domain W3C validator