Metamath Proof Explorer

Theorem limcco

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

Ref Expression
Hypotheses limcco.r ⊢φ∧x∈A∧R≠C→R∈B
limcco.s ⊢φ∧y∈B→S∈ℂ
limcco.c ⊢φ→C∈x∈A⟼RlimℂX
limcco.d ⊢φ→D∈y∈B⟼SlimℂC
limcco.1 ⊢y=R→S=T
limcco.2 ⊢φ∧x∈A∧R=C→T=D
Assertion limcco ⊢φ→D∈x∈A⟼TlimℂX

Proof

Step Hyp Ref Expression
1 limcco.r ⊢φ∧x∈A∧R≠C→R∈B
2 limcco.s ⊢φ∧y∈B→S∈ℂ
3 limcco.c ⊢φ→C∈x∈A⟼RlimℂX
4 limcco.d ⊢φ→D∈y∈B⟼SlimℂC
5 limcco.1 ⊢y=R→S=T
6 limcco.2 ⊢φ∧x∈A∧R=C→T=D
7 1 expr ⊢φ∧x∈A→R≠C→R∈B
8 7 necon1bd ⊢φ∧x∈A→¬R∈B→R=C
9 limccl ⊢x∈A⟼RlimℂX⊆ℂ
10 9 3 sselid ⊢φ→C∈ℂ
11 10 adantr ⊢φ∧x∈A→C∈ℂ
12 elsn2g ⊢C∈ℂ→R∈C↔R=C
13 11 12 syl ⊢φ∧x∈A→R∈C↔R=C
14 8 13 sylibrd ⊢φ∧x∈A→¬R∈B→R∈C
15 14 orrd ⊢φ∧x∈A→R∈B∨R∈C
16 elun ⊢R∈B∪C↔R∈B∨R∈C
17 15 16 sylibr ⊢φ∧x∈A→R∈B∪C
18 17 fmpttd ⊢φ→x∈A⟼R:A⟶B∪C
19 eqid ⊢y∈B⟼S=y∈B⟼S
20 19 2 dmmptd ⊢φ→dom⁡y∈B⟼S=B
21 limcrcl ⊢D∈y∈B⟼SlimℂC→y∈B⟼S:dom⁡y∈B⟼S⟶ℂ∧dom⁡y∈B⟼S⊆ℂ∧C∈ℂ
22 4 21 syl ⊢φ→y∈B⟼S:dom⁡y∈B⟼S⟶ℂ∧dom⁡y∈B⟼S⊆ℂ∧C∈ℂ
23 22 simp2d ⊢φ→dom⁡y∈B⟼S⊆ℂ
24 20 23 eqsstrrd ⊢φ→B⊆ℂ
25 10 snssd ⊢φ→C⊆ℂ
26 24 25 unssd ⊢φ→B∪C⊆ℂ
27 eqid ⊢TopOpen⁡ℂfld=TopOpen⁡ℂfld
28 eqid ⊢TopOpen⁡ℂfld↾𝑡B∪C=TopOpen⁡ℂfld↾𝑡B∪C
29 24 10 2 28 27 limcmpt ⊢φ→D∈y∈B⟼SlimℂC↔y∈B∪C⟼ify=CDS∈TopOpen⁡ℂfld↾𝑡B∪CCnPTopOpen⁡ℂfld⁡C
30 4 29 mpbid ⊢φ→y∈B∪C⟼ify=CDS∈TopOpen⁡ℂfld↾𝑡B∪CCnPTopOpen⁡ℂfld⁡C
31 18 26 27 28 3 30 limccnp ⊢φ→y∈B∪C⟼ify=CDS⁡C∈y∈B∪C⟼ify=CDS∘x∈A⟼RlimℂX
32 eqid ⊢y∈B∪C⟼ify=CDS=y∈B∪C⟼ify=CDS
33 iftrue ⊢y=C→ify=CDS=D
34 ssun2 ⊢C⊆B∪C
35 snssg ⊢C∈x∈A⟼RlimℂX→C∈B∪C↔C⊆B∪C
36 3 35 syl ⊢φ→C∈B∪C↔C⊆B∪C
37 34 36 mpbiri ⊢φ→C∈B∪C
38 32 33 37 4 fvmptd3 ⊢φ→y∈B∪C⟼ify=CDS⁡C=D
39 eqidd ⊢φ→x∈A⟼R=x∈A⟼R
40 eqidd ⊢φ→y∈B∪C⟼ify=CDS=y∈B∪C⟼ify=CDS
41 eqeq1 ⊢y=R→y=C↔R=C
42 41 5 ifbieq2d ⊢y=R→ify=CDS=ifR=CDT
43 17 39 40 42 fmptco ⊢φ→y∈B∪C⟼ify=CDS∘x∈A⟼R=x∈A⟼ifR=CDT
44 6 anassrs ⊢φ∧x∈A∧R=C→T=D
45 44 ifeq1da ⊢φ∧x∈A→ifR=CTT=ifR=CDT
46 ifid ⊢ifR=CTT=T
47 45 46 eqtr3di ⊢φ∧x∈A→ifR=CDT=T
48 47 mpteq2dva ⊢φ→x∈A⟼ifR=CDT=x∈A⟼T
49 43 48 eqtrd ⊢φ→y∈B∪C⟼ify=CDS∘x∈A⟼R=x∈A⟼T
50 49 oveq1d ⊢φ→y∈B∪C⟼ify=CDS∘x∈A⟼RlimℂX=x∈A⟼TlimℂX
51 31 38 50 3eltr3d ⊢φ→D∈x∈A⟼TlimℂX