Step |
Hyp |
Ref |
Expression |
1 |
|
tpnei.1 |
|- X = U. J |
2 |
1
|
elcls |
|- ( ( J e. Top /\ S C_ X /\ P e. X ) -> ( P e. ( ( cls ` J ) ` S ) <-> A. x e. J ( P e. x -> ( x i^i S ) =/= (/) ) ) ) |
3 |
1
|
isneip |
|- ( ( J e. Top /\ P e. X ) -> ( n e. ( ( nei ` J ) ` { P } ) <-> ( n C_ X /\ E. x e. J ( P e. x /\ x C_ n ) ) ) ) |
4 |
|
r19.29r |
|- ( ( E. x e. J ( P e. x /\ x C_ n ) /\ A. x e. J ( P e. x -> ( x i^i S ) =/= (/) ) ) -> E. x e. J ( ( P e. x /\ x C_ n ) /\ ( P e. x -> ( x i^i S ) =/= (/) ) ) ) |
5 |
|
pm3.35 |
|- ( ( P e. x /\ ( P e. x -> ( x i^i S ) =/= (/) ) ) -> ( x i^i S ) =/= (/) ) |
6 |
|
ssrin |
|- ( x C_ n -> ( x i^i S ) C_ ( n i^i S ) ) |
7 |
|
sseq2 |
|- ( ( n i^i S ) = (/) -> ( ( x i^i S ) C_ ( n i^i S ) <-> ( x i^i S ) C_ (/) ) ) |
8 |
|
ss0 |
|- ( ( x i^i S ) C_ (/) -> ( x i^i S ) = (/) ) |
9 |
7 8
|
syl6bi |
|- ( ( n i^i S ) = (/) -> ( ( x i^i S ) C_ ( n i^i S ) -> ( x i^i S ) = (/) ) ) |
10 |
6 9
|
syl5com |
|- ( x C_ n -> ( ( n i^i S ) = (/) -> ( x i^i S ) = (/) ) ) |
11 |
10
|
necon3d |
|- ( x C_ n -> ( ( x i^i S ) =/= (/) -> ( n i^i S ) =/= (/) ) ) |
12 |
5 11
|
syl5com |
|- ( ( P e. x /\ ( P e. x -> ( x i^i S ) =/= (/) ) ) -> ( x C_ n -> ( n i^i S ) =/= (/) ) ) |
13 |
12
|
ex |
|- ( P e. x -> ( ( P e. x -> ( x i^i S ) =/= (/) ) -> ( x C_ n -> ( n i^i S ) =/= (/) ) ) ) |
14 |
13
|
com23 |
|- ( P e. x -> ( x C_ n -> ( ( P e. x -> ( x i^i S ) =/= (/) ) -> ( n i^i S ) =/= (/) ) ) ) |
15 |
14
|
imp31 |
|- ( ( ( P e. x /\ x C_ n ) /\ ( P e. x -> ( x i^i S ) =/= (/) ) ) -> ( n i^i S ) =/= (/) ) |
16 |
15
|
rexlimivw |
|- ( E. x e. J ( ( P e. x /\ x C_ n ) /\ ( P e. x -> ( x i^i S ) =/= (/) ) ) -> ( n i^i S ) =/= (/) ) |
17 |
4 16
|
syl |
|- ( ( E. x e. J ( P e. x /\ x C_ n ) /\ A. x e. J ( P e. x -> ( x i^i S ) =/= (/) ) ) -> ( n i^i S ) =/= (/) ) |
18 |
17
|
ex |
|- ( E. x e. J ( P e. x /\ x C_ n ) -> ( A. x e. J ( P e. x -> ( x i^i S ) =/= (/) ) -> ( n i^i S ) =/= (/) ) ) |
19 |
18
|
adantl |
|- ( ( n C_ X /\ E. x e. J ( P e. x /\ x C_ n ) ) -> ( A. x e. J ( P e. x -> ( x i^i S ) =/= (/) ) -> ( n i^i S ) =/= (/) ) ) |
20 |
3 19
|
syl6bi |
|- ( ( J e. Top /\ P e. X ) -> ( n e. ( ( nei ` J ) ` { P } ) -> ( A. x e. J ( P e. x -> ( x i^i S ) =/= (/) ) -> ( n i^i S ) =/= (/) ) ) ) |
21 |
20
|
3adant2 |
|- ( ( J e. Top /\ S C_ X /\ P e. X ) -> ( n e. ( ( nei ` J ) ` { P } ) -> ( A. x e. J ( P e. x -> ( x i^i S ) =/= (/) ) -> ( n i^i S ) =/= (/) ) ) ) |
22 |
21
|
com23 |
|- ( ( J e. Top /\ S C_ X /\ P e. X ) -> ( A. x e. J ( P e. x -> ( x i^i S ) =/= (/) ) -> ( n e. ( ( nei ` J ) ` { P } ) -> ( n i^i S ) =/= (/) ) ) ) |
23 |
22
|
imp |
|- ( ( ( J e. Top /\ S C_ X /\ P e. X ) /\ A. x e. J ( P e. x -> ( x i^i S ) =/= (/) ) ) -> ( n e. ( ( nei ` J ) ` { P } ) -> ( n i^i S ) =/= (/) ) ) |
24 |
23
|
ralrimiv |
|- ( ( ( J e. Top /\ S C_ X /\ P e. X ) /\ A. x e. J ( P e. x -> ( x i^i S ) =/= (/) ) ) -> A. n e. ( ( nei ` J ) ` { P } ) ( n i^i S ) =/= (/) ) |
25 |
|
opnneip |
|- ( ( J e. Top /\ x e. J /\ P e. x ) -> x e. ( ( nei ` J ) ` { P } ) ) |
26 |
|
ineq1 |
|- ( n = x -> ( n i^i S ) = ( x i^i S ) ) |
27 |
26
|
neeq1d |
|- ( n = x -> ( ( n i^i S ) =/= (/) <-> ( x i^i S ) =/= (/) ) ) |
28 |
27
|
rspccva |
|- ( ( A. n e. ( ( nei ` J ) ` { P } ) ( n i^i S ) =/= (/) /\ x e. ( ( nei ` J ) ` { P } ) ) -> ( x i^i S ) =/= (/) ) |
29 |
|
idd |
|- ( ( P e. X /\ ( J e. Top /\ x e. J /\ P e. x ) /\ S C_ X ) -> ( ( x i^i S ) =/= (/) -> ( x i^i S ) =/= (/) ) ) |
30 |
29
|
3exp |
|- ( P e. X -> ( ( J e. Top /\ x e. J /\ P e. x ) -> ( S C_ X -> ( ( x i^i S ) =/= (/) -> ( x i^i S ) =/= (/) ) ) ) ) |
31 |
30
|
com14 |
|- ( ( x i^i S ) =/= (/) -> ( ( J e. Top /\ x e. J /\ P e. x ) -> ( S C_ X -> ( P e. X -> ( x i^i S ) =/= (/) ) ) ) ) |
32 |
28 31
|
syl |
|- ( ( A. n e. ( ( nei ` J ) ` { P } ) ( n i^i S ) =/= (/) /\ x e. ( ( nei ` J ) ` { P } ) ) -> ( ( J e. Top /\ x e. J /\ P e. x ) -> ( S C_ X -> ( P e. X -> ( x i^i S ) =/= (/) ) ) ) ) |
33 |
32
|
ex |
|- ( A. n e. ( ( nei ` J ) ` { P } ) ( n i^i S ) =/= (/) -> ( x e. ( ( nei ` J ) ` { P } ) -> ( ( J e. Top /\ x e. J /\ P e. x ) -> ( S C_ X -> ( P e. X -> ( x i^i S ) =/= (/) ) ) ) ) ) |
34 |
33
|
com3l |
|- ( x e. ( ( nei ` J ) ` { P } ) -> ( ( J e. Top /\ x e. J /\ P e. x ) -> ( A. n e. ( ( nei ` J ) ` { P } ) ( n i^i S ) =/= (/) -> ( S C_ X -> ( P e. X -> ( x i^i S ) =/= (/) ) ) ) ) ) |
35 |
25 34
|
mpcom |
|- ( ( J e. Top /\ x e. J /\ P e. x ) -> ( A. n e. ( ( nei ` J ) ` { P } ) ( n i^i S ) =/= (/) -> ( S C_ X -> ( P e. X -> ( x i^i S ) =/= (/) ) ) ) ) |
36 |
35
|
3expia |
|- ( ( J e. Top /\ x e. J ) -> ( P e. x -> ( A. n e. ( ( nei ` J ) ` { P } ) ( n i^i S ) =/= (/) -> ( S C_ X -> ( P e. X -> ( x i^i S ) =/= (/) ) ) ) ) ) |
37 |
36
|
com25 |
|- ( ( J e. Top /\ x e. J ) -> ( P e. X -> ( A. n e. ( ( nei ` J ) ` { P } ) ( n i^i S ) =/= (/) -> ( S C_ X -> ( P e. x -> ( x i^i S ) =/= (/) ) ) ) ) ) |
38 |
37
|
ex |
|- ( J e. Top -> ( x e. J -> ( P e. X -> ( A. n e. ( ( nei ` J ) ` { P } ) ( n i^i S ) =/= (/) -> ( S C_ X -> ( P e. x -> ( x i^i S ) =/= (/) ) ) ) ) ) ) |
39 |
38
|
com25 |
|- ( J e. Top -> ( S C_ X -> ( P e. X -> ( A. n e. ( ( nei ` J ) ` { P } ) ( n i^i S ) =/= (/) -> ( x e. J -> ( P e. x -> ( x i^i S ) =/= (/) ) ) ) ) ) ) |
40 |
39
|
3imp1 |
|- ( ( ( J e. Top /\ S C_ X /\ P e. X ) /\ A. n e. ( ( nei ` J ) ` { P } ) ( n i^i S ) =/= (/) ) -> ( x e. J -> ( P e. x -> ( x i^i S ) =/= (/) ) ) ) |
41 |
40
|
ralrimiv |
|- ( ( ( J e. Top /\ S C_ X /\ P e. X ) /\ A. n e. ( ( nei ` J ) ` { P } ) ( n i^i S ) =/= (/) ) -> A. x e. J ( P e. x -> ( x i^i S ) =/= (/) ) ) |
42 |
24 41
|
impbida |
|- ( ( J e. Top /\ S C_ X /\ P e. X ) -> ( A. x e. J ( P e. x -> ( x i^i S ) =/= (/) ) <-> A. n e. ( ( nei ` J ) ` { P } ) ( n i^i S ) =/= (/) ) ) |
43 |
2 42
|
bitrd |
|- ( ( J e. Top /\ S C_ X /\ P e. X ) -> ( P e. ( ( cls ` J ) ` S ) <-> A. n e. ( ( nei ` J ) ` { P } ) ( n i^i S ) =/= (/) ) ) |