Metamath Proof Explorer

Theorem fclscf

Description: Characterization of fineness of topologies in terms of cluster points. (Contributed by Jeff Hankins, 12-Nov-2009) (Revised by Stefan O'Rear, 8-Aug-2015)

Ref Expression
Assertion fclscf 
|- ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) -> ( J C_ K <-> A. f e. ( Fil ` X ) ( K fClus f ) C_ ( J fClus f ) ) )

Proof

Step Hyp Ref Expression
1 simpll 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ ( J C_ K /\ x e. ( K fClus f ) ) ) -> J e. ( TopOn ` X ) )
2 simplr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ ( J C_ K /\ x e. ( K fClus f ) ) ) -> K e. ( TopOn ` X ) )
3 fclstopon 
 |-  ( x e. ( K fClus f ) -> ( K e. ( TopOn ` X ) <-> f e. ( Fil ` X ) ) )
4 3 ad2antll 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ ( J C_ K /\ x e. ( K fClus f ) ) ) -> ( K e. ( TopOn ` X ) <-> f e. ( Fil ` X ) ) )
5 2 4 mpbid 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ ( J C_ K /\ x e. ( K fClus f ) ) ) -> f e. ( Fil ` X ) )
6 simprl 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ ( J C_ K /\ x e. ( K fClus f ) ) ) -> J C_ K )
7 fclsss1 
 |-  ( ( J e. ( TopOn ` X ) /\ f e. ( Fil ` X ) /\ J C_ K ) -> ( K fClus f ) C_ ( J fClus f ) )
8 1 5 6 7 syl3anc 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ ( J C_ K /\ x e. ( K fClus f ) ) ) -> ( K fClus f ) C_ ( J fClus f ) )
9 simprr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ ( J C_ K /\ x e. ( K fClus f ) ) ) -> x e. ( K fClus f ) )
10 8 9 sseldd 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ ( J C_ K /\ x e. ( K fClus f ) ) ) -> x e. ( J fClus f ) )
11 10 expr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ J C_ K ) -> ( x e. ( K fClus f ) -> x e. ( J fClus f ) ) )
12 11 ssrdv 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ J C_ K ) -> ( K fClus f ) C_ ( J fClus f ) )
13 12 ralrimivw 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ J C_ K ) -> A. f e. ( Fil ` X ) ( K fClus f ) C_ ( J fClus f ) )
14 simpllr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fClus f ) C_ ( J fClus f ) ) /\ x e. J ) -> K e. ( TopOn ` X ) )
15 toponmax 
 |-  ( K e. ( TopOn ` X ) -> X e. K )
16 ssid 
 |-  X C_ X
17 eleq2 
 |-  ( u = X -> ( y e. u <-> y e. X ) )
18 sseq1 
 |-  ( u = X -> ( u C_ X <-> X C_ X ) )
19 17 18 anbi12d 
 |-  ( u = X -> ( ( y e. u /\ u C_ X ) <-> ( y e. X /\ X C_ X ) ) )
20 19 rspcev 
 |-  ( ( X e. K /\ ( y e. X /\ X C_ X ) ) -> E. u e. K ( y e. u /\ u C_ X ) )
21 16 20 mpanr2 
 |-  ( ( X e. K /\ y e. X ) -> E. u e. K ( y e. u /\ u C_ X ) )
22 21 ex 
 |-  ( X e. K -> ( y e. X -> E. u e. K ( y e. u /\ u C_ X ) ) )
23 14 15 22 3syl 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fClus f ) C_ ( J fClus f ) ) /\ x e. J ) -> ( y e. X -> E. u e. K ( y e. u /\ u C_ X ) ) )
24 eleq2 
 |-  ( x = X -> ( y e. x <-> y e. X ) )
25 sseq2 
 |-  ( x = X -> ( u C_ x <-> u C_ X ) )
26 25 anbi2d 
 |-  ( x = X -> ( ( y e. u /\ u C_ x ) <-> ( y e. u /\ u C_ X ) ) )
27 26 rexbidv 
 |-  ( x = X -> ( E. u e. K ( y e. u /\ u C_ x ) <-> E. u e. K ( y e. u /\ u C_ X ) ) )
28 24 27 imbi12d 
 |-  ( x = X -> ( ( y e. x -> E. u e. K ( y e. u /\ u C_ x ) ) <-> ( y e. X -> E. u e. K ( y e. u /\ u C_ X ) ) ) )
29 23 28 syl5ibrcom 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fClus f ) C_ ( J fClus f ) ) /\ x e. J ) -> ( x = X -> ( y e. x -> E. u e. K ( y e. u /\ u C_ x ) ) ) )
30 simplll 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fClus f ) C_ ( J fClus f ) ) /\ ( x e. J /\ ( x =/= X /\ y e. x ) ) ) -> J e. ( TopOn ` X ) )
31 simprl 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fClus f ) C_ ( J fClus f ) ) /\ ( x e. J /\ ( x =/= X /\ y e. x ) ) ) -> x e. J )
32 simprrr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fClus f ) C_ ( J fClus f ) ) /\ ( x e. J /\ ( x =/= X /\ y e. x ) ) ) -> y e. x )
33 supnfcls 
 |-  ( ( J e. ( TopOn ` X ) /\ x e. J /\ y e. x ) -> -. y e. ( J fClus { y e. ~P X | ( X \ x ) C_ y } ) )
34 30 31 32 33 syl3anc 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fClus f ) C_ ( J fClus f ) ) /\ ( x e. J /\ ( x =/= X /\ y e. x ) ) ) -> -. y e. ( J fClus { y e. ~P X | ( X \ x ) C_ y } ) )
35 toponss 
 |-  ( ( J e. ( TopOn ` X ) /\ x e. J ) -> x C_ X )
36 30 31 35 syl2anc 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fClus f ) C_ ( J fClus f ) ) /\ ( x e. J /\ ( x =/= X /\ y e. x ) ) ) -> x C_ X )
37 36 32 sseldd 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fClus f ) C_ ( J fClus f ) ) /\ ( x e. J /\ ( x =/= X /\ y e. x ) ) ) -> y e. X )
38 simpllr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fClus f ) C_ ( J fClus f ) ) /\ ( x e. J /\ ( x =/= X /\ y e. x ) ) ) -> K e. ( TopOn ` X ) )
39 toponmax 
 |-  ( J e. ( TopOn ` X ) -> X e. J )
40 30 39 syl 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fClus f ) C_ ( J fClus f ) ) /\ ( x e. J /\ ( x =/= X /\ y e. x ) ) ) -> X e. J )
41 difssd 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fClus f ) C_ ( J fClus f ) ) /\ ( x e. J /\ ( x =/= X /\ y e. x ) ) ) -> ( X \ x ) C_ X )
42 simprrl 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fClus f ) C_ ( J fClus f ) ) /\ ( x e. J /\ ( x =/= X /\ y e. x ) ) ) -> x =/= X )
43 pssdifn0 
 |-  ( ( x C_ X /\ x =/= X ) -> ( X \ x ) =/= (/) )
44 36 42 43 syl2anc 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fClus f ) C_ ( J fClus f ) ) /\ ( x e. J /\ ( x =/= X /\ y e. x ) ) ) -> ( X \ x ) =/= (/) )
45 supfil 
 |-  ( ( X e. J /\ ( X \ x ) C_ X /\ ( X \ x ) =/= (/) ) -> { y e. ~P X | ( X \ x ) C_ y } e. ( Fil ` X ) )
46 40 41 44 45 syl3anc 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fClus f ) C_ ( J fClus f ) ) /\ ( x e. J /\ ( x =/= X /\ y e. x ) ) ) -> { y e. ~P X | ( X \ x ) C_ y } e. ( Fil ` X ) )
47 fclsopn 
 |-  ( ( K e. ( TopOn ` X ) /\ { y e. ~P X | ( X \ x ) C_ y } e. ( Fil ` X ) ) -> ( y e. ( K fClus { y e. ~P X | ( X \ x ) C_ y } ) <-> ( y e. X /\ A. u e. K ( y e. u -> A. n e. { y e. ~P X | ( X \ x ) C_ y } ( u i^i n ) =/= (/) ) ) ) )
48 38 46 47 syl2anc 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fClus f ) C_ ( J fClus f ) ) /\ ( x e. J /\ ( x =/= X /\ y e. x ) ) ) -> ( y e. ( K fClus { y e. ~P X | ( X \ x ) C_ y } ) <-> ( y e. X /\ A. u e. K ( y e. u -> A. n e. { y e. ~P X | ( X \ x ) C_ y } ( u i^i n ) =/= (/) ) ) ) )
49 37 48 mpbirand 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fClus f ) C_ ( J fClus f ) ) /\ ( x e. J /\ ( x =/= X /\ y e. x ) ) ) -> ( y e. ( K fClus { y e. ~P X | ( X \ x ) C_ y } ) <-> A. u e. K ( y e. u -> A. n e. { y e. ~P X | ( X \ x ) C_ y } ( u i^i n ) =/= (/) ) ) )
50 oveq2 
 |-  ( f = { y e. ~P X | ( X \ x ) C_ y } -> ( K fClus f ) = ( K fClus { y e. ~P X | ( X \ x ) C_ y } ) )
51 oveq2 
 |-  ( f = { y e. ~P X | ( X \ x ) C_ y } -> ( J fClus f ) = ( J fClus { y e. ~P X | ( X \ x ) C_ y } ) )
52 50 51 sseq12d 
 |-  ( f = { y e. ~P X | ( X \ x ) C_ y } -> ( ( K fClus f ) C_ ( J fClus f ) <-> ( K fClus { y e. ~P X | ( X \ x ) C_ y } ) C_ ( J fClus { y e. ~P X | ( X \ x ) C_ y } ) ) )
53 simplr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fClus f ) C_ ( J fClus f ) ) /\ ( x e. J /\ ( x =/= X /\ y e. x ) ) ) -> A. f e. ( Fil ` X ) ( K fClus f ) C_ ( J fClus f ) )
54 52 53 46 rspcdva 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fClus f ) C_ ( J fClus f ) ) /\ ( x e. J /\ ( x =/= X /\ y e. x ) ) ) -> ( K fClus { y e. ~P X | ( X \ x ) C_ y } ) C_ ( J fClus { y e. ~P X | ( X \ x ) C_ y } ) )
55 54 sseld 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fClus f ) C_ ( J fClus f ) ) /\ ( x e. J /\ ( x =/= X /\ y e. x ) ) ) -> ( y e. ( K fClus { y e. ~P X | ( X \ x ) C_ y } ) -> y e. ( J fClus { y e. ~P X | ( X \ x ) C_ y } ) ) )
56 49 55 sylbird 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fClus f ) C_ ( J fClus f ) ) /\ ( x e. J /\ ( x =/= X /\ y e. x ) ) ) -> ( A. u e. K ( y e. u -> A. n e. { y e. ~P X | ( X \ x ) C_ y } ( u i^i n ) =/= (/) ) -> y e. ( J fClus { y e. ~P X | ( X \ x ) C_ y } ) ) )
57 34 56 mtod 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fClus f ) C_ ( J fClus f ) ) /\ ( x e. J /\ ( x =/= X /\ y e. x ) ) ) -> -. A. u e. K ( y e. u -> A. n e. { y e. ~P X | ( X \ x ) C_ y } ( u i^i n ) =/= (/) ) )
58 rexanali 
 |-  ( E. u e. K ( y e. u /\ -. A. n e. { y e. ~P X | ( X \ x ) C_ y } ( u i^i n ) =/= (/) ) <-> -. A. u e. K ( y e. u -> A. n e. { y e. ~P X | ( X \ x ) C_ y } ( u i^i n ) =/= (/) ) )
59 rexnal 
 |-  ( E. n e. { y e. ~P X | ( X \ x ) C_ y } -. ( u i^i n ) =/= (/) <-> -. A. n e. { y e. ~P X | ( X \ x ) C_ y } ( u i^i n ) =/= (/) )
60 sseq2 
 |-  ( y = n -> ( ( X \ x ) C_ y <-> ( X \ x ) C_ n ) )
61 60 elrab 
 |-  ( n e. { y e. ~P X | ( X \ x ) C_ y } <-> ( n e. ~P X /\ ( X \ x ) C_ n ) )
62 sslin 
 |-  ( ( X \ x ) C_ n -> ( u i^i ( X \ x ) ) C_ ( u i^i n ) )
63 61 62 simplbiim 
 |-  ( n e. { y e. ~P X | ( X \ x ) C_ y } -> ( u i^i ( X \ x ) ) C_ ( u i^i n ) )
64 ssn0 
 |-  ( ( ( u i^i ( X \ x ) ) C_ ( u i^i n ) /\ ( u i^i ( X \ x ) ) =/= (/) ) -> ( u i^i n ) =/= (/) )
65 64 ex 
 |-  ( ( u i^i ( X \ x ) ) C_ ( u i^i n ) -> ( ( u i^i ( X \ x ) ) =/= (/) -> ( u i^i n ) =/= (/) ) )
66 65 necon1bd 
 |-  ( ( u i^i ( X \ x ) ) C_ ( u i^i n ) -> ( -. ( u i^i n ) =/= (/) -> ( u i^i ( X \ x ) ) = (/) ) )
67 inssdif0 
 |-  ( ( u i^i X ) C_ x <-> ( u i^i ( X \ x ) ) = (/) )
68 66 67 syl6ibr 
 |-  ( ( u i^i ( X \ x ) ) C_ ( u i^i n ) -> ( -. ( u i^i n ) =/= (/) -> ( u i^i X ) C_ x ) )
69 toponss 
 |-  ( ( K e. ( TopOn ` X ) /\ u e. K ) -> u C_ X )
70 38 69 sylan 
 |-  ( ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fClus f ) C_ ( J fClus f ) ) /\ ( x e. J /\ ( x =/= X /\ y e. x ) ) ) /\ u e. K ) -> u C_ X )
71 df-ss 
 |-  ( u C_ X <-> ( u i^i X ) = u )
72 70 71 sylib 
 |-  ( ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fClus f ) C_ ( J fClus f ) ) /\ ( x e. J /\ ( x =/= X /\ y e. x ) ) ) /\ u e. K ) -> ( u i^i X ) = u )
73 72 sseq1d 
 |-  ( ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fClus f ) C_ ( J fClus f ) ) /\ ( x e. J /\ ( x =/= X /\ y e. x ) ) ) /\ u e. K ) -> ( ( u i^i X ) C_ x <-> u C_ x ) )
74 73 biimpd 
 |-  ( ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fClus f ) C_ ( J fClus f ) ) /\ ( x e. J /\ ( x =/= X /\ y e. x ) ) ) /\ u e. K ) -> ( ( u i^i X ) C_ x -> u C_ x ) )
75 68 74 syl9r 
 |-  ( ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fClus f ) C_ ( J fClus f ) ) /\ ( x e. J /\ ( x =/= X /\ y e. x ) ) ) /\ u e. K ) -> ( ( u i^i ( X \ x ) ) C_ ( u i^i n ) -> ( -. ( u i^i n ) =/= (/) -> u C_ x ) ) )
76 63 75 syl5 
 |-  ( ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fClus f ) C_ ( J fClus f ) ) /\ ( x e. J /\ ( x =/= X /\ y e. x ) ) ) /\ u e. K ) -> ( n e. { y e. ~P X | ( X \ x ) C_ y } -> ( -. ( u i^i n ) =/= (/) -> u C_ x ) ) )
77 76 rexlimdv 
 |-  ( ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fClus f ) C_ ( J fClus f ) ) /\ ( x e. J /\ ( x =/= X /\ y e. x ) ) ) /\ u e. K ) -> ( E. n e. { y e. ~P X | ( X \ x ) C_ y } -. ( u i^i n ) =/= (/) -> u C_ x ) )
78 59 77 syl5bir 
 |-  ( ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fClus f ) C_ ( J fClus f ) ) /\ ( x e. J /\ ( x =/= X /\ y e. x ) ) ) /\ u e. K ) -> ( -. A. n e. { y e. ~P X | ( X \ x ) C_ y } ( u i^i n ) =/= (/) -> u C_ x ) )
79 78 anim2d 
 |-  ( ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fClus f ) C_ ( J fClus f ) ) /\ ( x e. J /\ ( x =/= X /\ y e. x ) ) ) /\ u e. K ) -> ( ( y e. u /\ -. A. n e. { y e. ~P X | ( X \ x ) C_ y } ( u i^i n ) =/= (/) ) -> ( y e. u /\ u C_ x ) ) )
80 79 reximdva 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fClus f ) C_ ( J fClus f ) ) /\ ( x e. J /\ ( x =/= X /\ y e. x ) ) ) -> ( E. u e. K ( y e. u /\ -. A. n e. { y e. ~P X | ( X \ x ) C_ y } ( u i^i n ) =/= (/) ) -> E. u e. K ( y e. u /\ u C_ x ) ) )
81 58 80 syl5bir 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fClus f ) C_ ( J fClus f ) ) /\ ( x e. J /\ ( x =/= X /\ y e. x ) ) ) -> ( -. A. u e. K ( y e. u -> A. n e. { y e. ~P X | ( X \ x ) C_ y } ( u i^i n ) =/= (/) ) -> E. u e. K ( y e. u /\ u C_ x ) ) )
82 57 81 mpd 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fClus f ) C_ ( J fClus f ) ) /\ ( x e. J /\ ( x =/= X /\ y e. x ) ) ) -> E. u e. K ( y e. u /\ u C_ x ) )
83 82 anassrs 
 |-  ( ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fClus f ) C_ ( J fClus f ) ) /\ x e. J ) /\ ( x =/= X /\ y e. x ) ) -> E. u e. K ( y e. u /\ u C_ x ) )
84 83 exp32 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fClus f ) C_ ( J fClus f ) ) /\ x e. J ) -> ( x =/= X -> ( y e. x -> E. u e. K ( y e. u /\ u C_ x ) ) ) )
85 29 84 pm2.61dne 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fClus f ) C_ ( J fClus f ) ) /\ x e. J ) -> ( y e. x -> E. u e. K ( y e. u /\ u C_ x ) ) )
86 85 ralrimiv 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fClus f ) C_ ( J fClus f ) ) /\ x e. J ) -> A. y e. x E. u e. K ( y e. u /\ u C_ x ) )
87 topontop 
 |-  ( K e. ( TopOn ` X ) -> K e. Top )
88 eltop2 
 |-  ( K e. Top -> ( x e. K <-> A. y e. x E. u e. K ( y e. u /\ u C_ x ) ) )
89 14 87 88 3syl 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fClus f ) C_ ( J fClus f ) ) /\ x e. J ) -> ( x e. K <-> A. y e. x E. u e. K ( y e. u /\ u C_ x ) ) )
90 86 89 mpbird 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fClus f ) C_ ( J fClus f ) ) /\ x e. J ) -> x e. K )
91 90 ex 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fClus f ) C_ ( J fClus f ) ) -> ( x e. J -> x e. K ) )
92 91 ssrdv 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fClus f ) C_ ( J fClus f ) ) -> J C_ K )
93 13 92 impbida 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) -> ( J C_ K <-> A. f e. ( Fil ` X ) ( K fClus f ) C_ ( J fClus f ) ) )