Metamath Proof Explorer

Theorem fclsss1

Description: A finer topology has fewer cluster points. (Contributed by Jeff Hankins, 11-Nov-2009) (Revised by Stefan O'Rear, 8-Aug-2015)

Ref Expression
Assertion fclsss1 
|- ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ J C_ K ) -> ( K fClus F ) C_ ( J fClus F ) )

Proof

Step Hyp Ref Expression
1 simpl3 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ J C_ K ) /\ x e. ( K fClus F ) ) -> J C_ K )
2 ssralv 
 |-  ( J C_ K -> ( A. o e. K ( x e. o -> A. s e. F ( o i^i s ) =/= (/) ) -> A. o e. J ( x e. o -> A. s e. F ( o i^i s ) =/= (/) ) ) )
3 2 anim2d 
 |-  ( J C_ K -> ( ( x e. X /\ A. o e. K ( x e. o -> A. s e. F ( o i^i s ) =/= (/) ) ) -> ( x e. X /\ A. o e. J ( x e. o -> A. s e. F ( o i^i s ) =/= (/) ) ) ) )
4 1 3 syl 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ J C_ K ) /\ x e. ( K fClus F ) ) -> ( ( x e. X /\ A. o e. K ( x e. o -> A. s e. F ( o i^i s ) =/= (/) ) ) -> ( x e. X /\ A. o e. J ( x e. o -> A. s e. F ( o i^i s ) =/= (/) ) ) ) )
5 simpl2 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ J C_ K ) /\ x e. ( K fClus F ) ) -> F e. ( Fil ` X ) )
6 fclstopon 
 |-  ( x e. ( K fClus F ) -> ( K e. ( TopOn ` X ) <-> F e. ( Fil ` X ) ) )
7 6 adantl 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ J C_ K ) /\ x e. ( K fClus F ) ) -> ( K e. ( TopOn ` X ) <-> F e. ( Fil ` X ) ) )
8 5 7 mpbird 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ J C_ K ) /\ x e. ( K fClus F ) ) -> K e. ( TopOn ` X ) )
9 fclsopn 
 |-  ( ( K e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) -> ( x e. ( K fClus F ) <-> ( x e. X /\ A. o e. K ( x e. o -> A. s e. F ( o i^i s ) =/= (/) ) ) ) )
10 8 5 9 syl2anc 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ J C_ K ) /\ x e. ( K fClus F ) ) -> ( x e. ( K fClus F ) <-> ( x e. X /\ A. o e. K ( x e. o -> A. s e. F ( o i^i s ) =/= (/) ) ) ) )
11 simpl1 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ J C_ K ) /\ x e. ( K fClus F ) ) -> J e. ( TopOn ` X ) )
12 fclsopn 
 |-  ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) -> ( x e. ( J fClus F ) <-> ( x e. X /\ A. o e. J ( x e. o -> A. s e. F ( o i^i s ) =/= (/) ) ) ) )
13 11 5 12 syl2anc 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ J C_ K ) /\ x e. ( K fClus F ) ) -> ( x e. ( J fClus F ) <-> ( x e. X /\ A. o e. J ( x e. o -> A. s e. F ( o i^i s ) =/= (/) ) ) ) )
14 4 10 13 3imtr4d 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ J C_ K ) /\ x e. ( K fClus F ) ) -> ( x e. ( K fClus F ) -> x e. ( J fClus F ) ) )
15 14 ex 
 |-  ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ J C_ K ) -> ( x e. ( K fClus F ) -> ( x e. ( K fClus F ) -> x e. ( J fClus F ) ) ) )
16 15 pm2.43d 
 |-  ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ J C_ K ) -> ( x e. ( K fClus F ) -> x e. ( J fClus F ) ) )
17 16 ssrdv 
 |-  ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ J C_ K ) -> ( K fClus F ) C_ ( J fClus F ) )