Step |
Hyp |
Ref |
Expression |
1 |
|
eqid |
|- U. J = U. J |
2 |
1
|
fclsfil |
|- ( A e. ( J fClus F ) -> F e. ( Fil ` U. J ) ) |
3 |
|
fclstopon |
|- ( A e. ( J fClus F ) -> ( J e. ( TopOn ` U. J ) <-> F e. ( Fil ` U. J ) ) ) |
4 |
2 3
|
mpbird |
|- ( A e. ( J fClus F ) -> J e. ( TopOn ` U. J ) ) |
5 |
|
fclsopn |
|- ( ( J e. ( TopOn ` U. J ) /\ F e. ( Fil ` U. J ) ) -> ( A e. ( J fClus F ) <-> ( A e. U. J /\ A. o e. J ( A e. o -> A. s e. F ( o i^i s ) =/= (/) ) ) ) ) |
6 |
4 2 5
|
syl2anc |
|- ( A e. ( J fClus F ) -> ( A e. ( J fClus F ) <-> ( A e. U. J /\ A. o e. J ( A e. o -> A. s e. F ( o i^i s ) =/= (/) ) ) ) ) |
7 |
6
|
ibi |
|- ( A e. ( J fClus F ) -> ( A e. U. J /\ A. o e. J ( A e. o -> A. s e. F ( o i^i s ) =/= (/) ) ) ) |
8 |
|
eleq2 |
|- ( o = U -> ( A e. o <-> A e. U ) ) |
9 |
|
ineq1 |
|- ( o = U -> ( o i^i s ) = ( U i^i s ) ) |
10 |
9
|
neeq1d |
|- ( o = U -> ( ( o i^i s ) =/= (/) <-> ( U i^i s ) =/= (/) ) ) |
11 |
10
|
ralbidv |
|- ( o = U -> ( A. s e. F ( o i^i s ) =/= (/) <-> A. s e. F ( U i^i s ) =/= (/) ) ) |
12 |
8 11
|
imbi12d |
|- ( o = U -> ( ( A e. o -> A. s e. F ( o i^i s ) =/= (/) ) <-> ( A e. U -> A. s e. F ( U i^i s ) =/= (/) ) ) ) |
13 |
12
|
rspccv |
|- ( A. o e. J ( A e. o -> A. s e. F ( o i^i s ) =/= (/) ) -> ( U e. J -> ( A e. U -> A. s e. F ( U i^i s ) =/= (/) ) ) ) |
14 |
7 13
|
simpl2im |
|- ( A e. ( J fClus F ) -> ( U e. J -> ( A e. U -> A. s e. F ( U i^i s ) =/= (/) ) ) ) |
15 |
|
ineq2 |
|- ( s = S -> ( U i^i s ) = ( U i^i S ) ) |
16 |
15
|
neeq1d |
|- ( s = S -> ( ( U i^i s ) =/= (/) <-> ( U i^i S ) =/= (/) ) ) |
17 |
16
|
rspccv |
|- ( A. s e. F ( U i^i s ) =/= (/) -> ( S e. F -> ( U i^i S ) =/= (/) ) ) |
18 |
14 17
|
syl8 |
|- ( A e. ( J fClus F ) -> ( U e. J -> ( A e. U -> ( S e. F -> ( U i^i S ) =/= (/) ) ) ) ) |
19 |
18
|
3imp2 |
|- ( ( A e. ( J fClus F ) /\ ( U e. J /\ A e. U /\ S e. F ) ) -> ( U i^i S ) =/= (/) ) |