Metamath Proof Explorer

Theorem limcco

Description: Composition of two limits. (Contributed by Mario Carneiro, 29-Dec-2016)

Ref Expression
Hypotheses limcco.r 
|- ( ( ph /\ ( x e. A /\ R =/= C ) ) -> R e. B )
limcco.s 
|- ( ( ph /\ y e. B ) -> S e. CC )
limcco.c 
|- ( ph -> C e. ( ( x e. A |-> R ) limCC X ) )
limcco.d 
|- ( ph -> D e. ( ( y e. B |-> S ) limCC C ) )
limcco.1 
|- ( y = R -> S = T )
limcco.2 
|- ( ( ph /\ ( x e. A /\ R = C ) ) -> T = D )
Assertion limcco 
|- ( ph -> D e. ( ( x e. A |-> T ) limCC X ) )

Proof

Step Hyp Ref Expression
1 limcco.r 
 |-  ( ( ph /\ ( x e. A /\ R =/= C ) ) -> R e. B )
2 limcco.s 
 |-  ( ( ph /\ y e. B ) -> S e. CC )
3 limcco.c 
 |-  ( ph -> C e. ( ( x e. A |-> R ) limCC X ) )
4 limcco.d 
 |-  ( ph -> D e. ( ( y e. B |-> S ) limCC C ) )
5 limcco.1 
 |-  ( y = R -> S = T )
6 limcco.2 
 |-  ( ( ph /\ ( x e. A /\ R = C ) ) -> T = D )
7 1 expr 
 |-  ( ( ph /\ x e. A ) -> ( R =/= C -> R e. B ) )
8 7 necon1bd 
 |-  ( ( ph /\ x e. A ) -> ( -. R e. B -> R = C ) )
9 limccl 
 |-  ( ( x e. A |-> R ) limCC X ) C_ CC
10 9 3 sseldi 
 |-  ( ph -> C e. CC )
11 10 adantr 
 |-  ( ( ph /\ x e. A ) -> C e. CC )
12 elsn2g 
 |-  ( C e. CC -> ( R e. { C } <-> R = C ) )
13 11 12 syl 
 |-  ( ( ph /\ x e. A ) -> ( R e. { C } <-> R = C ) )
14 8 13 sylibrd 
 |-  ( ( ph /\ x e. A ) -> ( -. R e. B -> R e. { C } ) )
15 14 orrd 
 |-  ( ( ph /\ x e. A ) -> ( R e. B \/ R e. { C } ) )
16 elun 
 |-  ( R e. ( B u. { C } ) <-> ( R e. B \/ R e. { C } ) )
17 15 16 sylibr 
 |-  ( ( ph /\ x e. A ) -> R e. ( B u. { C } ) )
18 17 fmpttd 
 |-  ( ph -> ( x e. A |-> R ) : A --> ( B u. { C } ) )
19 eqid 
 |-  ( y e. B |-> S ) = ( y e. B |-> S )
20 19 2 dmmptd 
 |-  ( ph -> dom ( y e. B |-> S ) = B )
21 limcrcl 
 |-  ( D e. ( ( y e. B |-> S ) limCC C ) -> ( ( y e. B |-> S ) : dom ( y e. B |-> S ) --> CC /\ dom ( y e. B |-> S ) C_ CC /\ C e. CC ) )
22 4 21 syl 
 |-  ( ph -> ( ( y e. B |-> S ) : dom ( y e. B |-> S ) --> CC /\ dom ( y e. B |-> S ) C_ CC /\ C e. CC ) )
23 22 simp2d 
 |-  ( ph -> dom ( y e. B |-> S ) C_ CC )
24 20 23 eqsstrrd 
 |-  ( ph -> B C_ CC )
25 10 snssd 
 |-  ( ph -> { C } C_ CC )
26 24 25 unssd 
 |-  ( ph -> ( B u. { C } ) C_ CC )
27 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
28 eqid 
 |-  ( ( TopOpen ` CCfld ) |`t ( B u. { C } ) ) = ( ( TopOpen ` CCfld ) |`t ( B u. { C } ) )
29 24 10 2 28 27 limcmpt 
 |-  ( ph -> ( D e. ( ( y e. B |-> S ) limCC C ) <-> ( y e. ( B u. { C } ) |-> if ( y = C , D , S ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( B u. { C } ) ) CnP ( TopOpen ` CCfld ) ) ` C ) ) )
30 4 29 mpbid 
 |-  ( ph -> ( y e. ( B u. { C } ) |-> if ( y = C , D , S ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( B u. { C } ) ) CnP ( TopOpen ` CCfld ) ) ` C ) )
31 18 26 27 28 3 30 limccnp 
 |-  ( ph -> ( ( y e. ( B u. { C } ) |-> if ( y = C , D , S ) ) ` C ) e. ( ( ( y e. ( B u. { C } ) |-> if ( y = C , D , S ) ) o. ( x e. A |-> R ) ) limCC X ) )
32 eqid 
 |-  ( y e. ( B u. { C } ) |-> if ( y = C , D , S ) ) = ( y e. ( B u. { C } ) |-> if ( y = C , D , S ) )
33 iftrue 
 |-  ( y = C -> if ( y = C , D , S ) = D )
34 ssun2 
 |-  { C } C_ ( B u. { C } )
35 snssg 
 |-  ( C e. ( ( x e. A |-> R ) limCC X ) -> ( C e. ( B u. { C } ) <-> { C } C_ ( B u. { C } ) ) )
36 3 35 syl 
 |-  ( ph -> ( C e. ( B u. { C } ) <-> { C } C_ ( B u. { C } ) ) )
37 34 36 mpbiri 
 |-  ( ph -> C e. ( B u. { C } ) )
38 32 33 37 4 fvmptd3 
 |-  ( ph -> ( ( y e. ( B u. { C } ) |-> if ( y = C , D , S ) ) ` C ) = D )
39 eqidd 
 |-  ( ph -> ( x e. A |-> R ) = ( x e. A |-> R ) )
40 eqidd 
 |-  ( ph -> ( y e. ( B u. { C } ) |-> if ( y = C , D , S ) ) = ( y e. ( B u. { C } ) |-> if ( y = C , D , S ) ) )
41 eqeq1 
 |-  ( y = R -> ( y = C <-> R = C ) )
42 41 5 ifbieq2d 
 |-  ( y = R -> if ( y = C , D , S ) = if ( R = C , D , T ) )
43 17 39 40 42 fmptco 
 |-  ( ph -> ( ( y e. ( B u. { C } ) |-> if ( y = C , D , S ) ) o. ( x e. A |-> R ) ) = ( x e. A |-> if ( R = C , D , T ) ) )
44 ifid 
 |-  if ( R = C , T , T ) = T
45 6 anassrs 
 |-  ( ( ( ph /\ x e. A ) /\ R = C ) -> T = D )
46 45 ifeq1da 
 |-  ( ( ph /\ x e. A ) -> if ( R = C , T , T ) = if ( R = C , D , T ) )
47 44 46 syl5reqr 
 |-  ( ( ph /\ x e. A ) -> if ( R = C , D , T ) = T )
48 47 mpteq2dva 
 |-  ( ph -> ( x e. A |-> if ( R = C , D , T ) ) = ( x e. A |-> T ) )
49 43 48 eqtrd 
 |-  ( ph -> ( ( y e. ( B u. { C } ) |-> if ( y = C , D , S ) ) o. ( x e. A |-> R ) ) = ( x e. A |-> T ) )
50 49 oveq1d 
 |-  ( ph -> ( ( ( y e. ( B u. { C } ) |-> if ( y = C , D , S ) ) o. ( x e. A |-> R ) ) limCC X ) = ( ( x e. A |-> T ) limCC X ) )
51 31 38 50 3eltr3d 
 |-  ( ph -> D e. ( ( x e. A |-> T ) limCC X ) )