Metamath Proof Explorer


Theorem opnneiss

Description: An open set is a neighborhood of any of its subsets. (Contributed by NM, 13-Feb-2007)

Ref Expression
Assertion opnneiss J Top N J S N N nei J S

Proof

Step Hyp Ref Expression
1 simp3 J Top N J S N S N
2 eqid J = J
3 2 eltopss J Top N J N J
4 sstr S N N J S J
5 4 ancoms N J S N S J
6 3 5 stoic3 J Top N J S N S J
7 2 opnneissb J Top N J S J S N N nei J S
8 6 7 syld3an3 J Top N J S N S N N nei J S
9 1 8 mpbid J Top N J S N N nei J S