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

Theorem neii1 21796
 Description: A neighborhood is included in the topology's base set. (Contributed by NM, 12-Feb-2007.)
Hypothesis
Ref Expression
neifval.1 𝑋 = 𝐽
Assertion
Ref Expression
neii1 ((𝐽 ∈ Top ∧ 𝑁 ∈ ((nei‘𝐽)‘𝑆)) → 𝑁𝑋)

Proof of Theorem neii1
Dummy variable 𝑔 is distinct from all other variables.
StepHypRef Expression
1 neifval.1 . . 3 𝑋 = 𝐽
21neiss2 21791 . 2 ((𝐽 ∈ Top ∧ 𝑁 ∈ ((nei‘𝐽)‘𝑆)) → 𝑆𝑋)
31isnei 21793 . . . 4 ((𝐽 ∈ Top ∧ 𝑆𝑋) → (𝑁 ∈ ((nei‘𝐽)‘𝑆) ↔ (𝑁𝑋 ∧ ∃𝑔𝐽 (𝑆𝑔𝑔𝑁))))
4 simpl 487 . . . 4 ((𝑁𝑋 ∧ ∃𝑔𝐽 (𝑆𝑔𝑔𝑁)) → 𝑁𝑋)
53, 4syl6bi 256 . . 3 ((𝐽 ∈ Top ∧ 𝑆𝑋) → (𝑁 ∈ ((nei‘𝐽)‘𝑆) → 𝑁𝑋))
65impancom 456 . 2 ((𝐽 ∈ Top ∧ 𝑁 ∈ ((nei‘𝐽)‘𝑆)) → (𝑆𝑋𝑁𝑋))
72, 6mpd 15 1 ((𝐽 ∈ Top ∧ 𝑁 ∈ ((nei‘𝐽)‘𝑆)) → 𝑁𝑋)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 400   = wceq 1539   ∈ wcel 2112  ∃wrex 3072   ⊆ wss 3859  ∪ cuni 4796  ‘cfv 6333  Topctop 21583  neicnei 21787 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 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5232  ax-pr 5296 This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3an 1087  df-tru 1542  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ne 2953  df-ral 3076  df-rex 3077  df-reu 3078  df-rab 3080  df-v 3412  df-sbc 3698  df-csb 3807  df-dif 3862  df-un 3864  df-in 3866  df-ss 3876  df-nul 4227  df-if 4419  df-pw 4494  df-sn 4521  df-pr 4523  df-op 4527  df-uni 4797  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5428  df-xp 5528  df-rel 5529  df-cnv 5530  df-co 5531  df-dm 5532  df-rn 5533  df-res 5534  df-ima 5535  df-iota 6292  df-fun 6335  df-fn 6336  df-f 6337  df-f1 6338  df-fo 6339  df-f1o 6340  df-fv 6341  df-top 21584  df-nei 21788 This theorem is referenced by:  neisspw  21797  neiss  21799  opnnei  21810  neiuni  21812  topssnei  21814  innei  21815  neissex  21817  iscnp4  21953  llycmpkgen2  22240  neitx  22297  flimopn  22665  flfnei  22681  fclsneii  22707  fcfnei  22725  cnextcn  22757  limcflf  24570  cvmlift2lem1  32770  neiin  34060  neibastop2  34089
 Copyright terms: Public domain W3C validator