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