Metamath Proof Explorer

Theorem limccog

Description: Limit of the composition of two functions. If the limit of F at A is B and the limit of G at B is C , then the limit of G o. F at A is C . With respect to limcco and limccnp , here we drop continuity assumptions. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses limccog.1 
|- ( ph -> ran F C_ ( dom G \ { B } ) )
limccog.2 
|- ( ph -> B e. ( F limCC A ) )
limccog.3 
|- ( ph -> C e. ( G limCC B ) )
Assertion limccog 
|- ( ph -> C e. ( ( G o. F ) limCC A ) )

Proof

Step Hyp Ref Expression
1 limccog.1 
 |-  ( ph -> ran F C_ ( dom G \ { B } ) )
2 limccog.2 
 |-  ( ph -> B e. ( F limCC A ) )
3 limccog.3 
 |-  ( ph -> C e. ( G limCC B ) )
4 limccl 
 |-  ( G limCC B ) C_ CC
5 4 3 sselid 
 |-  ( ph -> C e. CC )
6 limcrcl 
 |-  ( C e. ( G limCC B ) -> ( G : dom G --> CC /\ dom G C_ CC /\ B e. CC ) )
7 3 6 syl 
 |-  ( ph -> ( G : dom G --> CC /\ dom G C_ CC /\ B e. CC ) )
8 7 simp1d 
 |-  ( ph -> G : dom G --> CC )
9 7 simp2d 
 |-  ( ph -> dom G C_ CC )
10 7 simp3d 
 |-  ( ph -> B e. CC )
11 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
12 8 9 10 11 ellimc2 
 |-  ( ph -> ( C e. ( G limCC B ) <-> ( C e. CC /\ A. u e. ( TopOpen ` CCfld ) ( C e. u -> E. v e. ( TopOpen ` CCfld ) ( B e. v /\ ( G " ( v i^i ( dom G \ { B } ) ) ) C_ u ) ) ) ) )
13 3 12 mpbid 
 |-  ( ph -> ( C e. CC /\ A. u e. ( TopOpen ` CCfld ) ( C e. u -> E. v e. ( TopOpen ` CCfld ) ( B e. v /\ ( G " ( v i^i ( dom G \ { B } ) ) ) C_ u ) ) ) )
14 13 simprd 
 |-  ( ph -> A. u e. ( TopOpen ` CCfld ) ( C e. u -> E. v e. ( TopOpen ` CCfld ) ( B e. v /\ ( G " ( v i^i ( dom G \ { B } ) ) ) C_ u ) ) )
15 14 r19.21bi 
 |-  ( ( ph /\ u e. ( TopOpen ` CCfld ) ) -> ( C e. u -> E. v e. ( TopOpen ` CCfld ) ( B e. v /\ ( G " ( v i^i ( dom G \ { B } ) ) ) C_ u ) ) )
16 15 imp 
 |-  ( ( ( ph /\ u e. ( TopOpen ` CCfld ) ) /\ C e. u ) -> E. v e. ( TopOpen ` CCfld ) ( B e. v /\ ( G " ( v i^i ( dom G \ { B } ) ) ) C_ u ) )
17 simp1ll 
 |-  ( ( ( ( ph /\ u e. ( TopOpen ` CCfld ) ) /\ C e. u ) /\ v e. ( TopOpen ` CCfld ) /\ ( B e. v /\ ( G " ( v i^i ( dom G \ { B } ) ) ) C_ u ) ) -> ph )
18 simp2 
 |-  ( ( ( ( ph /\ u e. ( TopOpen ` CCfld ) ) /\ C e. u ) /\ v e. ( TopOpen ` CCfld ) /\ ( B e. v /\ ( G " ( v i^i ( dom G \ { B } ) ) ) C_ u ) ) -> v e. ( TopOpen ` CCfld ) )
19 simp3l 
 |-  ( ( ( ( ph /\ u e. ( TopOpen ` CCfld ) ) /\ C e. u ) /\ v e. ( TopOpen ` CCfld ) /\ ( B e. v /\ ( G " ( v i^i ( dom G \ { B } ) ) ) C_ u ) ) -> B e. v )
20 limcrcl 
 |-  ( B e. ( F limCC A ) -> ( F : dom F --> CC /\ dom F C_ CC /\ A e. CC ) )
21 2 20 syl 
 |-  ( ph -> ( F : dom F --> CC /\ dom F C_ CC /\ A e. CC ) )
22 21 simp1d 
 |-  ( ph -> F : dom F --> CC )
23 21 simp2d 
 |-  ( ph -> dom F C_ CC )
24 21 simp3d 
 |-  ( ph -> A e. CC )
25 22 23 24 11 ellimc2 
 |-  ( ph -> ( B e. ( F limCC A ) <-> ( B e. CC /\ A. v e. ( TopOpen ` CCfld ) ( B e. v -> E. w e. ( TopOpen ` CCfld ) ( A e. w /\ ( F " ( w i^i ( dom F \ { A } ) ) ) C_ v ) ) ) ) )
26 2 25 mpbid 
 |-  ( ph -> ( B e. CC /\ A. v e. ( TopOpen ` CCfld ) ( B e. v -> E. w e. ( TopOpen ` CCfld ) ( A e. w /\ ( F " ( w i^i ( dom F \ { A } ) ) ) C_ v ) ) ) )
27 26 simprd 
 |-  ( ph -> A. v e. ( TopOpen ` CCfld ) ( B e. v -> E. w e. ( TopOpen ` CCfld ) ( A e. w /\ ( F " ( w i^i ( dom F \ { A } ) ) ) C_ v ) ) )
28 27 r19.21bi 
 |-  ( ( ph /\ v e. ( TopOpen ` CCfld ) ) -> ( B e. v -> E. w e. ( TopOpen ` CCfld ) ( A e. w /\ ( F " ( w i^i ( dom F \ { A } ) ) ) C_ v ) ) )
29 28 imp 
 |-  ( ( ( ph /\ v e. ( TopOpen ` CCfld ) ) /\ B e. v ) -> E. w e. ( TopOpen ` CCfld ) ( A e. w /\ ( F " ( w i^i ( dom F \ { A } ) ) ) C_ v ) )
30 17 18 19 29 syl21anc 
 |-  ( ( ( ( ph /\ u e. ( TopOpen ` CCfld ) ) /\ C e. u ) /\ v e. ( TopOpen ` CCfld ) /\ ( B e. v /\ ( G " ( v i^i ( dom G \ { B } ) ) ) C_ u ) ) -> E. w e. ( TopOpen ` CCfld ) ( A e. w /\ ( F " ( w i^i ( dom F \ { A } ) ) ) C_ v ) )
31 imaco 
 |-  ( ( G o. F ) " ( w i^i ( dom F \ { A } ) ) ) = ( G " ( F " ( w i^i ( dom F \ { A } ) ) ) )
32 17 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ u e. ( TopOpen ` CCfld ) ) /\ C e. u ) /\ v e. ( TopOpen ` CCfld ) /\ ( B e. v /\ ( G " ( v i^i ( dom G \ { B } ) ) ) C_ u ) ) /\ w e. ( TopOpen ` CCfld ) ) /\ ( F " ( w i^i ( dom F \ { A } ) ) ) C_ v ) -> ph )
33 simpl3r 
 |-  ( ( ( ( ( ph /\ u e. ( TopOpen ` CCfld ) ) /\ C e. u ) /\ v e. ( TopOpen ` CCfld ) /\ ( B e. v /\ ( G " ( v i^i ( dom G \ { B } ) ) ) C_ u ) ) /\ w e. ( TopOpen ` CCfld ) ) -> ( G " ( v i^i ( dom G \ { B } ) ) ) C_ u )
34 33 adantr 
 |-  ( ( ( ( ( ( ph /\ u e. ( TopOpen ` CCfld ) ) /\ C e. u ) /\ v e. ( TopOpen ` CCfld ) /\ ( B e. v /\ ( G " ( v i^i ( dom G \ { B } ) ) ) C_ u ) ) /\ w e. ( TopOpen ` CCfld ) ) /\ ( F " ( w i^i ( dom F \ { A } ) ) ) C_ v ) -> ( G " ( v i^i ( dom G \ { B } ) ) ) C_ u )
35 simpr 
 |-  ( ( ( ( ( ( ph /\ u e. ( TopOpen ` CCfld ) ) /\ C e. u ) /\ v e. ( TopOpen ` CCfld ) /\ ( B e. v /\ ( G " ( v i^i ( dom G \ { B } ) ) ) C_ u ) ) /\ w e. ( TopOpen ` CCfld ) ) /\ ( F " ( w i^i ( dom F \ { A } ) ) ) C_ v ) -> ( F " ( w i^i ( dom F \ { A } ) ) ) C_ v )
36 simpr 
 |-  ( ( ph /\ ( F " ( w i^i ( dom F \ { A } ) ) ) C_ v ) -> ( F " ( w i^i ( dom F \ { A } ) ) ) C_ v )
37 imassrn 
 |-  ( F " ( w i^i ( dom F \ { A } ) ) ) C_ ran F
38 37 1 sstrid 
 |-  ( ph -> ( F " ( w i^i ( dom F \ { A } ) ) ) C_ ( dom G \ { B } ) )
39 38 adantr 
 |-  ( ( ph /\ ( F " ( w i^i ( dom F \ { A } ) ) ) C_ v ) -> ( F " ( w i^i ( dom F \ { A } ) ) ) C_ ( dom G \ { B } ) )
40 36 39 ssind 
 |-  ( ( ph /\ ( F " ( w i^i ( dom F \ { A } ) ) ) C_ v ) -> ( F " ( w i^i ( dom F \ { A } ) ) ) C_ ( v i^i ( dom G \ { B } ) ) )
41 imass2 
 |-  ( ( F " ( w i^i ( dom F \ { A } ) ) ) C_ ( v i^i ( dom G \ { B } ) ) -> ( G " ( F " ( w i^i ( dom F \ { A } ) ) ) ) C_ ( G " ( v i^i ( dom G \ { B } ) ) ) )
42 40 41 syl 
 |-  ( ( ph /\ ( F " ( w i^i ( dom F \ { A } ) ) ) C_ v ) -> ( G " ( F " ( w i^i ( dom F \ { A } ) ) ) ) C_ ( G " ( v i^i ( dom G \ { B } ) ) ) )
43 42 adantlr 
 |-  ( ( ( ph /\ ( G " ( v i^i ( dom G \ { B } ) ) ) C_ u ) /\ ( F " ( w i^i ( dom F \ { A } ) ) ) C_ v ) -> ( G " ( F " ( w i^i ( dom F \ { A } ) ) ) ) C_ ( G " ( v i^i ( dom G \ { B } ) ) ) )
44 simplr 
 |-  ( ( ( ph /\ ( G " ( v i^i ( dom G \ { B } ) ) ) C_ u ) /\ ( F " ( w i^i ( dom F \ { A } ) ) ) C_ v ) -> ( G " ( v i^i ( dom G \ { B } ) ) ) C_ u )
45 43 44 sstrd 
 |-  ( ( ( ph /\ ( G " ( v i^i ( dom G \ { B } ) ) ) C_ u ) /\ ( F " ( w i^i ( dom F \ { A } ) ) ) C_ v ) -> ( G " ( F " ( w i^i ( dom F \ { A } ) ) ) ) C_ u )
46 32 34 35 45 syl21anc 
 |-  ( ( ( ( ( ( ph /\ u e. ( TopOpen ` CCfld ) ) /\ C e. u ) /\ v e. ( TopOpen ` CCfld ) /\ ( B e. v /\ ( G " ( v i^i ( dom G \ { B } ) ) ) C_ u ) ) /\ w e. ( TopOpen ` CCfld ) ) /\ ( F " ( w i^i ( dom F \ { A } ) ) ) C_ v ) -> ( G " ( F " ( w i^i ( dom F \ { A } ) ) ) ) C_ u )
47 31 46 eqsstrid 
 |-  ( ( ( ( ( ( ph /\ u e. ( TopOpen ` CCfld ) ) /\ C e. u ) /\ v e. ( TopOpen ` CCfld ) /\ ( B e. v /\ ( G " ( v i^i ( dom G \ { B } ) ) ) C_ u ) ) /\ w e. ( TopOpen ` CCfld ) ) /\ ( F " ( w i^i ( dom F \ { A } ) ) ) C_ v ) -> ( ( G o. F ) " ( w i^i ( dom F \ { A } ) ) ) C_ u )
48 47 ex 
 |-  ( ( ( ( ( ph /\ u e. ( TopOpen ` CCfld ) ) /\ C e. u ) /\ v e. ( TopOpen ` CCfld ) /\ ( B e. v /\ ( G " ( v i^i ( dom G \ { B } ) ) ) C_ u ) ) /\ w e. ( TopOpen ` CCfld ) ) -> ( ( F " ( w i^i ( dom F \ { A } ) ) ) C_ v -> ( ( G o. F ) " ( w i^i ( dom F \ { A } ) ) ) C_ u ) )
49 48 anim2d 
 |-  ( ( ( ( ( ph /\ u e. ( TopOpen ` CCfld ) ) /\ C e. u ) /\ v e. ( TopOpen ` CCfld ) /\ ( B e. v /\ ( G " ( v i^i ( dom G \ { B } ) ) ) C_ u ) ) /\ w e. ( TopOpen ` CCfld ) ) -> ( ( A e. w /\ ( F " ( w i^i ( dom F \ { A } ) ) ) C_ v ) -> ( A e. w /\ ( ( G o. F ) " ( w i^i ( dom F \ { A } ) ) ) C_ u ) ) )
50 49 reximdva 
 |-  ( ( ( ( ph /\ u e. ( TopOpen ` CCfld ) ) /\ C e. u ) /\ v e. ( TopOpen ` CCfld ) /\ ( B e. v /\ ( G " ( v i^i ( dom G \ { B } ) ) ) C_ u ) ) -> ( E. w e. ( TopOpen ` CCfld ) ( A e. w /\ ( F " ( w i^i ( dom F \ { A } ) ) ) C_ v ) -> E. w e. ( TopOpen ` CCfld ) ( A e. w /\ ( ( G o. F ) " ( w i^i ( dom F \ { A } ) ) ) C_ u ) ) )
51 30 50 mpd 
 |-  ( ( ( ( ph /\ u e. ( TopOpen ` CCfld ) ) /\ C e. u ) /\ v e. ( TopOpen ` CCfld ) /\ ( B e. v /\ ( G " ( v i^i ( dom G \ { B } ) ) ) C_ u ) ) -> E. w e. ( TopOpen ` CCfld ) ( A e. w /\ ( ( G o. F ) " ( w i^i ( dom F \ { A } ) ) ) C_ u ) )
52 51 rexlimdv3a 
 |-  ( ( ( ph /\ u e. ( TopOpen ` CCfld ) ) /\ C e. u ) -> ( E. v e. ( TopOpen ` CCfld ) ( B e. v /\ ( G " ( v i^i ( dom G \ { B } ) ) ) C_ u ) -> E. w e. ( TopOpen ` CCfld ) ( A e. w /\ ( ( G o. F ) " ( w i^i ( dom F \ { A } ) ) ) C_ u ) ) )
53 16 52 mpd 
 |-  ( ( ( ph /\ u e. ( TopOpen ` CCfld ) ) /\ C e. u ) -> E. w e. ( TopOpen ` CCfld ) ( A e. w /\ ( ( G o. F ) " ( w i^i ( dom F \ { A } ) ) ) C_ u ) )
54 53 ex 
 |-  ( ( ph /\ u e. ( TopOpen ` CCfld ) ) -> ( C e. u -> E. w e. ( TopOpen ` CCfld ) ( A e. w /\ ( ( G o. F ) " ( w i^i ( dom F \ { A } ) ) ) C_ u ) ) )
55 54 ralrimiva 
 |-  ( ph -> A. u e. ( TopOpen ` CCfld ) ( C e. u -> E. w e. ( TopOpen ` CCfld ) ( A e. w /\ ( ( G o. F ) " ( w i^i ( dom F \ { A } ) ) ) C_ u ) ) )
56 22 ffund 
 |-  ( ph -> Fun F )
57 fdmrn 
 |-  ( Fun F <-> F : dom F --> ran F )
58 56 57 sylib 
 |-  ( ph -> F : dom F --> ran F )
59 1 difss2d 
 |-  ( ph -> ran F C_ dom G )
60 58 59 fssd 
 |-  ( ph -> F : dom F --> dom G )
61 fco 
 |-  ( ( G : dom G --> CC /\ F : dom F --> dom G ) -> ( G o. F ) : dom F --> CC )
62 8 60 61 syl2anc 
 |-  ( ph -> ( G o. F ) : dom F --> CC )
63 62 23 24 11 ellimc2 
 |-  ( ph -> ( C e. ( ( G o. F ) limCC A ) <-> ( C e. CC /\ A. u e. ( TopOpen ` CCfld ) ( C e. u -> E. w e. ( TopOpen ` CCfld ) ( A e. w /\ ( ( G o. F ) " ( w i^i ( dom F \ { A } ) ) ) C_ u ) ) ) ) )
64 5 55 63 mpbir2and 
 |-  ( ph -> C e. ( ( G o. F ) limCC A ) )