Metamath Proof Explorer

Theorem topssnei

Description: A finer topology has more neighborhoods. (Contributed by Mario Carneiro, 9-Apr-2015)

Ref Expression
Hypotheses tpnei.1 
|- X = U. J
topssnei.2 
|- Y = U. K
Assertion topssnei 
|- ( ( ( J e. Top /\ K e. Top /\ X = Y ) /\ J C_ K ) -> ( ( nei ` J ) ` S ) C_ ( ( nei ` K ) ` S ) )

Proof

Step Hyp Ref Expression
1 tpnei.1 
 |-  X = U. J
2 topssnei.2 
 |-  Y = U. K
3 simpl2 
 |-  ( ( ( J e. Top /\ K e. Top /\ X = Y ) /\ ( J C_ K /\ x e. ( ( nei ` J ) ` S ) ) ) -> K e. Top )
4 simprl 
 |-  ( ( ( J e. Top /\ K e. Top /\ X = Y ) /\ ( J C_ K /\ x e. ( ( nei ` J ) ` S ) ) ) -> J C_ K )
5 simpl1 
 |-  ( ( ( J e. Top /\ K e. Top /\ X = Y ) /\ ( J C_ K /\ x e. ( ( nei ` J ) ` S ) ) ) -> J e. Top )
6 simprr 
 |-  ( ( ( J e. Top /\ K e. Top /\ X = Y ) /\ ( J C_ K /\ x e. ( ( nei ` J ) ` S ) ) ) -> x e. ( ( nei ` J ) ` S ) )
7 1 neii1 
 |-  ( ( J e. Top /\ x e. ( ( nei ` J ) ` S ) ) -> x C_ X )
8 5 6 7 syl2anc 
 |-  ( ( ( J e. Top /\ K e. Top /\ X = Y ) /\ ( J C_ K /\ x e. ( ( nei ` J ) ` S ) ) ) -> x C_ X )
9 1 ntropn 
 |-  ( ( J e. Top /\ x C_ X ) -> ( ( int ` J ) ` x ) e. J )
10 5 8 9 syl2anc 
 |-  ( ( ( J e. Top /\ K e. Top /\ X = Y ) /\ ( J C_ K /\ x e. ( ( nei ` J ) ` S ) ) ) -> ( ( int ` J ) ` x ) e. J )
11 4 10 sseldd 
 |-  ( ( ( J e. Top /\ K e. Top /\ X = Y ) /\ ( J C_ K /\ x e. ( ( nei ` J ) ` S ) ) ) -> ( ( int ` J ) ` x ) e. K )
12 1 neiss2 
 |-  ( ( J e. Top /\ x e. ( ( nei ` J ) ` S ) ) -> S C_ X )
13 5 6 12 syl2anc 
 |-  ( ( ( J e. Top /\ K e. Top /\ X = Y ) /\ ( J C_ K /\ x e. ( ( nei ` J ) ` S ) ) ) -> S C_ X )
14 1 neiint 
 |-  ( ( J e. Top /\ S C_ X /\ x C_ X ) -> ( x e. ( ( nei ` J ) ` S ) <-> S C_ ( ( int ` J ) ` x ) ) )
15 5 13 8 14 syl3anc 
 |-  ( ( ( J e. Top /\ K e. Top /\ X = Y ) /\ ( J C_ K /\ x e. ( ( nei ` J ) ` S ) ) ) -> ( x e. ( ( nei ` J ) ` S ) <-> S C_ ( ( int ` J ) ` x ) ) )
16 6 15 mpbid 
 |-  ( ( ( J e. Top /\ K e. Top /\ X = Y ) /\ ( J C_ K /\ x e. ( ( nei ` J ) ` S ) ) ) -> S C_ ( ( int ` J ) ` x ) )
17 opnneiss 
 |-  ( ( K e. Top /\ ( ( int ` J ) ` x ) e. K /\ S C_ ( ( int ` J ) ` x ) ) -> ( ( int ` J ) ` x ) e. ( ( nei ` K ) ` S ) )
18 3 11 16 17 syl3anc 
 |-  ( ( ( J e. Top /\ K e. Top /\ X = Y ) /\ ( J C_ K /\ x e. ( ( nei ` J ) ` S ) ) ) -> ( ( int ` J ) ` x ) e. ( ( nei ` K ) ` S ) )
19 1 ntrss2 
 |-  ( ( J e. Top /\ x C_ X ) -> ( ( int ` J ) ` x ) C_ x )
20 5 8 19 syl2anc 
 |-  ( ( ( J e. Top /\ K e. Top /\ X = Y ) /\ ( J C_ K /\ x e. ( ( nei ` J ) ` S ) ) ) -> ( ( int ` J ) ` x ) C_ x )
21 simpl3 
 |-  ( ( ( J e. Top /\ K e. Top /\ X = Y ) /\ ( J C_ K /\ x e. ( ( nei ` J ) ` S ) ) ) -> X = Y )
22 8 21 sseqtrd 
 |-  ( ( ( J e. Top /\ K e. Top /\ X = Y ) /\ ( J C_ K /\ x e. ( ( nei ` J ) ` S ) ) ) -> x C_ Y )
23 2 ssnei2 
 |-  ( ( ( K e. Top /\ ( ( int ` J ) ` x ) e. ( ( nei ` K ) ` S ) ) /\ ( ( ( int ` J ) ` x ) C_ x /\ x C_ Y ) ) -> x e. ( ( nei ` K ) ` S ) )
24 3 18 20 22 23 syl22anc 
 |-  ( ( ( J e. Top /\ K e. Top /\ X = Y ) /\ ( J C_ K /\ x e. ( ( nei ` J ) ` S ) ) ) -> x e. ( ( nei ` K ) ` S ) )
25 24 expr 
 |-  ( ( ( J e. Top /\ K e. Top /\ X = Y ) /\ J C_ K ) -> ( x e. ( ( nei ` J ) ` S ) -> x e. ( ( nei ` K ) ` S ) ) )
26 25 ssrdv 
 |-  ( ( ( J e. Top /\ K e. Top /\ X = Y ) /\ J C_ K ) -> ( ( nei ` J ) ` S ) C_ ( ( nei ` K ) ` S ) )