Metamath Proof Explorer

Theorem limcco

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

Ref Expression
Hypotheses limcco.r ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑅 ≠ 𝐶 ) ) → 𝑅 ∈ 𝐵 )
limcco.s ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → 𝑆 ∈ ℂ )
limcco.c ⊢ ( 𝜑 → 𝐶 ∈ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) limℂ 𝑋 ) )
limcco.d ⊢ ( 𝜑 → 𝐷 ∈ ( ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) limℂ 𝐶 ) )
limcco.1 ⊢ ( 𝑦 = 𝑅 → 𝑆 = 𝑇 )
limcco.2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑅 = 𝐶 ) ) → 𝑇 = 𝐷 )
Assertion limcco ( 𝜑 → 𝐷 ∈ ( ( 𝑥 ∈ 𝐴 ↦ 𝑇 ) limℂ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 limcco.r ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑅 ≠ 𝐶 ) ) → 𝑅 ∈ 𝐵 )
2 limcco.s ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → 𝑆 ∈ ℂ )
3 limcco.c ⊢ ( 𝜑 → 𝐶 ∈ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) limℂ 𝑋 ) )
4 limcco.d ⊢ ( 𝜑 → 𝐷 ∈ ( ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) limℂ 𝐶 ) )
5 limcco.1 ⊢ ( 𝑦 = 𝑅 → 𝑆 = 𝑇 )
6 limcco.2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑅 = 𝐶 ) ) → 𝑇 = 𝐷 )
7 1 expr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑅 ≠ 𝐶 → 𝑅 ∈ 𝐵 ) )
8 7 necon1bd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ¬ 𝑅 ∈ 𝐵 → 𝑅 = 𝐶 ) )
9 limccl ⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) limℂ 𝑋 ) ⊆ ℂ
10 9 3 sselid ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
11 10 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
12 elsn2g ⊢ ( 𝐶 ∈ ℂ → ( 𝑅 ∈ { 𝐶 } ↔ 𝑅 = 𝐶 ) )
13 11 12 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑅 ∈ { 𝐶 } ↔ 𝑅 = 𝐶 ) )
14 8 13 sylibrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ¬ 𝑅 ∈ 𝐵 → 𝑅 ∈ { 𝐶 } ) )
15 14 orrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑅 ∈ 𝐵 ∨ 𝑅 ∈ { 𝐶 } ) )
16 elun ⊢ ( 𝑅 ∈ ( 𝐵 ∪ { 𝐶 } ) ↔ ( 𝑅 ∈ 𝐵 ∨ 𝑅 ∈ { 𝐶 } ) )
17 15 16 sylibr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑅 ∈ ( 𝐵 ∪ { 𝐶 } ) )
18 17 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) : 𝐴 ⟶ ( 𝐵 ∪ { 𝐶 } ) )
19 eqid ⊢ ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) = ( 𝑦 ∈ 𝐵 ↦ 𝑆 )
20 19 2 dmmptd ⊢ ( 𝜑 → dom ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) = 𝐵 )
21 limcrcl ⊢ ( 𝐷 ∈ ( ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) limℂ 𝐶 ) → ( ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) : dom ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) ⟶ ℂ ∧ dom ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) ⊆ ℂ ∧ 𝐶 ∈ ℂ ) )
22 4 21 syl ⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) : dom ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) ⟶ ℂ ∧ dom ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) ⊆ ℂ ∧ 𝐶 ∈ ℂ ) )
23 22 simp2d ⊢ ( 𝜑 → dom ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) ⊆ ℂ )
24 20 23 eqsstrrd ⊢ ( 𝜑 → 𝐵 ⊆ ℂ )
25 10 snssd ⊢ ( 𝜑 → { 𝐶 } ⊆ ℂ )
26 24 25 unssd ⊢ ( 𝜑 → ( 𝐵 ∪ { 𝐶 } ) ⊆ ℂ )
27 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
28 eqid ⊢ ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐵 ∪ { 𝐶 } ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐵 ∪ { 𝐶 } ) )
29 24 10 2 28 27 limcmpt ⊢ ( 𝜑 → ( 𝐷 ∈ ( ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) limℂ 𝐶 ) ↔ ( 𝑦 ∈ ( 𝐵 ∪ { 𝐶 } ) ↦ if ( 𝑦 = 𝐶 , 𝐷 , 𝑆 ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐵 ∪ { 𝐶 } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝐶 ) ) )
30 4 29 mpbid ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐵 ∪ { 𝐶 } ) ↦ if ( 𝑦 = 𝐶 , 𝐷 , 𝑆 ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐵 ∪ { 𝐶 } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝐶 ) )
31 18 26 27 28 3 30 limccnp ⊢ ( 𝜑 → ( ( 𝑦 ∈ ( 𝐵 ∪ { 𝐶 } ) ↦ if ( 𝑦 = 𝐶 , 𝐷 , 𝑆 ) ) ‘ 𝐶 ) ∈ ( ( ( 𝑦 ∈ ( 𝐵 ∪ { 𝐶 } ) ↦ if ( 𝑦 = 𝐶 , 𝐷 , 𝑆 ) ) ∘ ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ) limℂ 𝑋 ) )
32 eqid ⊢ ( 𝑦 ∈ ( 𝐵 ∪ { 𝐶 } ) ↦ if ( 𝑦 = 𝐶 , 𝐷 , 𝑆 ) ) = ( 𝑦 ∈ ( 𝐵 ∪ { 𝐶 } ) ↦ if ( 𝑦 = 𝐶 , 𝐷 , 𝑆 ) )
33 iftrue ⊢ ( 𝑦 = 𝐶 → if ( 𝑦 = 𝐶 , 𝐷 , 𝑆 ) = 𝐷 )
34 ssun2 ⊢ { 𝐶 } ⊆ ( 𝐵 ∪ { 𝐶 } )
35 snssg ⊢ ( 𝐶 ∈ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) limℂ 𝑋 ) → ( 𝐶 ∈ ( 𝐵 ∪ { 𝐶 } ) ↔ { 𝐶 } ⊆ ( 𝐵 ∪ { 𝐶 } ) ) )
36 3 35 syl ⊢ ( 𝜑 → ( 𝐶 ∈ ( 𝐵 ∪ { 𝐶 } ) ↔ { 𝐶 } ⊆ ( 𝐵 ∪ { 𝐶 } ) ) )
37 34 36 mpbiri ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐵 ∪ { 𝐶 } ) )
38 32 33 37 4 fvmptd3 ⊢ ( 𝜑 → ( ( 𝑦 ∈ ( 𝐵 ∪ { 𝐶 } ) ↦ if ( 𝑦 = 𝐶 , 𝐷 , 𝑆 ) ) ‘ 𝐶 ) = 𝐷 )
39 eqidd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) = ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) )
40 eqidd ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐵 ∪ { 𝐶 } ) ↦ if ( 𝑦 = 𝐶 , 𝐷 , 𝑆 ) ) = ( 𝑦 ∈ ( 𝐵 ∪ { 𝐶 } ) ↦ if ( 𝑦 = 𝐶 , 𝐷 , 𝑆 ) ) )
41 eqeq1 ⊢ ( 𝑦 = 𝑅 → ( 𝑦 = 𝐶 ↔ 𝑅 = 𝐶 ) )
42 41 5 ifbieq2d ⊢ ( 𝑦 = 𝑅 → if ( 𝑦 = 𝐶 , 𝐷 , 𝑆 ) = if ( 𝑅 = 𝐶 , 𝐷 , 𝑇 ) )
43 17 39 40 42 fmptco ⊢ ( 𝜑 → ( ( 𝑦 ∈ ( 𝐵 ∪ { 𝐶 } ) ↦ if ( 𝑦 = 𝐶 , 𝐷 , 𝑆 ) ) ∘ ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ) = ( 𝑥 ∈ 𝐴 ↦ if ( 𝑅 = 𝐶 , 𝐷 , 𝑇 ) ) )
44 6 anassrs ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑅 = 𝐶 ) → 𝑇 = 𝐷 )
45 44 ifeq1da ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 𝑅 = 𝐶 , 𝑇 , 𝑇 ) = if ( 𝑅 = 𝐶 , 𝐷 , 𝑇 ) )
46 ifid ⊢ if ( 𝑅 = 𝐶 , 𝑇 , 𝑇 ) = 𝑇
47 45 46 eqtr3di ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 𝑅 = 𝐶 , 𝐷 , 𝑇 ) = 𝑇 )
48 47 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ if ( 𝑅 = 𝐶 , 𝐷 , 𝑇 ) ) = ( 𝑥 ∈ 𝐴 ↦ 𝑇 ) )
49 43 48 eqtrd ⊢ ( 𝜑 → ( ( 𝑦 ∈ ( 𝐵 ∪ { 𝐶 } ) ↦ if ( 𝑦 = 𝐶 , 𝐷 , 𝑆 ) ) ∘ ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ) = ( 𝑥 ∈ 𝐴 ↦ 𝑇 ) )
50 49 oveq1d ⊢ ( 𝜑 → ( ( ( 𝑦 ∈ ( 𝐵 ∪ { 𝐶 } ) ↦ if ( 𝑦 = 𝐶 , 𝐷 , 𝑆 ) ) ∘ ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ) limℂ 𝑋 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝑇 ) limℂ 𝑋 ) )
51 31 38 50 3eltr3d ⊢ ( 𝜑 → 𝐷 ∈ ( ( 𝑥 ∈ 𝐴 ↦ 𝑇 ) limℂ 𝑋 ) )