Metamath Proof Explorer

Theorem neiint

Description: An intuitive definition of a neighborhood in terms of interior. (Contributed by Szymon Jaroszewicz, 18-Dec-2007) (Revised by Mario Carneiro, 11-Nov-2013)

Ref Expression
Hypothesis neifval.1 
|- X = U. J
Assertion neiint 
|- ( ( J e. Top /\ S C_ X /\ N C_ X ) -> ( N e. ( ( nei ` J ) ` S ) <-> S C_ ( ( int ` J ) ` N ) ) )

Proof

Step Hyp Ref Expression
1 neifval.1 
 |-  X = U. J
2 1 isnei 
 |-  ( ( J e. Top /\ S C_ X ) -> ( N e. ( ( nei ` J ) ` S ) <-> ( N C_ X /\ E. v e. J ( S C_ v /\ v C_ N ) ) ) )
3 2 3adant3 
 |-  ( ( J e. Top /\ S C_ X /\ N C_ X ) -> ( N e. ( ( nei ` J ) ` S ) <-> ( N C_ X /\ E. v e. J ( S C_ v /\ v C_ N ) ) ) )
4 3 3anibar 
 |-  ( ( J e. Top /\ S C_ X /\ N C_ X ) -> ( N e. ( ( nei ` J ) ` S ) <-> E. v e. J ( S C_ v /\ v C_ N ) ) )
5 simprrl 
 |-  ( ( ( J e. Top /\ S C_ X /\ N C_ X ) /\ ( v e. J /\ ( S C_ v /\ v C_ N ) ) ) -> S C_ v )
6 1 ssntr 
 |-  ( ( ( J e. Top /\ N C_ X ) /\ ( v e. J /\ v C_ N ) ) -> v C_ ( ( int ` J ) ` N ) )
7 6 3adantl2 
 |-  ( ( ( J e. Top /\ S C_ X /\ N C_ X ) /\ ( v e. J /\ v C_ N ) ) -> v C_ ( ( int ` J ) ` N ) )
8 7 adantrrl 
 |-  ( ( ( J e. Top /\ S C_ X /\ N C_ X ) /\ ( v e. J /\ ( S C_ v /\ v C_ N ) ) ) -> v C_ ( ( int ` J ) ` N ) )
9 5 8 sstrd 
 |-  ( ( ( J e. Top /\ S C_ X /\ N C_ X ) /\ ( v e. J /\ ( S C_ v /\ v C_ N ) ) ) -> S C_ ( ( int ` J ) ` N ) )
10 9 rexlimdvaa 
 |-  ( ( J e. Top /\ S C_ X /\ N C_ X ) -> ( E. v e. J ( S C_ v /\ v C_ N ) -> S C_ ( ( int ` J ) ` N ) ) )
11 simpl1 
 |-  ( ( ( J e. Top /\ S C_ X /\ N C_ X ) /\ S C_ ( ( int ` J ) ` N ) ) -> J e. Top )
12 simpl3 
 |-  ( ( ( J e. Top /\ S C_ X /\ N C_ X ) /\ S C_ ( ( int ` J ) ` N ) ) -> N C_ X )
13 1 ntropn 
 |-  ( ( J e. Top /\ N C_ X ) -> ( ( int ` J ) ` N ) e. J )
14 11 12 13 syl2anc 
 |-  ( ( ( J e. Top /\ S C_ X /\ N C_ X ) /\ S C_ ( ( int ` J ) ` N ) ) -> ( ( int ` J ) ` N ) e. J )
15 simpr 
 |-  ( ( ( J e. Top /\ S C_ X /\ N C_ X ) /\ S C_ ( ( int ` J ) ` N ) ) -> S C_ ( ( int ` J ) ` N ) )
16 1 ntrss2 
 |-  ( ( J e. Top /\ N C_ X ) -> ( ( int ` J ) ` N ) C_ N )
17 11 12 16 syl2anc 
 |-  ( ( ( J e. Top /\ S C_ X /\ N C_ X ) /\ S C_ ( ( int ` J ) ` N ) ) -> ( ( int ` J ) ` N ) C_ N )
18 sseq2 
 |-  ( v = ( ( int ` J ) ` N ) -> ( S C_ v <-> S C_ ( ( int ` J ) ` N ) ) )
19 sseq1 
 |-  ( v = ( ( int ` J ) ` N ) -> ( v C_ N <-> ( ( int ` J ) ` N ) C_ N ) )
20 18 19 anbi12d 
 |-  ( v = ( ( int ` J ) ` N ) -> ( ( S C_ v /\ v C_ N ) <-> ( S C_ ( ( int ` J ) ` N ) /\ ( ( int ` J ) ` N ) C_ N ) ) )
21 20 rspcev 
 |-  ( ( ( ( int ` J ) ` N ) e. J /\ ( S C_ ( ( int ` J ) ` N ) /\ ( ( int ` J ) ` N ) C_ N ) ) -> E. v e. J ( S C_ v /\ v C_ N ) )
22 14 15 17 21 syl12anc 
 |-  ( ( ( J e. Top /\ S C_ X /\ N C_ X ) /\ S C_ ( ( int ` J ) ` N ) ) -> E. v e. J ( S C_ v /\ v C_ N ) )
23 22 ex 
 |-  ( ( J e. Top /\ S C_ X /\ N C_ X ) -> ( S C_ ( ( int ` J ) ` N ) -> E. v e. J ( S C_ v /\ v C_ N ) ) )
24 10 23 impbid 
 |-  ( ( J e. Top /\ S C_ X /\ N C_ X ) -> ( E. v e. J ( S C_ v /\ v C_ N ) <-> S C_ ( ( int ` J ) ` N ) ) )
25 4 24 bitrd 
 |-  ( ( J e. Top /\ S C_ X /\ N C_ X ) -> ( N e. ( ( nei ` J ) ` S ) <-> S C_ ( ( int ` J ) ` N ) ) )