Metamath Proof Explorer


Theorem opnneissb

Description: An open set is a neighborhood of any of its subsets. (Contributed by FL, 2-Oct-2006)

Ref Expression
Hypothesis neips.1 X = J
Assertion opnneissb J Top N J S X S N N nei J S

Proof

Step Hyp Ref Expression
1 neips.1 X = J
2 1 eltopss J Top N J N X
3 2 adantr J Top N J S X S N N X
4 ssid N N
5 sseq2 g = N S g S N
6 sseq1 g = N g N N N
7 5 6 anbi12d g = N S g g N S N N N
8 7 rspcev N J S N N N g J S g g N
9 4 8 mpanr2 N J S N g J S g g N
10 9 ad2ant2l J Top N J S X S N g J S g g N
11 1 isnei J Top S X N nei J S N X g J S g g N
12 11 ad2ant2r J Top N J S X S N N nei J S N X g J S g g N
13 3 10 12 mpbir2and J Top N J S X S N N nei J S
14 13 exp43 J Top N J S X S N N nei J S
15 14 3imp J Top N J S X S N N nei J S
16 ssnei J Top N nei J S S N
17 16 ex J Top N nei J S S N
18 17 3ad2ant1 J Top N J S X N nei J S S N
19 15 18 impbid J Top N J S X S N N nei J S