Metamath Proof Explorer

Theorem fclsss2

Description: A finer filter has fewer cluster points. (Contributed by Jeff Hankins, 11-Nov-2009) (Revised by Mario Carneiro, 26-Aug-2015)

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

Proof

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