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 ) )