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

Theorem nllytop 22847
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 22843 . 2 (𝐽 ∈ 𝑛-Locally 𝐴 ↔ (𝐽 ∈ Top ∧ βˆ€π‘₯ ∈ 𝐽 βˆ€π‘¦ ∈ π‘₯ βˆƒπ‘’ ∈ (((neiβ€˜π½)β€˜{𝑦}) ∩ 𝒫 π‘₯)(𝐽 β†Ύt 𝑒) ∈ 𝐴))
21simplbi 499 1 (𝐽 ∈ 𝑛-Locally 𝐴 β†’ 𝐽 ∈ Top)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∈ wcel 2107  βˆ€wral 3061  βˆƒwrex 3070   ∩ cin 3913  π’« cpw 4564  {csn 4590  β€˜cfv 6500  (class class class)co 7361   β†Ύt crest 17310  Topctop 22265  neicnei 22471  π‘›-Locally cnlly 22839
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3062  df-rex 3071  df-rab 3407  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4287  df-if 4491  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4870  df-br 5110  df-iota 6452  df-fv 6508  df-ov 7364  df-nlly 22841
This theorem is referenced by:  nlly2i  22850  restnlly  22856  nllyrest  22860  nllyidm  22863  cldllycmp  22869  llycmpkgen  22926  txnlly  23011  txkgen  23026  xkococnlem  23033  xkococn  23034  cnmptkk  23057  xkofvcn  23058  cnmptk1p  23059  cnmptk2  23060  xkocnv  23188  xkohmeo  23189
  Copyright terms: Public domain W3C validator