Metamath Proof Explorer

Theorem limcmpt

Description: Express the limit operator for a function defined by a mapping. (Contributed by Mario Carneiro, 25-Dec-2016)

Ref Expression
Hypotheses limcmpt.a ⊢ φ → A ⊆ ℂ
limcmpt.b ⊢ φ → B ∈ ℂ
limcmpt.f ⊢ φ ∧ z ∈ A → D ∈ ℂ
limcmpt.j ⊢ J = K ↾ 𝑡 A ∪ B
limcmpt.k ⊢ K = TopOpen ⁡ ℂ fld
Assertion limcmpt ⊢ φ → C ∈ z ∈ A ⟼ D lim ℂ B ↔ z ∈ A ∪ B ⟼ if z = B C D ∈ J CnP K ⁡ B

Proof

Step Hyp Ref Expression
1 limcmpt.a ⊢ φ → A ⊆ ℂ
2 limcmpt.b ⊢ φ → B ∈ ℂ
3 limcmpt.f ⊢ φ ∧ z ∈ A → D ∈ ℂ
4 limcmpt.j ⊢ J = K ↾ 𝑡 A ∪ B
5 limcmpt.k ⊢ K = TopOpen ⁡ ℂ fld
6 nfcv ⊢ Ⅎ _ y if z = B C z ∈ A ⟼ D ⁡ z
7 nfv ⊢ Ⅎ z y = B
8 nfcv ⊢ Ⅎ _ z C
9 nffvmpt1 ⊢ Ⅎ _ z z ∈ A ⟼ D ⁡ y
10 7 8 9 nfif ⊢ Ⅎ _ z if y = B C z ∈ A ⟼ D ⁡ y
11 eqeq1 ⊢ z = y → z = B ↔ y = B
12 fveq2 ⊢ z = y → z ∈ A ⟼ D ⁡ z = z ∈ A ⟼ D ⁡ y
13 11 12 ifbieq2d ⊢ z = y → if z = B C z ∈ A ⟼ D ⁡ z = if y = B C z ∈ A ⟼ D ⁡ y
14 6 10 13 cbvmpt ⊢ z ∈ A ∪ B ⟼ if z = B C z ∈ A ⟼ D ⁡ z = y ∈ A ∪ B ⟼ if y = B C z ∈ A ⟼ D ⁡ y
15 3 fmpttd ⊢ φ → z ∈ A ⟼ D : A ⟶ ℂ
16 4 5 14 15 1 2 ellimc ⊢ φ → C ∈ z ∈ A ⟼ D lim ℂ B ↔ z ∈ A ∪ B ⟼ if z = B C z ∈ A ⟼ D ⁡ z ∈ J CnP K ⁡ B
17 elun ⊢ z ∈ A ∪ B ↔ z ∈ A ∨ z ∈ B
18 velsn ⊢ z ∈ B ↔ z = B
19 18 orbi2i ⊢ z ∈ A ∨ z ∈ B ↔ z ∈ A ∨ z = B
20 17 19 bitri ⊢ z ∈ A ∪ B ↔ z ∈ A ∨ z = B
21 pm5.61 ⊢ z ∈ A ∨ z = B ∧ ¬ z = B ↔ z ∈ A ∧ ¬ z = B
22 21 simplbi ⊢ z ∈ A ∨ z = B ∧ ¬ z = B → z ∈ A
23 20 22 sylanb ⊢ z ∈ A ∪ B ∧ ¬ z = B → z ∈ A
24 23 3 sylan2 ⊢ φ ∧ z ∈ A ∪ B ∧ ¬ z = B → D ∈ ℂ
25 eqid ⊢ z ∈ A ⟼ D = z ∈ A ⟼ D
26 25 fvmpt2 ⊢ z ∈ A ∧ D ∈ ℂ → z ∈ A ⟼ D ⁡ z = D
27 23 24 26 syl2an2 ⊢ φ ∧ z ∈ A ∪ B ∧ ¬ z = B → z ∈ A ⟼ D ⁡ z = D
28 27 anassrs ⊢ φ ∧ z ∈ A ∪ B ∧ ¬ z = B → z ∈ A ⟼ D ⁡ z = D
29 28 ifeq2da ⊢ φ ∧ z ∈ A ∪ B → if z = B C z ∈ A ⟼ D ⁡ z = if z = B C D
30 29 mpteq2dva ⊢ φ → z ∈ A ∪ B ⟼ if z = B C z ∈ A ⟼ D ⁡ z = z ∈ A ∪ B ⟼ if z = B C D
31 30 eleq1d ⊢ φ → z ∈ A ∪ B ⟼ if z = B C z ∈ A ⟼ D ⁡ z ∈ J CnP K ⁡ B ↔ z ∈ A ∪ B ⟼ if z = B C D ∈ J CnP K ⁡ B
32 16 31 bitrd ⊢ φ → C ∈ z ∈ A ⟼ D lim ℂ B ↔ z ∈ A ∪ B ⟼ if z = B C D ∈ J CnP K ⁡ B