Step |
Hyp |
Ref |
Expression |
1 |
|
neii2 |
|- ( ( J e. Top /\ N e. ( ( nei ` J ) ` N ) ) -> E. x e. J ( N C_ x /\ x C_ N ) ) |
2 |
|
eqss |
|- ( N = x <-> ( N C_ x /\ x C_ N ) ) |
3 |
|
eleq1a |
|- ( x e. J -> ( N = x -> N e. J ) ) |
4 |
2 3
|
syl5bir |
|- ( x e. J -> ( ( N C_ x /\ x C_ N ) -> N e. J ) ) |
5 |
4
|
rexlimiv |
|- ( E. x e. J ( N C_ x /\ x C_ N ) -> N e. J ) |
6 |
1 5
|
syl |
|- ( ( J e. Top /\ N e. ( ( nei ` J ) ` N ) ) -> N e. J ) |
7 |
6
|
ex |
|- ( J e. Top -> ( N e. ( ( nei ` J ) ` N ) -> N e. J ) ) |
8 |
|
ssid |
|- N C_ N |
9 |
|
opnneiss |
|- ( ( J e. Top /\ N e. J /\ N C_ N ) -> N e. ( ( nei ` J ) ` N ) ) |
10 |
9
|
3exp |
|- ( J e. Top -> ( N e. J -> ( N C_ N -> N e. ( ( nei ` J ) ` N ) ) ) ) |
11 |
8 10
|
mpii |
|- ( J e. Top -> ( N e. J -> N e. ( ( nei ` J ) ` N ) ) ) |
12 |
7 11
|
impbid |
|- ( J e. Top -> ( N e. ( ( nei ` J ) ` N ) <-> N e. J ) ) |