MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fclscf Structured version   Visualization version   Unicode version
Theorem fclscf 21829
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.)
Assertion
Ref Expression
fclscf |- ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` X ) ) -> ( J C_ K <-> A. f e. ( Fil ` X ) ( K fClus f ) C_ ( J fClus f ) ) )
Distinct variable groups:   f, J   f, K   f, X
Proof of Theorem fclscf
Dummy variables n u x y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpll 790 . . . . . . 7 |- ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` X ) ) /\ ( J C_ K /\ x e. ( K fClus f ) ) ) -> J e. (TopOn ` X ) )
2 simplr 792 . . . . . . . 8 |- ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` X ) ) /\ ( J C_ K /\ x e. ( K fClus f ) ) ) -> K e. (TopOn ` X ) )
3 fclstopon 21816 . . . . . . . . 9 |- ( x e. ( K fClus f ) -> ( K e. (TopOn ` X ) <-> f e. ( Fil ` X ) ) )
43ad2antll 765 . . . . . . . 8 |- ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` X ) ) /\ ( J C_ K /\ x e. ( K fClus f ) ) ) -> ( K e. (TopOn ` X ) <-> f e. ( Fil ` X ) ) )
52, 4mpbid 222 . . . . . . 7 |- ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` X ) ) /\ ( J C_ K /\ x e. ( K fClus f ) ) ) -> f e. ( Fil ` X ) )
6 simprl 794 . . . . . . 7 |- ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` X ) ) /\ ( J C_ K /\ x e. ( K fClus f ) ) ) -> J C_ K )
7 fclsss1 21826 . . . . . . 7 |- ( ( J e. (TopOn ` X ) /\ f e. ( Fil ` X ) /\ J C_ K ) -> ( K fClus f ) C_ ( J fClus f ) )
81, 5, 6, 7syl3anc 1326 . . . . . 6 |- ( ( ( 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 796 . . . . . 6 |- ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` X ) ) /\ ( J C_ K /\ x e. ( K fClus f ) ) ) -> x e. ( K fClus f ) )
108, 9sseldd 3604 . . . . 5 |- ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` X ) ) /\ ( J C_ K /\ x e. ( K fClus f ) ) ) -> x e. ( J fClus f ) )
1110expr 643 . . . 4 |- ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` X ) ) /\ J C_ K ) -> ( x e. ( K fClus f ) -> x e. ( J fClus f ) ) )
1211ssrdv 3609 . . 3 |- ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` X ) ) /\ J C_ K ) -> ( K fClus f ) C_ ( J fClus f ) )
1312ralrimivw 2967 . 2 |- ( ( ( 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 799 . . . . . . . . 9 |- ( ( ( ( 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 20730 . . . . . . . . 9 |- ( K e. (TopOn ` X ) -> X e. K )
16 ssid 3624 . . . . . . . . . . 11 |- X C_ X
17 eleq2 2690 . . . . . . . . . . . . 13 |- ( u = X -> ( y e. u <-> y e. X ) )
18 sseq1 3626 . . . . . . . . . . . . 13 |- ( u = X -> ( u C_ X <-> X C_ X ) )
1917, 18anbi12d 747 . . . . . . . . . . . 12 |- ( u = X -> ( ( y e. u /\ u C_ X ) <-> ( y e. X /\ X C_ X ) ) )
2019rspcev 3309 . . . . . . . . . . 11 |- ( ( X e. K /\ ( y e. X /\ X C_ X ) ) -> E. u e. K ( y e. u /\ u C_ X ) )
2116, 20mpanr2 720 . . . . . . . . . 10 |- ( ( X e. K /\ y e. X ) -> E. u e. K ( y e. u /\ u C_ X ) )
2221ex 450 . . . . . . . . 9 |- ( X e. K -> ( y e. X -> E. u e. K ( y e. u /\ u C_ X ) ) )
2314, 15, 223syl 18 . . . . . . . 8 |- ( ( ( ( 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 2690 . . . . . . . . 9 |- ( x = X -> ( y e. x <-> y e. X ) )
25 sseq2 3627 . . . . . . . . . . 11 |- ( x = X -> ( u C_ x <-> u C_ X ) )
2625anbi2d 740 . . . . . . . . . 10 |- ( x = X -> ( ( y e. u /\ u C_ x ) <-> ( y e. u /\ u C_ X ) ) )
2726rexbidv 3052 . . . . . . . . 9 |- ( x = X -> ( E. u e. K ( y e. u /\ u C_ x ) <-> E. u e. K ( y e. u /\ u C_ X ) ) )
2824, 27imbi12d 334 . . . . . . . 8 |- ( 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 ) ) ) )
2923, 28syl5ibrcom 237 . . . . . . 7 |- ( ( ( ( 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 798 . . . . . . . . . . . 12 |- ( ( ( ( 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 794 . . . . . . . . . . . 12 |- ( ( ( ( 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 805 . . . . . . . . . . . 12 |- ( ( ( ( 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 21824 . . . . . . . . . . . 12 |- ( ( J e. (TopOn ` X ) /\ x e. J /\ y e. x ) -> -. y e. ( J fClus { y e. ~P X | ( X \ x ) C_ y } ) )
3430, 31, 32, 33syl3anc 1326 . . . . . . . . . . 11 |- ( ( ( ( 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 simpllr 799 . . . . . . . . . . . . . 14 |- ( ( ( ( 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 ) )
36 toponmax 20730 . . . . . . . . . . . . . . . 16 |- ( J e. (TopOn ` X ) -> X e. J )
3730, 36syl 17 . . . . . . . . . . . . . . 15 |- ( ( ( ( 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 )
38 difssd 3738 . . . . . . . . . . . . . . 15 |- ( ( ( ( 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 )
39 toponss 20731 . . . . . . . . . . . . . . . . 17 |- ( ( J e. (TopOn ` X ) /\ x e. J ) -> x C_ X )
4030, 31, 39syl2anc 693 . . . . . . . . . . . . . . . 16 |- ( ( ( ( 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 )
41 simprrl 804 . . . . . . . . . . . . . . . 16 |- ( ( ( ( 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 )
42 pssdifn0 3944 . . . . . . . . . . . . . . . 16 |- ( ( x C_ X /\ x =/= X ) -> ( X \ x ) =/= (/) )
4340, 41, 42syl2anc 693 . . . . . . . . . . . . . . 15 |- ( ( ( ( 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 ) =/= (/) )
44 supfil 21699 . . . . . . . . . . . . . . 15 |- ( ( X e. J /\ ( X \ x ) C_ X /\ ( X \ x ) =/= (/) ) -> { y e. ~P X | ( X \ x ) C_ y } e. ( Fil ` X ) )
4537, 38, 43, 44syl3anc 1326 . . . . . . . . . . . . . 14 |- ( ( ( ( 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 ) )
46 fclsopn 21818 . . . . . . . . . . . . . 14 |- ( ( 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 ) =/= (/) ) ) ) )
4735, 45, 46syl2anc 693 . . . . . . . . . . . . 13 |- ( ( ( ( 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 ) =/= (/) ) ) ) )
4840, 32sseldd 3604 . . . . . . . . . . . . . 14 |- ( ( ( ( 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 )
4948biantrurd 529 . . . . . . . . . . . . 13 |- ( ( ( ( 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. X /\ A. u e. K ( y e. u -> A. n e. { y e. ~P X | ( X \ x ) C_ y } ( u i^i n ) =/= (/) ) ) ) )
5047, 49bitr4d 271 . . . . . . . . . . . 12 |- ( ( ( ( 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 ) =/= (/) ) ) )
51 simplr 792 . . . . . . . . . . . . . 14 |- ( ( ( ( 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 ) )
52 oveq2 6658 . . . . . . . . . . . . . . . 16 |- ( f = { y e. ~P X | ( X \ x ) C_ y } -> ( K fClus f ) = ( K fClus { y e. ~P X | ( X \ x ) C_ y } ) )
53 oveq2 6658 . . . . . . . . . . . . . . . 16 |- ( f = { y e. ~P X | ( X \ x ) C_ y } -> ( J fClus f ) = ( J fClus { y e. ~P X | ( X \ x ) C_ y } ) )
5452, 53sseq12d 3634 . . . . . . . . . . . . . . 15 |- ( 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 } ) ) )
5554rspcv 3305 . . . . . . . . . . . . . 14 |- ( { y e. ~P X | ( X \ x ) C_ y } e. ( Fil ` X ) -> ( A. f e. ( Fil ` X ) ( 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 } ) ) )
5645, 51, 55sylc 65 . . . . . . . . . . . . 13 |- ( ( ( ( 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 } ) )
5756sseld 3602 . . . . . . . . . . . 12 |- ( ( ( ( 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 } ) ) )
5850, 57sylbird 250 . . . . . . . . . . 11 |- ( ( ( ( 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 } ) ) )
5934, 58mtod 189 . . . . . . . . . 10 |- ( ( ( ( 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 ) =/= (/) ) )
60 rexanali 2998 . . . . . . . . . . 11 |- ( 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 ) =/= (/) ) )
61 rexnal 2995 . . . . . . . . . . . . . 14 |- ( 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 ) =/= (/) )
62 sseq2 3627 . . . . . . . . . . . . . . . . . . 19 |- ( y = n -> ( ( X \ x ) C_ y <-> ( X \ x ) C_ n ) )
6362elrab 3363 . . . . . . . . . . . . . . . . . 18 |- ( n e. { y e. ~P X | ( X \ x ) C_ y } <-> ( n e. ~P X /\ ( X \ x ) C_ n ) )
6463simprbi 480 . . . . . . . . . . . . . . . . 17 |- ( n e. { y e. ~P X | ( X \ x ) C_ y } -> ( X \ x ) C_ n )
65 sslin 3839 . . . . . . . . . . . . . . . . 17 |- ( ( X \ x ) C_ n -> ( u i^i ( X \ x ) ) C_ ( u i^i n ) )
6664, 65syl 17 . . . . . . . . . . . . . . . 16 |- ( n e. { y e. ~P X | ( X \ x ) C_ y } -> ( u i^i ( X \ x ) ) C_ ( u i^i n ) )
67 ssn0 3976 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( u i^i ( X \ x ) ) C_ ( u i^i n ) /\ ( u i^i ( X \ x ) ) =/= (/) ) -> ( u i^i n ) =/= (/) )
6867ex 450 . . . . . . . . . . . . . . . . . . 19 |- ( ( u i^i ( X \ x ) ) C_ ( u i^i n ) -> ( ( u i^i ( X \ x ) ) =/= (/) -> ( u i^i n ) =/= (/) ) )
6968necon1bd 2812 . . . . . . . . . . . . . . . . . 18 |- ( ( u i^i ( X \ x ) ) C_ ( u i^i n ) -> ( -. ( u i^i n ) =/= (/) -> ( u i^i ( X \ x ) ) = (/) ) )
70 inssdif0 3947 . . . . . . . . . . . . . . . . . 18 |- ( ( u i^i X ) C_ x <-> ( u i^i ( X \ x ) ) = (/) )
7169, 70syl6ibr 242 . . . . . . . . . . . . . . . . 17 |- ( ( u i^i ( X \ x ) ) C_ ( u i^i n ) -> ( -. ( u i^i n ) =/= (/) -> ( u i^i X ) C_ x ) )
72 toponss 20731 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( K e. (TopOn ` X ) /\ u e. K ) -> u C_ X )
7335, 72sylan 488 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( 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 )
74 df-ss 3588 . . . . . . . . . . . . . . . . . . . 20 |- ( u C_ X <-> ( u i^i X ) = u )
7573, 74sylib 208 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( 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 )
7675sseq1d 3632 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( 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 ) )
7776biimpd 219 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( 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 ) )
7871, 77syl9r 78 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( 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 ) ) )
7966, 78syl5 34 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( 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 ) ) )
8079rexlimdv 3030 . . . . . . . . . . . . . 14 |- ( ( ( ( ( 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 ) )
8161, 80syl5bir 233 . . . . . . . . . . . . 13 |- ( ( ( ( ( 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 ) )
8281anim2d 589 . . . . . . . . . . . 12 |- ( ( ( ( ( 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 ) ) )
8382reximdva 3017 . . . . . . . . . . 11 |- ( ( ( ( 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 ) ) )
8460, 83syl5bir 233 . . . . . . . . . 10 |- ( ( ( ( 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 ) ) )
8559, 84mpd 15 . . . . . . . . 9 |- ( ( ( ( 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 ) )
8685anassrs 680 . . . . . . . 8 |- ( ( ( ( ( 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 ) )
8786exp32 631 . . . . . . 7 |- ( ( ( ( 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 ) ) ) )
8829, 87pm2.61dne 2880 . . . . . 6 |- ( ( ( ( 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 ) ) )
8988ralrimiv 2965 . . . . 5 |- ( ( ( ( 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 ) )
90 topontop 20718 . . . . . 6 |- ( K e. (TopOn ` X ) -> K e. Top )
91 eltop2 20779 . . . . . 6 |- ( K e. Top -> ( x e. K <-> A. y e. x E. u e. K ( y e. u /\ u C_ x ) ) )
9214, 90, 913syl 18 . . . . 5 |- ( ( ( ( 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 ) ) )
9389, 92mpbird 247 . . . 4 |- ( ( ( ( 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 )
9493ex 450 . . 3 |- ( ( ( 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 ) )
9594ssrdv 3609 . 2 |- ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fClus f ) C_ ( J fClus f ) ) -> J C_ K )
9613, 95impbida 877 1 |- ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` X ) ) -> ( J C_ K <-> A. f e. ( Fil ` X ) ( K fClus f ) C_ ( J fClus f ) ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   /\ wa 384   = wceq 1483   e. wcel 1990   =/= wne 2794   A.wral 2912   E.wrex 2913   {crab 2916   \ cdif 3571   i^i cin 3573   C_ wss 3574   (/)c0 3915   ~Pcpw 4158   ` cfv 5888  (class class class)co 6650   Topctop 20698  TopOnctopon 20715   Filcfil 21649   fClus cfcls 21740
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-iin 4523  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-topgen 16104  df-fbas 19743  df-top 20699  df-topon 20716  df-cld 20823  df-ntr 20824  df-cls 20825  df-fil 21650  df-fcls 21745
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator