Step |
Hyp |
Ref |
Expression |
1 |
|
neips.1 |
|- X = U. J |
2 |
1
|
clsss3 |
|- ( ( J e. Top /\ S C_ X ) -> ( ( cls ` J ) ` S ) C_ X ) |
3 |
2
|
sseld |
|- ( ( J e. Top /\ S C_ X ) -> ( P e. ( ( cls ` J ) ` S ) -> P e. X ) ) |
4 |
3
|
impr |
|- ( ( J e. Top /\ ( S C_ X /\ P e. ( ( cls ` J ) ` S ) ) ) -> P e. X ) |
5 |
1
|
isneip |
|- ( ( J e. Top /\ P e. X ) -> ( N e. ( ( nei ` J ) ` { P } ) <-> ( N C_ X /\ E. g e. J ( P e. g /\ g C_ N ) ) ) ) |
6 |
4 5
|
syldan |
|- ( ( J e. Top /\ ( S C_ X /\ P e. ( ( cls ` J ) ` S ) ) ) -> ( N e. ( ( nei ` J ) ` { P } ) <-> ( N C_ X /\ E. g e. J ( P e. g /\ g C_ N ) ) ) ) |
7 |
|
3anass |
|- ( ( J e. Top /\ S C_ X /\ P e. ( ( cls ` J ) ` S ) ) <-> ( J e. Top /\ ( S C_ X /\ P e. ( ( cls ` J ) ` S ) ) ) ) |
8 |
1
|
clsndisj |
|- ( ( ( J e. Top /\ S C_ X /\ P e. ( ( cls ` J ) ` S ) ) /\ ( g e. J /\ P e. g ) ) -> ( g i^i S ) =/= (/) ) |
9 |
7 8
|
sylanbr |
|- ( ( ( J e. Top /\ ( S C_ X /\ P e. ( ( cls ` J ) ` S ) ) ) /\ ( g e. J /\ P e. g ) ) -> ( g i^i S ) =/= (/) ) |
10 |
9
|
anassrs |
|- ( ( ( ( J e. Top /\ ( S C_ X /\ P e. ( ( cls ` J ) ` S ) ) ) /\ g e. J ) /\ P e. g ) -> ( g i^i S ) =/= (/) ) |
11 |
10
|
adantllr |
|- ( ( ( ( ( J e. Top /\ ( S C_ X /\ P e. ( ( cls ` J ) ` S ) ) ) /\ N C_ X ) /\ g e. J ) /\ P e. g ) -> ( g i^i S ) =/= (/) ) |
12 |
11
|
adantrr |
|- ( ( ( ( ( J e. Top /\ ( S C_ X /\ P e. ( ( cls ` J ) ` S ) ) ) /\ N C_ X ) /\ g e. J ) /\ ( P e. g /\ g C_ N ) ) -> ( g i^i S ) =/= (/) ) |
13 |
|
ssdisj |
|- ( ( g C_ N /\ ( N i^i S ) = (/) ) -> ( g i^i S ) = (/) ) |
14 |
13
|
ex |
|- ( g C_ N -> ( ( N i^i S ) = (/) -> ( g i^i S ) = (/) ) ) |
15 |
14
|
necon3d |
|- ( g C_ N -> ( ( g i^i S ) =/= (/) -> ( N i^i S ) =/= (/) ) ) |
16 |
15
|
ad2antll |
|- ( ( ( ( ( J e. Top /\ ( S C_ X /\ P e. ( ( cls ` J ) ` S ) ) ) /\ N C_ X ) /\ g e. J ) /\ ( P e. g /\ g C_ N ) ) -> ( ( g i^i S ) =/= (/) -> ( N i^i S ) =/= (/) ) ) |
17 |
12 16
|
mpd |
|- ( ( ( ( ( J e. Top /\ ( S C_ X /\ P e. ( ( cls ` J ) ` S ) ) ) /\ N C_ X ) /\ g e. J ) /\ ( P e. g /\ g C_ N ) ) -> ( N i^i S ) =/= (/) ) |
18 |
17
|
rexlimdva2 |
|- ( ( ( J e. Top /\ ( S C_ X /\ P e. ( ( cls ` J ) ` S ) ) ) /\ N C_ X ) -> ( E. g e. J ( P e. g /\ g C_ N ) -> ( N i^i S ) =/= (/) ) ) |
19 |
18
|
expimpd |
|- ( ( J e. Top /\ ( S C_ X /\ P e. ( ( cls ` J ) ` S ) ) ) -> ( ( N C_ X /\ E. g e. J ( P e. g /\ g C_ N ) ) -> ( N i^i S ) =/= (/) ) ) |
20 |
6 19
|
sylbid |
|- ( ( J e. Top /\ ( S C_ X /\ P e. ( ( cls ` J ) ` S ) ) ) -> ( N e. ( ( nei ` J ) ` { P } ) -> ( N i^i S ) =/= (/) ) ) |
21 |
20
|
exp32 |
|- ( J e. Top -> ( S C_ X -> ( P e. ( ( cls ` J ) ` S ) -> ( N e. ( ( nei ` J ) ` { P } ) -> ( N i^i S ) =/= (/) ) ) ) ) |
22 |
21
|
imp43 |
|- ( ( ( J e. Top /\ S C_ X ) /\ ( P e. ( ( cls ` J ) ` S ) /\ N e. ( ( nei ` J ) ` { P } ) ) ) -> ( N i^i S ) =/= (/) ) |