Step |
Hyp |
Ref |
Expression |
1 |
|
neips.1 |
|- X = U. J |
2 |
1
|
eltopss |
|- ( ( J e. Top /\ N e. J ) -> N C_ X ) |
3 |
2
|
adantr |
|- ( ( ( J e. Top /\ N e. J ) /\ ( S C_ X /\ S C_ N ) ) -> N C_ X ) |
4 |
|
ssid |
|- N C_ N |
5 |
|
sseq2 |
|- ( g = N -> ( S C_ g <-> S C_ N ) ) |
6 |
|
sseq1 |
|- ( g = N -> ( g C_ N <-> N C_ N ) ) |
7 |
5 6
|
anbi12d |
|- ( g = N -> ( ( S C_ g /\ g C_ N ) <-> ( S C_ N /\ N C_ N ) ) ) |
8 |
7
|
rspcev |
|- ( ( N e. J /\ ( S C_ N /\ N C_ N ) ) -> E. g e. J ( S C_ g /\ g C_ N ) ) |
9 |
4 8
|
mpanr2 |
|- ( ( N e. J /\ S C_ N ) -> E. g e. J ( S C_ g /\ g C_ N ) ) |
10 |
9
|
ad2ant2l |
|- ( ( ( J e. Top /\ N e. J ) /\ ( S C_ X /\ S C_ N ) ) -> E. g e. J ( S C_ g /\ g C_ N ) ) |
11 |
1
|
isnei |
|- ( ( J e. Top /\ S C_ X ) -> ( N e. ( ( nei ` J ) ` S ) <-> ( N C_ X /\ E. g e. J ( S C_ g /\ g C_ N ) ) ) ) |
12 |
11
|
ad2ant2r |
|- ( ( ( J e. Top /\ N e. J ) /\ ( S C_ X /\ S C_ N ) ) -> ( N e. ( ( nei ` J ) ` S ) <-> ( N C_ X /\ E. g e. J ( S C_ g /\ g C_ N ) ) ) ) |
13 |
3 10 12
|
mpbir2and |
|- ( ( ( J e. Top /\ N e. J ) /\ ( S C_ X /\ S C_ N ) ) -> N e. ( ( nei ` J ) ` S ) ) |
14 |
13
|
exp43 |
|- ( J e. Top -> ( N e. J -> ( S C_ X -> ( S C_ N -> N e. ( ( nei ` J ) ` S ) ) ) ) ) |
15 |
14
|
3imp |
|- ( ( J e. Top /\ N e. J /\ S C_ X ) -> ( S C_ N -> N e. ( ( nei ` J ) ` S ) ) ) |
16 |
|
ssnei |
|- ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) -> S C_ N ) |
17 |
16
|
ex |
|- ( J e. Top -> ( N e. ( ( nei ` J ) ` S ) -> S C_ N ) ) |
18 |
17
|
3ad2ant1 |
|- ( ( J e. Top /\ N e. J /\ S C_ X ) -> ( N e. ( ( nei ` J ) ` S ) -> S C_ N ) ) |
19 |
15 18
|
impbid |
|- ( ( J e. Top /\ N e. J /\ S C_ X ) -> ( S C_ N <-> N e. ( ( nei ` J ) ` S ) ) ) |