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⟼DlimℂB↔z∈A∪B⟼ifz=BCD∈JCnPK⁡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 ⊢Ⅎ_yifz=BCz∈A⟼D⁡z
7 nfv ⊢Ⅎzy=B
8 nfcv ⊢Ⅎ_zC
9 nffvmpt1 ⊢Ⅎ_zz∈A⟼D⁡y
10 7 8 9 nfif ⊢Ⅎ_zify=BCz∈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→ifz=BCz∈A⟼D⁡z=ify=BCz∈A⟼D⁡y
14 6 10 13 cbvmpt ⊢z∈A∪B⟼ifz=BCz∈A⟼D⁡z=y∈A∪B⟼ify=BCz∈A⟼D⁡y
15 3 fmpttd ⊢φ→z∈A⟼D:A⟶ℂ
16 4 5 14 15 1 2 ellimc ⊢φ→C∈z∈A⟼DlimℂB↔z∈A∪B⟼ifz=BCz∈A⟼D⁡z∈JCnPK⁡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→ifz=BCz∈A⟼D⁡z=ifz=BCD
30 29 mpteq2dva ⊢φ→z∈A∪B⟼ifz=BCz∈A⟼D⁡z=z∈A∪B⟼ifz=BCD
31 30 eleq1d ⊢φ→z∈A∪B⟼ifz=BCz∈A⟼D⁡z∈JCnPK⁡B↔z∈A∪B⟼ifz=BCD∈JCnPK⁡B
32 16 31 bitrd ⊢φ→C∈z∈A⟼DlimℂB↔z∈A∪B⟼ifz=BCD∈JCnPK⁡B