Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > opnneip | Structured version Visualization version GIF version |
Description: An open set is a neighborhood of any of its members. (Contributed by NM, 8-Mar-2007.) |
Ref | Expression |
---|---|
opnneip | ⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ 𝐽 ∧ 𝑃 ∈ 𝑁) → 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | snssi 4693 | . 2 ⊢ (𝑃 ∈ 𝑁 → {𝑃} ⊆ 𝑁) | |
2 | opnneiss 21862 | . 2 ⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ 𝐽 ∧ {𝑃} ⊆ 𝑁) → 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) | |
3 | 1, 2 | syl3an3 1166 | 1 ⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ 𝐽 ∧ 𝑃 ∈ 𝑁) → 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1088 ∈ wcel 2113 ⊆ wss 3841 {csn 4513 ‘cfv 6333 Topctop 21637 neicnei 21841 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1916 ax-6 1974 ax-7 2019 ax-8 2115 ax-9 2123 ax-10 2144 ax-11 2161 ax-12 2178 ax-ext 2710 ax-rep 5151 ax-sep 5164 ax-nul 5171 ax-pow 5229 ax-pr 5293 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2540 df-eu 2570 df-clab 2717 df-cleq 2730 df-clel 2811 df-nfc 2881 df-ne 2935 df-ral 3058 df-rex 3059 df-reu 3060 df-rab 3062 df-v 3399 df-sbc 3680 df-csb 3789 df-dif 3844 df-un 3846 df-in 3848 df-ss 3858 df-nul 4210 df-if 4412 df-pw 4487 df-sn 4514 df-pr 4516 df-op 4520 df-uni 4794 df-iun 4880 df-br 5028 df-opab 5090 df-mpt 5108 df-id 5425 df-xp 5525 df-rel 5526 df-cnv 5527 df-co 5528 df-dm 5529 df-rn 5530 df-res 5531 df-ima 5532 df-iota 6291 df-fun 6335 df-fn 6336 df-f 6337 df-f1 6338 df-fo 6339 df-f1o 6340 df-fv 6341 df-top 21638 df-nei 21842 |
This theorem is referenced by: opnnei 21864 neindisj2 21867 iscnp4 22007 cnpnei 22008 hausnei2 22097 llynlly 22221 nllyrest 22230 nllyidm 22233 hausllycmp 22238 cldllycmp 22239 txnlly 22381 flimfil 22713 flimopn 22719 fbflim2 22721 hausflimlem 22723 flimcf 22726 flimsncls 22730 fclsnei 22763 fcfnei 22779 cnextcn 22811 utopreg 22997 blnei 23248 cnllycmp 23701 flimcfil 24059 limcflf 24625 rrhre 31533 cvmlift2lem12 32839 |
Copyright terms: Public domain | W3C validator |