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 ⟼ R lim ℂ X
limcco.d ⊢ φ → D ∈ y ∈ B ⟼ S lim ℂ C
limcco.1 ⊢ y = R → S = T
limcco.2 ⊢ φ ∧ x ∈ A ∧ R = C → T = D
Assertion limcco ⊢ φ → D ∈ x ∈ A ⟼ T lim ℂ 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 ⟼ R lim ℂ X
4 limcco.d ⊢ φ → D ∈ y ∈ B ⟼ S lim ℂ 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 ⟼ R lim ℂ X ⊆ ℂ
10 9 3 sseldi ⊢ φ → 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 ⟼ S lim ℂ 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 ⟼ S lim ℂ C ↔ y ∈ B ∪ C ⟼ if y = C D S ∈ TopOpen ⁡ ℂ fld ↾ 𝑡 B ∪ C CnP TopOpen ⁡ ℂ fld ⁡ C
30 4 29 mpbid ⊢ φ → y ∈ B ∪ C ⟼ if y = C D S ∈ TopOpen ⁡ ℂ fld ↾ 𝑡 B ∪ C CnP TopOpen ⁡ ℂ fld ⁡ C
31 18 26 27 28 3 30 limccnp ⊢ φ → y ∈ B ∪ C ⟼ if y = C D S ⁡ C ∈ y ∈ B ∪ C ⟼ if y = C D S ∘ x ∈ A ⟼ R lim ℂ X
32 eqid ⊢ y ∈ B ∪ C ⟼ if y = C D S = y ∈ B ∪ C ⟼ if y = C D S
33 iftrue ⊢ y = C → if y = C D S = D
34 ssun2 ⊢ C ⊆ B ∪ C
35 snssg ⊢ C ∈ x ∈ A ⟼ R lim ℂ 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 ⟼ if y = C D S ⁡ C = D
39 eqidd ⊢ φ → x ∈ A ⟼ R = x ∈ A ⟼ R
40 eqidd ⊢ φ → y ∈ B ∪ C ⟼ if y = C D S = y ∈ B ∪ 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 ⊢ φ → y ∈ B ∪ C ⟼ if y = C D S ∘ x ∈ A ⟼ R = x ∈ A ⟼ if R = C D T
44 ifid ⊢ if R = C T T = T
45 6 anassrs ⊢ φ ∧ x ∈ A ∧ R = C → T = D
46 45 ifeq1da ⊢ φ ∧ x ∈ A → if R = C T T = if R = C D T
47 44 46 syl5reqr ⊢ φ ∧ x ∈ A → if R = C D T = T
48 47 mpteq2dva ⊢ φ → x ∈ A ⟼ if R = C D T = x ∈ A ⟼ T
49 43 48 eqtrd ⊢ φ → y ∈ B ∪ C ⟼ if y = C D S ∘ x ∈ A ⟼ R = x ∈ A ⟼ T
50 49 oveq1d ⊢ φ → y ∈ B ∪ C ⟼ if y = C D S ∘ x ∈ A ⟼ R lim ℂ X = x ∈ A ⟼ T lim ℂ X
51 31 38 50 3eltr3d ⊢ φ → D ∈ x ∈ A ⟼ T lim ℂ X