Metamath Proof Explorer

Theorem limcmpt2

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

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

Proof

Step Hyp Ref Expression
1 limcmpt2.a ⊢ φ → A ⊆ ℂ
2 limcmpt2.b ⊢ φ → B ∈ A
3 limcmpt2.f ⊢ φ ∧ z ∈ A ∧ z ≠ B → D ∈ ℂ
4 limcmpt2.j ⊢ J = K ↾ 𝑡 A
5 limcmpt2.k ⊢ K = TopOpen ⁡ ℂ fld
6 1 ssdifssd ⊢ φ → A ∖ B ⊆ ℂ
7 1 2 sseldd ⊢ φ → B ∈ ℂ
8 eldifsn ⊢ z ∈ A ∖ B ↔ z ∈ A ∧ z ≠ B
9 8 3 sylan2b ⊢ φ ∧ z ∈ A ∖ B → D ∈ ℂ
10 eqid ⊢ K ↾ 𝑡 A ∖ B ∪ B = K ↾ 𝑡 A ∖ B ∪ B
11 6 7 9 10 5 limcmpt ⊢ φ → C ∈ z ∈ A ∖ B ⟼ D lim ℂ B ↔ z ∈ A ∖ B ∪ B ⟼ if z = B C D ∈ K ↾ 𝑡 A ∖ B ∪ B CnP K ⁡ B
12 undif1 ⊢ A ∖ B ∪ B = A ∪ B
13 2 snssd ⊢ φ → B ⊆ A
14 ssequn2 ⊢ B ⊆ A ↔ A ∪ B = A
15 13 14 sylib ⊢ φ → A ∪ B = A
16 12 15 syl5eq ⊢ φ → A ∖ B ∪ B = A
17 16 mpteq1d ⊢ φ → z ∈ A ∖ B ∪ B ⟼ if z = B C D = z ∈ A ⟼ if z = B C D
18 16 oveq2d ⊢ φ → K ↾ 𝑡 A ∖ B ∪ B = K ↾ 𝑡 A
19 18 4 eqtr4di ⊢ φ → K ↾ 𝑡 A ∖ B ∪ B = J
20 19 oveq1d ⊢ φ → K ↾ 𝑡 A ∖ B ∪ B CnP K = J CnP K
21 20 fveq1d ⊢ φ → K ↾ 𝑡 A ∖ B ∪ B CnP K ⁡ B = J CnP K ⁡ B
22 17 21 eleq12d ⊢ φ → z ∈ A ∖ B ∪ B ⟼ if z = B C D ∈ K ↾ 𝑡 A ∖ B ∪ B CnP K ⁡ B ↔ z ∈ A ⟼ if z = B C D ∈ J CnP K ⁡ B
23 11 22 bitrd ⊢ φ → C ∈ z ∈ A ∖ B ⟼ D lim ℂ B ↔ z ∈ A ⟼ if z = B C D ∈ J CnP K ⁡ B