Metamath Proof Explorer

Theorem cldllycmp

Description: A closed subspace of a locally compact space is also locally compact. (The analogous result for open subspaces follows from the more general nllyrest .) (Contributed by Mario Carneiro, 2-Mar-2015)

Ref Expression
Assertion cldllycmp 
|- ( ( J e. N-Locally Comp /\ A e. ( Clsd ` J ) ) -> ( J |`t A ) e. N-Locally Comp )

Proof

Step Hyp Ref Expression
1 nllytop 
 |-  ( J e. N-Locally Comp -> J e. Top )
2 resttop 
 |-  ( ( J e. Top /\ A e. ( Clsd ` J ) ) -> ( J |`t A ) e. Top )
3 1 2 sylan 
 |-  ( ( J e. N-Locally Comp /\ A e. ( Clsd ` J ) ) -> ( J |`t A ) e. Top )
4 elrest 
 |-  ( ( J e. N-Locally Comp /\ A e. ( Clsd ` J ) ) -> ( x e. ( J |`t A ) <-> E. u e. J x = ( u i^i A ) ) )
5 simpll 
 |-  ( ( ( J e. N-Locally Comp /\ A e. ( Clsd ` J ) ) /\ ( u e. J /\ y e. ( u i^i A ) ) ) -> J e. N-Locally Comp )
6 simprl 
 |-  ( ( ( J e. N-Locally Comp /\ A e. ( Clsd ` J ) ) /\ ( u e. J /\ y e. ( u i^i A ) ) ) -> u e. J )
7 simprr 
 |-  ( ( ( J e. N-Locally Comp /\ A e. ( Clsd ` J ) ) /\ ( u e. J /\ y e. ( u i^i A ) ) ) -> y e. ( u i^i A ) )
8 7 elin1d 
 |-  ( ( ( J e. N-Locally Comp /\ A e. ( Clsd ` J ) ) /\ ( u e. J /\ y e. ( u i^i A ) ) ) -> y e. u )
9 nlly2i 
 |-  ( ( J e. N-Locally Comp /\ u e. J /\ y e. u ) -> E. s e. ~P u E. w e. J ( y e. w /\ w C_ s /\ ( J |`t s ) e. Comp ) )
10 5 6 8 9 syl3anc 
 |-  ( ( ( J e. N-Locally Comp /\ A e. ( Clsd ` J ) ) /\ ( u e. J /\ y e. ( u i^i A ) ) ) -> E. s e. ~P u E. w e. J ( y e. w /\ w C_ s /\ ( J |`t s ) e. Comp ) )
11 3 ad2antrr 
 |-  ( ( ( ( J e. N-Locally Comp /\ A e. ( Clsd ` J ) ) /\ ( u e. J /\ y e. ( u i^i A ) ) ) /\ ( ( s e. ~P u /\ w e. J ) /\ ( y e. w /\ w C_ s /\ ( J |`t s ) e. Comp ) ) ) -> ( J |`t A ) e. Top )
12 1 ad3antrrr 
 |-  ( ( ( ( J e. N-Locally Comp /\ A e. ( Clsd ` J ) ) /\ ( u e. J /\ y e. ( u i^i A ) ) ) /\ ( ( s e. ~P u /\ w e. J ) /\ ( y e. w /\ w C_ s /\ ( J |`t s ) e. Comp ) ) ) -> J e. Top )
13 simpllr 
 |-  ( ( ( ( J e. N-Locally Comp /\ A e. ( Clsd ` J ) ) /\ ( u e. J /\ y e. ( u i^i A ) ) ) /\ ( ( s e. ~P u /\ w e. J ) /\ ( y e. w /\ w C_ s /\ ( J |`t s ) e. Comp ) ) ) -> A e. ( Clsd ` J ) )
14 simprlr 
 |-  ( ( ( ( J e. N-Locally Comp /\ A e. ( Clsd ` J ) ) /\ ( u e. J /\ y e. ( u i^i A ) ) ) /\ ( ( s e. ~P u /\ w e. J ) /\ ( y e. w /\ w C_ s /\ ( J |`t s ) e. Comp ) ) ) -> w e. J )
15 elrestr 
 |-  ( ( J e. Top /\ A e. ( Clsd ` J ) /\ w e. J ) -> ( w i^i A ) e. ( J |`t A ) )
16 12 13 14 15 syl3anc 
 |-  ( ( ( ( J e. N-Locally Comp /\ A e. ( Clsd ` J ) ) /\ ( u e. J /\ y e. ( u i^i A ) ) ) /\ ( ( s e. ~P u /\ w e. J ) /\ ( y e. w /\ w C_ s /\ ( J |`t s ) e. Comp ) ) ) -> ( w i^i A ) e. ( J |`t A ) )
17 simprr1 
 |-  ( ( ( ( J e. N-Locally Comp /\ A e. ( Clsd ` J ) ) /\ ( u e. J /\ y e. ( u i^i A ) ) ) /\ ( ( s e. ~P u /\ w e. J ) /\ ( y e. w /\ w C_ s /\ ( J |`t s ) e. Comp ) ) ) -> y e. w )
18 simplrr 
 |-  ( ( ( ( J e. N-Locally Comp /\ A e. ( Clsd ` J ) ) /\ ( u e. J /\ y e. ( u i^i A ) ) ) /\ ( ( s e. ~P u /\ w e. J ) /\ ( y e. w /\ w C_ s /\ ( J |`t s ) e. Comp ) ) ) -> y e. ( u i^i A ) )
19 18 elin2d 
 |-  ( ( ( ( J e. N-Locally Comp /\ A e. ( Clsd ` J ) ) /\ ( u e. J /\ y e. ( u i^i A ) ) ) /\ ( ( s e. ~P u /\ w e. J ) /\ ( y e. w /\ w C_ s /\ ( J |`t s ) e. Comp ) ) ) -> y e. A )
20 17 19 elind 
 |-  ( ( ( ( J e. N-Locally Comp /\ A e. ( Clsd ` J ) ) /\ ( u e. J /\ y e. ( u i^i A ) ) ) /\ ( ( s e. ~P u /\ w e. J ) /\ ( y e. w /\ w C_ s /\ ( J |`t s ) e. Comp ) ) ) -> y e. ( w i^i A ) )
21 opnneip 
 |-  ( ( ( J |`t A ) e. Top /\ ( w i^i A ) e. ( J |`t A ) /\ y e. ( w i^i A ) ) -> ( w i^i A ) e. ( ( nei ` ( J |`t A ) ) ` { y } ) )
22 11 16 20 21 syl3anc 
 |-  ( ( ( ( J e. N-Locally Comp /\ A e. ( Clsd ` J ) ) /\ ( u e. J /\ y e. ( u i^i A ) ) ) /\ ( ( s e. ~P u /\ w e. J ) /\ ( y e. w /\ w C_ s /\ ( J |`t s ) e. Comp ) ) ) -> ( w i^i A ) e. ( ( nei ` ( J |`t A ) ) ` { y } ) )
23 simprr2 
 |-  ( ( ( ( J e. N-Locally Comp /\ A e. ( Clsd ` J ) ) /\ ( u e. J /\ y e. ( u i^i A ) ) ) /\ ( ( s e. ~P u /\ w e. J ) /\ ( y e. w /\ w C_ s /\ ( J |`t s ) e. Comp ) ) ) -> w C_ s )
24 23 ssrind 
 |-  ( ( ( ( J e. N-Locally Comp /\ A e. ( Clsd ` J ) ) /\ ( u e. J /\ y e. ( u i^i A ) ) ) /\ ( ( s e. ~P u /\ w e. J ) /\ ( y e. w /\ w C_ s /\ ( J |`t s ) e. Comp ) ) ) -> ( w i^i A ) C_ ( s i^i A ) )
25 inss2 
 |-  ( s i^i A ) C_ A
26 eqid 
 |-  U. J = U. J
27 26 cldss 
 |-  ( A e. ( Clsd ` J ) -> A C_ U. J )
28 13 27 syl 
 |-  ( ( ( ( J e. N-Locally Comp /\ A e. ( Clsd ` J ) ) /\ ( u e. J /\ y e. ( u i^i A ) ) ) /\ ( ( s e. ~P u /\ w e. J ) /\ ( y e. w /\ w C_ s /\ ( J |`t s ) e. Comp ) ) ) -> A C_ U. J )
29 26 restuni 
 |-  ( ( J e. Top /\ A C_ U. J ) -> A = U. ( J |`t A ) )
30 12 28 29 syl2anc 
 |-  ( ( ( ( J e. N-Locally Comp /\ A e. ( Clsd ` J ) ) /\ ( u e. J /\ y e. ( u i^i A ) ) ) /\ ( ( s e. ~P u /\ w e. J ) /\ ( y e. w /\ w C_ s /\ ( J |`t s ) e. Comp ) ) ) -> A = U. ( J |`t A ) )
31 25 30 sseqtrid 
 |-  ( ( ( ( J e. N-Locally Comp /\ A e. ( Clsd ` J ) ) /\ ( u e. J /\ y e. ( u i^i A ) ) ) /\ ( ( s e. ~P u /\ w e. J ) /\ ( y e. w /\ w C_ s /\ ( J |`t s ) e. Comp ) ) ) -> ( s i^i A ) C_ U. ( J |`t A ) )
32 eqid 
 |-  U. ( J |`t A ) = U. ( J |`t A )
33 32 ssnei2 
 |-  ( ( ( ( J |`t A ) e. Top /\ ( w i^i A ) e. ( ( nei ` ( J |`t A ) ) ` { y } ) ) /\ ( ( w i^i A ) C_ ( s i^i A ) /\ ( s i^i A ) C_ U. ( J |`t A ) ) ) -> ( s i^i A ) e. ( ( nei ` ( J |`t A ) ) ` { y } ) )
34 11 22 24 31 33 syl22anc 
 |-  ( ( ( ( J e. N-Locally Comp /\ A e. ( Clsd ` J ) ) /\ ( u e. J /\ y e. ( u i^i A ) ) ) /\ ( ( s e. ~P u /\ w e. J ) /\ ( y e. w /\ w C_ s /\ ( J |`t s ) e. Comp ) ) ) -> ( s i^i A ) e. ( ( nei ` ( J |`t A ) ) ` { y } ) )
35 simprll 
 |-  ( ( ( ( J e. N-Locally Comp /\ A e. ( Clsd ` J ) ) /\ ( u e. J /\ y e. ( u i^i A ) ) ) /\ ( ( s e. ~P u /\ w e. J ) /\ ( y e. w /\ w C_ s /\ ( J |`t s ) e. Comp ) ) ) -> s e. ~P u )
36 35 elpwid 
 |-  ( ( ( ( J e. N-Locally Comp /\ A e. ( Clsd ` J ) ) /\ ( u e. J /\ y e. ( u i^i A ) ) ) /\ ( ( s e. ~P u /\ w e. J ) /\ ( y e. w /\ w C_ s /\ ( J |`t s ) e. Comp ) ) ) -> s C_ u )
37 36 ssrind 
 |-  ( ( ( ( J e. N-Locally Comp /\ A e. ( Clsd ` J ) ) /\ ( u e. J /\ y e. ( u i^i A ) ) ) /\ ( ( s e. ~P u /\ w e. J ) /\ ( y e. w /\ w C_ s /\ ( J |`t s ) e. Comp ) ) ) -> ( s i^i A ) C_ ( u i^i A ) )
38 vex 
 |-  s e. _V
39 38 inex1 
 |-  ( s i^i A ) e. _V
40 39 elpw 
 |-  ( ( s i^i A ) e. ~P ( u i^i A ) <-> ( s i^i A ) C_ ( u i^i A ) )
41 37 40 sylibr 
 |-  ( ( ( ( J e. N-Locally Comp /\ A e. ( Clsd ` J ) ) /\ ( u e. J /\ y e. ( u i^i A ) ) ) /\ ( ( s e. ~P u /\ w e. J ) /\ ( y e. w /\ w C_ s /\ ( J |`t s ) e. Comp ) ) ) -> ( s i^i A ) e. ~P ( u i^i A ) )
42 34 41 elind 
 |-  ( ( ( ( J e. N-Locally Comp /\ A e. ( Clsd ` J ) ) /\ ( u e. J /\ y e. ( u i^i A ) ) ) /\ ( ( s e. ~P u /\ w e. J ) /\ ( y e. w /\ w C_ s /\ ( J |`t s ) e. Comp ) ) ) -> ( s i^i A ) e. ( ( ( nei ` ( J |`t A ) ) ` { y } ) i^i ~P ( u i^i A ) ) )
43 25 a1i 
 |-  ( ( ( ( J e. N-Locally Comp /\ A e. ( Clsd ` J ) ) /\ ( u e. J /\ y e. ( u i^i A ) ) ) /\ ( ( s e. ~P u /\ w e. J ) /\ ( y e. w /\ w C_ s /\ ( J |`t s ) e. Comp ) ) ) -> ( s i^i A ) C_ A )
44 restabs 
 |-  ( ( J e. Top /\ ( s i^i A ) C_ A /\ A e. ( Clsd ` J ) ) -> ( ( J |`t A ) |`t ( s i^i A ) ) = ( J |`t ( s i^i A ) ) )
45 12 43 13 44 syl3anc 
 |-  ( ( ( ( J e. N-Locally Comp /\ A e. ( Clsd ` J ) ) /\ ( u e. J /\ y e. ( u i^i A ) ) ) /\ ( ( s e. ~P u /\ w e. J ) /\ ( y e. w /\ w C_ s /\ ( J |`t s ) e. Comp ) ) ) -> ( ( J |`t A ) |`t ( s i^i A ) ) = ( J |`t ( s i^i A ) ) )
46 inss1 
 |-  ( s i^i A ) C_ s
47 46 a1i 
 |-  ( ( ( ( J e. N-Locally Comp /\ A e. ( Clsd ` J ) ) /\ ( u e. J /\ y e. ( u i^i A ) ) ) /\ ( ( s e. ~P u /\ w e. J ) /\ ( y e. w /\ w C_ s /\ ( J |`t s ) e. Comp ) ) ) -> ( s i^i A ) C_ s )
48 restabs 
 |-  ( ( J e. Top /\ ( s i^i A ) C_ s /\ s e. ~P u ) -> ( ( J |`t s ) |`t ( s i^i A ) ) = ( J |`t ( s i^i A ) ) )
49 12 47 35 48 syl3anc 
 |-  ( ( ( ( J e. N-Locally Comp /\ A e. ( Clsd ` J ) ) /\ ( u e. J /\ y e. ( u i^i A ) ) ) /\ ( ( s e. ~P u /\ w e. J ) /\ ( y e. w /\ w C_ s /\ ( J |`t s ) e. Comp ) ) ) -> ( ( J |`t s ) |`t ( s i^i A ) ) = ( J |`t ( s i^i A ) ) )
50 45 49 eqtr4d 
 |-  ( ( ( ( J e. N-Locally Comp /\ A e. ( Clsd ` J ) ) /\ ( u e. J /\ y e. ( u i^i A ) ) ) /\ ( ( s e. ~P u /\ w e. J ) /\ ( y e. w /\ w C_ s /\ ( J |`t s ) e. Comp ) ) ) -> ( ( J |`t A ) |`t ( s i^i A ) ) = ( ( J |`t s ) |`t ( s i^i A ) ) )
51 simprr3 
 |-  ( ( ( ( J e. N-Locally Comp /\ A e. ( Clsd ` J ) ) /\ ( u e. J /\ y e. ( u i^i A ) ) ) /\ ( ( s e. ~P u /\ w e. J ) /\ ( y e. w /\ w C_ s /\ ( J |`t s ) e. Comp ) ) ) -> ( J |`t s ) e. Comp )
52 incom 
 |-  ( s i^i A ) = ( A i^i s )
53 eqid 
 |-  ( A i^i s ) = ( A i^i s )
54 ineq1 
 |-  ( v = A -> ( v i^i s ) = ( A i^i s ) )
55 54 rspceeqv 
 |-  ( ( A e. ( Clsd ` J ) /\ ( A i^i s ) = ( A i^i s ) ) -> E. v e. ( Clsd ` J ) ( A i^i s ) = ( v i^i s ) )
56 13 53 55 sylancl 
 |-  ( ( ( ( J e. N-Locally Comp /\ A e. ( Clsd ` J ) ) /\ ( u e. J /\ y e. ( u i^i A ) ) ) /\ ( ( s e. ~P u /\ w e. J ) /\ ( y e. w /\ w C_ s /\ ( J |`t s ) e. Comp ) ) ) -> E. v e. ( Clsd ` J ) ( A i^i s ) = ( v i^i s ) )
57 simplrl 
 |-  ( ( ( ( J e. N-Locally Comp /\ A e. ( Clsd ` J ) ) /\ ( u e. J /\ y e. ( u i^i A ) ) ) /\ ( ( s e. ~P u /\ w e. J ) /\ ( y e. w /\ w C_ s /\ ( J |`t s ) e. Comp ) ) ) -> u e. J )
58 elssuni 
 |-  ( u e. J -> u C_ U. J )
59 57 58 syl 
 |-  ( ( ( ( J e. N-Locally Comp /\ A e. ( Clsd ` J ) ) /\ ( u e. J /\ y e. ( u i^i A ) ) ) /\ ( ( s e. ~P u /\ w e. J ) /\ ( y e. w /\ w C_ s /\ ( J |`t s ) e. Comp ) ) ) -> u C_ U. J )
60 36 59 sstrd 
 |-  ( ( ( ( J e. N-Locally Comp /\ A e. ( Clsd ` J ) ) /\ ( u e. J /\ y e. ( u i^i A ) ) ) /\ ( ( s e. ~P u /\ w e. J ) /\ ( y e. w /\ w C_ s /\ ( J |`t s ) e. Comp ) ) ) -> s C_ U. J )
61 26 restcld 
 |-  ( ( J e. Top /\ s C_ U. J ) -> ( ( A i^i s ) e. ( Clsd ` ( J |`t s ) ) <-> E. v e. ( Clsd ` J ) ( A i^i s ) = ( v i^i s ) ) )
62 12 60 61 syl2anc 
 |-  ( ( ( ( J e. N-Locally Comp /\ A e. ( Clsd ` J ) ) /\ ( u e. J /\ y e. ( u i^i A ) ) ) /\ ( ( s e. ~P u /\ w e. J ) /\ ( y e. w /\ w C_ s /\ ( J |`t s ) e. Comp ) ) ) -> ( ( A i^i s ) e. ( Clsd ` ( J |`t s ) ) <-> E. v e. ( Clsd ` J ) ( A i^i s ) = ( v i^i s ) ) )
63 56 62 mpbird 
 |-  ( ( ( ( J e. N-Locally Comp /\ A e. ( Clsd ` J ) ) /\ ( u e. J /\ y e. ( u i^i A ) ) ) /\ ( ( s e. ~P u /\ w e. J ) /\ ( y e. w /\ w C_ s /\ ( J |`t s ) e. Comp ) ) ) -> ( A i^i s ) e. ( Clsd ` ( J |`t s ) ) )
64 52 63 eqeltrid 
 |-  ( ( ( ( J e. N-Locally Comp /\ A e. ( Clsd ` J ) ) /\ ( u e. J /\ y e. ( u i^i A ) ) ) /\ ( ( s e. ~P u /\ w e. J ) /\ ( y e. w /\ w C_ s /\ ( J |`t s ) e. Comp ) ) ) -> ( s i^i A ) e. ( Clsd ` ( J |`t s ) ) )
65 cmpcld 
 |-  ( ( ( J |`t s ) e. Comp /\ ( s i^i A ) e. ( Clsd ` ( J |`t s ) ) ) -> ( ( J |`t s ) |`t ( s i^i A ) ) e. Comp )
66 51 64 65 syl2anc 
 |-  ( ( ( ( J e. N-Locally Comp /\ A e. ( Clsd ` J ) ) /\ ( u e. J /\ y e. ( u i^i A ) ) ) /\ ( ( s e. ~P u /\ w e. J ) /\ ( y e. w /\ w C_ s /\ ( J |`t s ) e. Comp ) ) ) -> ( ( J |`t s ) |`t ( s i^i A ) ) e. Comp )
67 50 66 eqeltrd 
 |-  ( ( ( ( J e. N-Locally Comp /\ A e. ( Clsd ` J ) ) /\ ( u e. J /\ y e. ( u i^i A ) ) ) /\ ( ( s e. ~P u /\ w e. J ) /\ ( y e. w /\ w C_ s /\ ( J |`t s ) e. Comp ) ) ) -> ( ( J |`t A ) |`t ( s i^i A ) ) e. Comp )
68 oveq2 
 |-  ( v = ( s i^i A ) -> ( ( J |`t A ) |`t v ) = ( ( J |`t A ) |`t ( s i^i A ) ) )
69 68 eleq1d 
 |-  ( v = ( s i^i A ) -> ( ( ( J |`t A ) |`t v ) e. Comp <-> ( ( J |`t A ) |`t ( s i^i A ) ) e. Comp ) )
70 69 rspcev 
 |-  ( ( ( s i^i A ) e. ( ( ( nei ` ( J |`t A ) ) ` { y } ) i^i ~P ( u i^i A ) ) /\ ( ( J |`t A ) |`t ( s i^i A ) ) e. Comp ) -> E. v e. ( ( ( nei ` ( J |`t A ) ) ` { y } ) i^i ~P ( u i^i A ) ) ( ( J |`t A ) |`t v ) e. Comp )
71 42 67 70 syl2anc 
 |-  ( ( ( ( J e. N-Locally Comp /\ A e. ( Clsd ` J ) ) /\ ( u e. J /\ y e. ( u i^i A ) ) ) /\ ( ( s e. ~P u /\ w e. J ) /\ ( y e. w /\ w C_ s /\ ( J |`t s ) e. Comp ) ) ) -> E. v e. ( ( ( nei ` ( J |`t A ) ) ` { y } ) i^i ~P ( u i^i A ) ) ( ( J |`t A ) |`t v ) e. Comp )
72 71 expr 
 |-  ( ( ( ( J e. N-Locally Comp /\ A e. ( Clsd ` J ) ) /\ ( u e. J /\ y e. ( u i^i A ) ) ) /\ ( s e. ~P u /\ w e. J ) ) -> ( ( y e. w /\ w C_ s /\ ( J |`t s ) e. Comp ) -> E. v e. ( ( ( nei ` ( J |`t A ) ) ` { y } ) i^i ~P ( u i^i A ) ) ( ( J |`t A ) |`t v ) e. Comp ) )
73 72 rexlimdvva 
 |-  ( ( ( J e. N-Locally Comp /\ A e. ( Clsd ` J ) ) /\ ( u e. J /\ y e. ( u i^i A ) ) ) -> ( E. s e. ~P u E. w e. J ( y e. w /\ w C_ s /\ ( J |`t s ) e. Comp ) -> E. v e. ( ( ( nei ` ( J |`t A ) ) ` { y } ) i^i ~P ( u i^i A ) ) ( ( J |`t A ) |`t v ) e. Comp ) )
74 10 73 mpd 
 |-  ( ( ( J e. N-Locally Comp /\ A e. ( Clsd ` J ) ) /\ ( u e. J /\ y e. ( u i^i A ) ) ) -> E. v e. ( ( ( nei ` ( J |`t A ) ) ` { y } ) i^i ~P ( u i^i A ) ) ( ( J |`t A ) |`t v ) e. Comp )
75 74 anassrs 
 |-  ( ( ( ( J e. N-Locally Comp /\ A e. ( Clsd ` J ) ) /\ u e. J ) /\ y e. ( u i^i A ) ) -> E. v e. ( ( ( nei ` ( J |`t A ) ) ` { y } ) i^i ~P ( u i^i A ) ) ( ( J |`t A ) |`t v ) e. Comp )
76 75 ralrimiva 
 |-  ( ( ( J e. N-Locally Comp /\ A e. ( Clsd ` J ) ) /\ u e. J ) -> A. y e. ( u i^i A ) E. v e. ( ( ( nei ` ( J |`t A ) ) ` { y } ) i^i ~P ( u i^i A ) ) ( ( J |`t A ) |`t v ) e. Comp )
77 pweq 
 |-  ( x = ( u i^i A ) -> ~P x = ~P ( u i^i A ) )
78 77 ineq2d 
 |-  ( x = ( u i^i A ) -> ( ( ( nei ` ( J |`t A ) ) ` { y } ) i^i ~P x ) = ( ( ( nei ` ( J |`t A ) ) ` { y } ) i^i ~P ( u i^i A ) ) )
79 78 rexeqdv 
 |-  ( x = ( u i^i A ) -> ( E. v e. ( ( ( nei ` ( J |`t A ) ) ` { y } ) i^i ~P x ) ( ( J |`t A ) |`t v ) e. Comp <-> E. v e. ( ( ( nei ` ( J |`t A ) ) ` { y } ) i^i ~P ( u i^i A ) ) ( ( J |`t A ) |`t v ) e. Comp ) )
80 79 raleqbi1dv 
 |-  ( x = ( u i^i A ) -> ( A. y e. x E. v e. ( ( ( nei ` ( J |`t A ) ) ` { y } ) i^i ~P x ) ( ( J |`t A ) |`t v ) e. Comp <-> A. y e. ( u i^i A ) E. v e. ( ( ( nei ` ( J |`t A ) ) ` { y } ) i^i ~P ( u i^i A ) ) ( ( J |`t A ) |`t v ) e. Comp ) )
81 76 80 syl5ibrcom 
 |-  ( ( ( J e. N-Locally Comp /\ A e. ( Clsd ` J ) ) /\ u e. J ) -> ( x = ( u i^i A ) -> A. y e. x E. v e. ( ( ( nei ` ( J |`t A ) ) ` { y } ) i^i ~P x ) ( ( J |`t A ) |`t v ) e. Comp ) )
82 81 rexlimdva 
 |-  ( ( J e. N-Locally Comp /\ A e. ( Clsd ` J ) ) -> ( E. u e. J x = ( u i^i A ) -> A. y e. x E. v e. ( ( ( nei ` ( J |`t A ) ) ` { y } ) i^i ~P x ) ( ( J |`t A ) |`t v ) e. Comp ) )
83 4 82 sylbid 
 |-  ( ( J e. N-Locally Comp /\ A e. ( Clsd ` J ) ) -> ( x e. ( J |`t A ) -> A. y e. x E. v e. ( ( ( nei ` ( J |`t A ) ) ` { y } ) i^i ~P x ) ( ( J |`t A ) |`t v ) e. Comp ) )
84 83 ralrimiv 
 |-  ( ( J e. N-Locally Comp /\ A e. ( Clsd ` J ) ) -> A. x e. ( J |`t A ) A. y e. x E. v e. ( ( ( nei ` ( J |`t A ) ) ` { y } ) i^i ~P x ) ( ( J |`t A ) |`t v ) e. Comp )
85 isnlly 
 |-  ( ( J |`t A ) e. N-Locally Comp <-> ( ( J |`t A ) e. Top /\ A. x e. ( J |`t A ) A. y e. x E. v e. ( ( ( nei ` ( J |`t A ) ) ` { y } ) i^i ~P x ) ( ( J |`t A ) |`t v ) e. Comp ) )
86 3 84 85 sylanbrc 
 |-  ( ( J e. N-Locally Comp /\ A e. ( Clsd ` J ) ) -> ( J |`t A ) e. N-Locally Comp )