Step |
Hyp |
Ref |
Expression |
1 |
|
neips.1 |
|- X = U. J |
2 |
|
simprr |
|- ( ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) /\ ( N C_ M /\ M C_ X ) ) -> M C_ X ) |
3 |
|
neii2 |
|- ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) -> E. g e. J ( S C_ g /\ g C_ N ) ) |
4 |
|
sstr2 |
|- ( g C_ N -> ( N C_ M -> g C_ M ) ) |
5 |
4
|
com12 |
|- ( N C_ M -> ( g C_ N -> g C_ M ) ) |
6 |
5
|
anim2d |
|- ( N C_ M -> ( ( S C_ g /\ g C_ N ) -> ( S C_ g /\ g C_ M ) ) ) |
7 |
6
|
reximdv |
|- ( N C_ M -> ( E. g e. J ( S C_ g /\ g C_ N ) -> E. g e. J ( S C_ g /\ g C_ M ) ) ) |
8 |
3 7
|
mpan9 |
|- ( ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) /\ N C_ M ) -> E. g e. J ( S C_ g /\ g C_ M ) ) |
9 |
8
|
adantrr |
|- ( ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) /\ ( N C_ M /\ M C_ X ) ) -> E. g e. J ( S C_ g /\ g C_ M ) ) |
10 |
1
|
neiss2 |
|- ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) -> S C_ X ) |
11 |
1
|
isnei |
|- ( ( J e. Top /\ S C_ X ) -> ( M e. ( ( nei ` J ) ` S ) <-> ( M C_ X /\ E. g e. J ( S C_ g /\ g C_ M ) ) ) ) |
12 |
10 11
|
syldan |
|- ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) -> ( M e. ( ( nei ` J ) ` S ) <-> ( M C_ X /\ E. g e. J ( S C_ g /\ g C_ M ) ) ) ) |
13 |
12
|
adantr |
|- ( ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) /\ ( N C_ M /\ M C_ X ) ) -> ( M e. ( ( nei ` J ) ` S ) <-> ( M C_ X /\ E. g e. J ( S C_ g /\ g C_ M ) ) ) ) |
14 |
2 9 13
|
mpbir2and |
|- ( ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) /\ ( N C_ M /\ M C_ X ) ) -> M e. ( ( nei ` J ) ` S ) ) |