Theorem nllytop 22624

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.

Step	Hyp	Ref	Expression
1		isnlly 22620	. 2 ⊢ (𝐽 ∈ 𝑛-Locally 𝐴 ↔ (𝐽 ∈ Top ∧ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (((nei‘𝐽)‘{𝑦}) ∩ 𝒫 𝑥)(𝐽 ↾t 𝑢) ∈ 𝐴))
2	1	simplbi 498	1 ⊢ (𝐽 ∈ 𝑛-Locally 𝐴 → 𝐽 ∈ Top)

Syntax hints:   → wi 4   ∈ wcel 2106  ∀wral 3064  ∃wrex 3065   ∩ cin 3886  𝒫 cpw 4533  {csn 4561  ‘cfv 6433  (class class class)co 7275   ↾_t crest 17131  Topctop 22042  neicnei 22248  𝑛-Locally cnlly 22616

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-iota 6391  df-fv 6441  df-ov 7278  df-nlly 22618

This theorem is referenced by:  nlly2i  22627  restnlly  22633  nllyrest  22637  nllyidm  22640  cldllycmp  22646  llycmpkgen  22703  txnlly  22788  txkgen  22803  xkococnlem  22810  xkococn  22811  cnmptkk  22834  xkofvcn  22835  cnmptk1p  22836  cnmptk2  22837  xkocnv  22965  xkohmeo  22966