Step |
Hyp |
Ref |
Expression |
1 |
|
eqid |
|- U. J = U. J |
2 |
1
|
fclselbas |
|- ( A e. ( J fClus F ) -> A e. U. J ) |
3 |
|
toponuni |
|- ( J e. ( TopOn ` X ) -> X = U. J ) |
4 |
3
|
adantr |
|- ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) -> X = U. J ) |
5 |
4
|
eleq2d |
|- ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) -> ( A e. X <-> A e. U. J ) ) |
6 |
2 5
|
syl5ibr |
|- ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) -> ( A e. ( J fClus F ) -> A e. X ) ) |
7 |
|
fclsneii |
|- ( ( A e. ( J fClus F ) /\ n e. ( ( nei ` J ) ` { A } ) /\ s e. F ) -> ( n i^i s ) =/= (/) ) |
8 |
7
|
3expb |
|- ( ( A e. ( J fClus F ) /\ ( n e. ( ( nei ` J ) ` { A } ) /\ s e. F ) ) -> ( n i^i s ) =/= (/) ) |
9 |
8
|
ralrimivva |
|- ( A e. ( J fClus F ) -> A. n e. ( ( nei ` J ) ` { A } ) A. s e. F ( n i^i s ) =/= (/) ) |
10 |
6 9
|
jca2 |
|- ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) -> ( A e. ( J fClus F ) -> ( A e. X /\ A. n e. ( ( nei ` J ) ` { A } ) A. s e. F ( n i^i s ) =/= (/) ) ) ) |
11 |
|
topontop |
|- ( J e. ( TopOn ` X ) -> J e. Top ) |
12 |
11
|
ad3antrrr |
|- ( ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) /\ A e. X ) /\ ( o e. J /\ A e. o ) ) -> J e. Top ) |
13 |
|
simprl |
|- ( ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) /\ A e. X ) /\ ( o e. J /\ A e. o ) ) -> o e. J ) |
14 |
|
simprr |
|- ( ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) /\ A e. X ) /\ ( o e. J /\ A e. o ) ) -> A e. o ) |
15 |
|
opnneip |
|- ( ( J e. Top /\ o e. J /\ A e. o ) -> o e. ( ( nei ` J ) ` { A } ) ) |
16 |
12 13 14 15
|
syl3anc |
|- ( ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) /\ A e. X ) /\ ( o e. J /\ A e. o ) ) -> o e. ( ( nei ` J ) ` { A } ) ) |
17 |
|
ineq1 |
|- ( n = o -> ( n i^i s ) = ( o i^i s ) ) |
18 |
17
|
neeq1d |
|- ( n = o -> ( ( n i^i s ) =/= (/) <-> ( o i^i s ) =/= (/) ) ) |
19 |
18
|
ralbidv |
|- ( n = o -> ( A. s e. F ( n i^i s ) =/= (/) <-> A. s e. F ( o i^i s ) =/= (/) ) ) |
20 |
19
|
rspcv |
|- ( o e. ( ( nei ` J ) ` { A } ) -> ( A. n e. ( ( nei ` J ) ` { A } ) A. s e. F ( n i^i s ) =/= (/) -> A. s e. F ( o i^i s ) =/= (/) ) ) |
21 |
16 20
|
syl |
|- ( ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) /\ A e. X ) /\ ( o e. J /\ A e. o ) ) -> ( A. n e. ( ( nei ` J ) ` { A } ) A. s e. F ( n i^i s ) =/= (/) -> A. s e. F ( o i^i s ) =/= (/) ) ) |
22 |
21
|
expr |
|- ( ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) /\ A e. X ) /\ o e. J ) -> ( A e. o -> ( A. n e. ( ( nei ` J ) ` { A } ) A. s e. F ( n i^i s ) =/= (/) -> A. s e. F ( o i^i s ) =/= (/) ) ) ) |
23 |
22
|
com23 |
|- ( ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) /\ A e. X ) /\ o e. J ) -> ( A. n e. ( ( nei ` J ) ` { A } ) A. s e. F ( n i^i s ) =/= (/) -> ( A e. o -> A. s e. F ( o i^i s ) =/= (/) ) ) ) |
24 |
23
|
ralrimdva |
|- ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) /\ A e. X ) -> ( A. n e. ( ( nei ` J ) ` { A } ) A. s e. F ( n i^i s ) =/= (/) -> A. o e. J ( A e. o -> A. s e. F ( o i^i s ) =/= (/) ) ) ) |
25 |
24
|
imdistanda |
|- ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) -> ( ( A e. X /\ A. n e. ( ( nei ` J ) ` { A } ) A. s e. F ( n i^i s ) =/= (/) ) -> ( A e. X /\ A. o e. J ( A e. o -> A. s e. F ( o i^i s ) =/= (/) ) ) ) ) |
26 |
|
fclsopn |
|- ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) -> ( A e. ( J fClus F ) <-> ( A e. X /\ A. o e. J ( A e. o -> A. s e. F ( o i^i s ) =/= (/) ) ) ) ) |
27 |
25 26
|
sylibrd |
|- ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) -> ( ( A e. X /\ A. n e. ( ( nei ` J ) ` { A } ) A. s e. F ( n i^i s ) =/= (/) ) -> A e. ( J fClus F ) ) ) |
28 |
10 27
|
impbid |
|- ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) -> ( A e. ( J fClus F ) <-> ( A e. X /\ A. n e. ( ( nei ` J ) ` { A } ) A. s e. F ( n i^i s ) =/= (/) ) ) ) |