Metamath Proof Explorer

Theorem limcresi

Description: Any limit of F is also a limit of the restriction of F . (Contributed by Mario Carneiro, 28-Dec-2016)

Ref Expression
Assertion limcresi 
|- ( F limCC B ) C_ ( ( F |` C ) limCC B )

Proof

Step Hyp Ref Expression
1 limcrcl 
 |-  ( x e. ( F limCC B ) -> ( F : dom F --> CC /\ dom F C_ CC /\ B e. CC ) )
2 1 simp1d 
 |-  ( x e. ( F limCC B ) -> F : dom F --> CC )
3 1 simp2d 
 |-  ( x e. ( F limCC B ) -> dom F C_ CC )
4 1 simp3d 
 |-  ( x e. ( F limCC B ) -> B e. CC )
5 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
6 2 3 4 5 ellimc2 
 |-  ( x e. ( F limCC B ) -> ( x e. ( F limCC B ) <-> ( x e. CC /\ A. u e. ( TopOpen ` CCfld ) ( x e. u -> E. v e. ( TopOpen ` CCfld ) ( B e. v /\ ( F " ( v i^i ( dom F \ { B } ) ) ) C_ u ) ) ) ) )
7 6 ibi 
 |-  ( x e. ( F limCC B ) -> ( x e. CC /\ A. u e. ( TopOpen ` CCfld ) ( x e. u -> E. v e. ( TopOpen ` CCfld ) ( B e. v /\ ( F " ( v i^i ( dom F \ { B } ) ) ) C_ u ) ) ) )
8 inss2 
 |-  ( v i^i ( ( dom F i^i C ) \ { B } ) ) C_ ( ( dom F i^i C ) \ { B } )
9 difss 
 |-  ( ( dom F i^i C ) \ { B } ) C_ ( dom F i^i C )
10 inss2 
 |-  ( dom F i^i C ) C_ C
11 9 10 sstri 
 |-  ( ( dom F i^i C ) \ { B } ) C_ C
12 8 11 sstri 
 |-  ( v i^i ( ( dom F i^i C ) \ { B } ) ) C_ C
13 resima2 
 |-  ( ( v i^i ( ( dom F i^i C ) \ { B } ) ) C_ C -> ( ( F |` C ) " ( v i^i ( ( dom F i^i C ) \ { B } ) ) ) = ( F " ( v i^i ( ( dom F i^i C ) \ { B } ) ) ) )
14 12 13 ax-mp 
 |-  ( ( F |` C ) " ( v i^i ( ( dom F i^i C ) \ { B } ) ) ) = ( F " ( v i^i ( ( dom F i^i C ) \ { B } ) ) )
15 inss1 
 |-  ( dom F i^i C ) C_ dom F
16 ssdif 
 |-  ( ( dom F i^i C ) C_ dom F -> ( ( dom F i^i C ) \ { B } ) C_ ( dom F \ { B } ) )
17 15 16 ax-mp 
 |-  ( ( dom F i^i C ) \ { B } ) C_ ( dom F \ { B } )
18 sslin 
 |-  ( ( ( dom F i^i C ) \ { B } ) C_ ( dom F \ { B } ) -> ( v i^i ( ( dom F i^i C ) \ { B } ) ) C_ ( v i^i ( dom F \ { B } ) ) )
19 imass2 
 |-  ( ( v i^i ( ( dom F i^i C ) \ { B } ) ) C_ ( v i^i ( dom F \ { B } ) ) -> ( F " ( v i^i ( ( dom F i^i C ) \ { B } ) ) ) C_ ( F " ( v i^i ( dom F \ { B } ) ) ) )
20 17 18 19 mp2b 
 |-  ( F " ( v i^i ( ( dom F i^i C ) \ { B } ) ) ) C_ ( F " ( v i^i ( dom F \ { B } ) ) )
21 14 20 eqsstri 
 |-  ( ( F |` C ) " ( v i^i ( ( dom F i^i C ) \ { B } ) ) ) C_ ( F " ( v i^i ( dom F \ { B } ) ) )
22 sstr 
 |-  ( ( ( ( F |` C ) " ( v i^i ( ( dom F i^i C ) \ { B } ) ) ) C_ ( F " ( v i^i ( dom F \ { B } ) ) ) /\ ( F " ( v i^i ( dom F \ { B } ) ) ) C_ u ) -> ( ( F |` C ) " ( v i^i ( ( dom F i^i C ) \ { B } ) ) ) C_ u )
23 21 22 mpan 
 |-  ( ( F " ( v i^i ( dom F \ { B } ) ) ) C_ u -> ( ( F |` C ) " ( v i^i ( ( dom F i^i C ) \ { B } ) ) ) C_ u )
24 23 anim2i 
 |-  ( ( B e. v /\ ( F " ( v i^i ( dom F \ { B } ) ) ) C_ u ) -> ( B e. v /\ ( ( F |` C ) " ( v i^i ( ( dom F i^i C ) \ { B } ) ) ) C_ u ) )
25 24 reximi 
 |-  ( E. v e. ( TopOpen ` CCfld ) ( B e. v /\ ( F " ( v i^i ( dom F \ { B } ) ) ) C_ u ) -> E. v e. ( TopOpen ` CCfld ) ( B e. v /\ ( ( F |` C ) " ( v i^i ( ( dom F i^i C ) \ { B } ) ) ) C_ u ) )
26 25 imim2i 
 |-  ( ( x e. u -> E. v e. ( TopOpen ` CCfld ) ( B e. v /\ ( F " ( v i^i ( dom F \ { B } ) ) ) C_ u ) ) -> ( x e. u -> E. v e. ( TopOpen ` CCfld ) ( B e. v /\ ( ( F |` C ) " ( v i^i ( ( dom F i^i C ) \ { B } ) ) ) C_ u ) ) )
27 26 ralimi 
 |-  ( A. u e. ( TopOpen ` CCfld ) ( x e. u -> E. v e. ( TopOpen ` CCfld ) ( B e. v /\ ( F " ( v i^i ( dom F \ { B } ) ) ) C_ u ) ) -> A. u e. ( TopOpen ` CCfld ) ( x e. u -> E. v e. ( TopOpen ` CCfld ) ( B e. v /\ ( ( F |` C ) " ( v i^i ( ( dom F i^i C ) \ { B } ) ) ) C_ u ) ) )
28 27 anim2i 
 |-  ( ( x e. CC /\ A. u e. ( TopOpen ` CCfld ) ( x e. u -> E. v e. ( TopOpen ` CCfld ) ( B e. v /\ ( F " ( v i^i ( dom F \ { B } ) ) ) C_ u ) ) ) -> ( x e. CC /\ A. u e. ( TopOpen ` CCfld ) ( x e. u -> E. v e. ( TopOpen ` CCfld ) ( B e. v /\ ( ( F |` C ) " ( v i^i ( ( dom F i^i C ) \ { B } ) ) ) C_ u ) ) ) )
29 7 28 syl 
 |-  ( x e. ( F limCC B ) -> ( x e. CC /\ A. u e. ( TopOpen ` CCfld ) ( x e. u -> E. v e. ( TopOpen ` CCfld ) ( B e. v /\ ( ( F |` C ) " ( v i^i ( ( dom F i^i C ) \ { B } ) ) ) C_ u ) ) ) )
30 fresin 
 |-  ( F : dom F --> CC -> ( F |` C ) : ( dom F i^i C ) --> CC )
31 2 30 syl 
 |-  ( x e. ( F limCC B ) -> ( F |` C ) : ( dom F i^i C ) --> CC )
32 15 3 sstrid 
 |-  ( x e. ( F limCC B ) -> ( dom F i^i C ) C_ CC )
33 31 32 4 5 ellimc2 
 |-  ( x e. ( F limCC B ) -> ( x e. ( ( F |` C ) limCC B ) <-> ( x e. CC /\ A. u e. ( TopOpen ` CCfld ) ( x e. u -> E. v e. ( TopOpen ` CCfld ) ( B e. v /\ ( ( F |` C ) " ( v i^i ( ( dom F i^i C ) \ { B } ) ) ) C_ u ) ) ) ) )
34 29 33 mpbird 
 |-  ( x e. ( F limCC B ) -> x e. ( ( F |` C ) limCC B ) )
35 34 ssriv 
 |-  ( F limCC B ) C_ ( ( F |` C ) limCC B )