Metamath Proof Explorer

Theorem tsmscls

Description: One half of tgptsmscls , true in any commutative monoid topological space. (Contributed by Mario Carneiro, 21-Sep-2015)

Ref Expression
Hypotheses tsmscls.b 
|- B = ( Base ` G )
tsmscls.j 
|- J = ( TopOpen ` G )
tsmscls.1 
|- ( ph -> G e. CMnd )
tsmscls.2 
|- ( ph -> G e. TopSp )
tsmscls.a 
|- ( ph -> A e. V )
tsmscls.f 
|- ( ph -> F : A --> B )
tsmscls.x 
|- ( ph -> X e. ( G tsums F ) )
Assertion tsmscls 
|- ( ph -> ( ( cls ` J ) ` { X } ) C_ ( G tsums F ) )

Proof

Step Hyp Ref Expression
1 tsmscls.b 
 |-  B = ( Base ` G )
2 tsmscls.j 
 |-  J = ( TopOpen ` G )
3 tsmscls.1 
 |-  ( ph -> G e. CMnd )
4 tsmscls.2 
 |-  ( ph -> G e. TopSp )
5 tsmscls.a 
 |-  ( ph -> A e. V )
6 tsmscls.f 
 |-  ( ph -> F : A --> B )
7 tsmscls.x 
 |-  ( ph -> X e. ( G tsums F ) )
8 eqid 
 |-  ( ~P A i^i Fin ) = ( ~P A i^i Fin )
9 eqid 
 |-  ran ( x e. ( ~P A i^i Fin ) |-> { y e. ( ~P A i^i Fin ) | x C_ y } ) = ran ( x e. ( ~P A i^i Fin ) |-> { y e. ( ~P A i^i Fin ) | x C_ y } )
10 1 2 8 9 4 5 6 tsmsval 
 |-  ( ph -> ( G tsums F ) = ( ( J fLimf ( ( ~P A i^i Fin ) filGen ran ( x e. ( ~P A i^i Fin ) |-> { y e. ( ~P A i^i Fin ) | x C_ y } ) ) ) ` ( y e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` y ) ) ) ) )
11 1 2 istps 
 |-  ( G e. TopSp <-> J e. ( TopOn ` B ) )
12 4 11 sylib 
 |-  ( ph -> J e. ( TopOn ` B ) )
13 eqid 
 |-  ( x e. ( ~P A i^i Fin ) |-> { y e. ( ~P A i^i Fin ) | x C_ y } ) = ( x e. ( ~P A i^i Fin ) |-> { y e. ( ~P A i^i Fin ) | x C_ y } )
14 8 13 9 5 tsmsfbas 
 |-  ( ph -> ran ( x e. ( ~P A i^i Fin ) |-> { y e. ( ~P A i^i Fin ) | x C_ y } ) e. ( fBas ` ( ~P A i^i Fin ) ) )
15 fgcl 
 |-  ( ran ( x e. ( ~P A i^i Fin ) |-> { y e. ( ~P A i^i Fin ) | x C_ y } ) e. ( fBas ` ( ~P A i^i Fin ) ) -> ( ( ~P A i^i Fin ) filGen ran ( x e. ( ~P A i^i Fin ) |-> { y e. ( ~P A i^i Fin ) | x C_ y } ) ) e. ( Fil ` ( ~P A i^i Fin ) ) )
16 14 15 syl 
 |-  ( ph -> ( ( ~P A i^i Fin ) filGen ran ( x e. ( ~P A i^i Fin ) |-> { y e. ( ~P A i^i Fin ) | x C_ y } ) ) e. ( Fil ` ( ~P A i^i Fin ) ) )
17 1 8 3 5 6 tsmslem1 
 |-  ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> ( G gsum ( F |` y ) ) e. B )
18 17 fmpttd 
 |-  ( ph -> ( y e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` y ) ) ) : ( ~P A i^i Fin ) --> B )
19 flfval 
 |-  ( ( J e. ( TopOn ` B ) /\ ( ( ~P A i^i Fin ) filGen ran ( x e. ( ~P A i^i Fin ) |-> { y e. ( ~P A i^i Fin ) | x C_ y } ) ) e. ( Fil ` ( ~P A i^i Fin ) ) /\ ( y e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` y ) ) ) : ( ~P A i^i Fin ) --> B ) -> ( ( J fLimf ( ( ~P A i^i Fin ) filGen ran ( x e. ( ~P A i^i Fin ) |-> { y e. ( ~P A i^i Fin ) | x C_ y } ) ) ) ` ( y e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` y ) ) ) ) = ( J fLim ( ( B FilMap ( y e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` y ) ) ) ) ` ( ( ~P A i^i Fin ) filGen ran ( x e. ( ~P A i^i Fin ) |-> { y e. ( ~P A i^i Fin ) | x C_ y } ) ) ) ) )
20 12 16 18 19 syl3anc 
 |-  ( ph -> ( ( J fLimf ( ( ~P A i^i Fin ) filGen ran ( x e. ( ~P A i^i Fin ) |-> { y e. ( ~P A i^i Fin ) | x C_ y } ) ) ) ` ( y e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` y ) ) ) ) = ( J fLim ( ( B FilMap ( y e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` y ) ) ) ) ` ( ( ~P A i^i Fin ) filGen ran ( x e. ( ~P A i^i Fin ) |-> { y e. ( ~P A i^i Fin ) | x C_ y } ) ) ) ) )
21 10 20 eqtrd 
 |-  ( ph -> ( G tsums F ) = ( J fLim ( ( B FilMap ( y e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` y ) ) ) ) ` ( ( ~P A i^i Fin ) filGen ran ( x e. ( ~P A i^i Fin ) |-> { y e. ( ~P A i^i Fin ) | x C_ y } ) ) ) ) )
22 7 21 eleqtrd 
 |-  ( ph -> X e. ( J fLim ( ( B FilMap ( y e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` y ) ) ) ) ` ( ( ~P A i^i Fin ) filGen ran ( x e. ( ~P A i^i Fin ) |-> { y e. ( ~P A i^i Fin ) | x C_ y } ) ) ) ) )
23 flimsncls 
 |-  ( X e. ( J fLim ( ( B FilMap ( y e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` y ) ) ) ) ` ( ( ~P A i^i Fin ) filGen ran ( x e. ( ~P A i^i Fin ) |-> { y e. ( ~P A i^i Fin ) | x C_ y } ) ) ) ) -> ( ( cls ` J ) ` { X } ) C_ ( J fLim ( ( B FilMap ( y e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` y ) ) ) ) ` ( ( ~P A i^i Fin ) filGen ran ( x e. ( ~P A i^i Fin ) |-> { y e. ( ~P A i^i Fin ) | x C_ y } ) ) ) ) )
24 22 23 syl 
 |-  ( ph -> ( ( cls ` J ) ` { X } ) C_ ( J fLim ( ( B FilMap ( y e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` y ) ) ) ) ` ( ( ~P A i^i Fin ) filGen ran ( x e. ( ~P A i^i Fin ) |-> { y e. ( ~P A i^i Fin ) | x C_ y } ) ) ) ) )
25 24 21 sseqtrrd 
 |-  ( ph -> ( ( cls ` J ) ` { X } ) C_ ( G tsums F ) )