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

Theorem nllytop 21257
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 21253 . 2 (𝐽 ∈ 𝑛-Locally 𝐴 ↔ (𝐽 ∈ Top ∧ ∀𝑥𝐽𝑦𝑥𝑢 ∈ (((nei‘𝐽)‘{𝑦}) ∩ 𝒫 𝑥)(𝐽t 𝑢) ∈ 𝐴))
21simplbi 476 1 (𝐽 ∈ 𝑛-Locally 𝐴𝐽 ∈ Top)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1988  wral 2909  wrex 2910  cin 3566  𝒫 cpw 4149  {csn 4168  cfv 5876  (class class class)co 6635  t crest 16062  Topctop 20679  neicnei 20882  𝑛-Locally cnlly 21249
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ral 2914  df-rex 2915  df-rab 2918  df-v 3197  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-sn 4169  df-pr 4171  df-op 4175  df-uni 4428  df-br 4645  df-iota 5839  df-fv 5884  df-ov 6638  df-nlly 21251
This theorem is referenced by:  nlly2i  21260  restnlly  21266  nllyrest  21270  nllyidm  21273  cldllycmp  21279  llycmpkgen  21336  txnlly  21421  txkgen  21436  xkococnlem  21443  xkococn  21444  cnmptkk  21467  xkofvcn  21468  cnmptk1p  21469  cnmptk2  21470  xkocnv  21598  xkohmeo  21599
  Copyright terms: Public domain W3C validator