Metamath Proof Explorer

Theorem limcvallem

Description: Lemma for ellimc . (Contributed by Mario Carneiro, 25-Dec-2016)

Ref Expression
Hypotheses limcval.j ⊢ J = K ↾ 𝑡 A ∪ B
limcval.k ⊢ K = TopOpen ⁡ ℂ fld
limcvallem.g ⊢ G = z ∈ A ∪ B ⟼ if z = B C F ⁡ z
Assertion limcvallem ⊢ F : A ⟶ ℂ ∧ A ⊆ ℂ ∧ B ∈ ℂ → G ∈ J CnP K ⁡ B → C ∈ ℂ

Proof

Step Hyp Ref Expression
1 limcval.j ⊢ J = K ↾ 𝑡 A ∪ B
2 limcval.k ⊢ K = TopOpen ⁡ ℂ fld
3 limcvallem.g ⊢ G = z ∈ A ∪ B ⟼ if z = B C F ⁡ z
4 iftrue ⊢ z = B → if z = B C F ⁡ z = C
5 4 eleq1d ⊢ z = B → if z = B C F ⁡ z ∈ ℂ ↔ C ∈ ℂ
6 2 cnfldtopon ⊢ K ∈ TopOn ⁡ ℂ
7 simpl2 ⊢ F : A ⟶ ℂ ∧ A ⊆ ℂ ∧ B ∈ ℂ ∧ G ∈ J CnP K ⁡ B → A ⊆ ℂ
8 simpl3 ⊢ F : A ⟶ ℂ ∧ A ⊆ ℂ ∧ B ∈ ℂ ∧ G ∈ J CnP K ⁡ B → B ∈ ℂ
9 8 snssd ⊢ F : A ⟶ ℂ ∧ A ⊆ ℂ ∧ B ∈ ℂ ∧ G ∈ J CnP K ⁡ B → B ⊆ ℂ
10 7 9 unssd ⊢ F : A ⟶ ℂ ∧ A ⊆ ℂ ∧ B ∈ ℂ ∧ G ∈ J CnP K ⁡ B → A ∪ B ⊆ ℂ
11 resttopon ⊢ K ∈ TopOn ⁡ ℂ ∧ A ∪ B ⊆ ℂ → K ↾ 𝑡 A ∪ B ∈ TopOn ⁡ A ∪ B
12 6 10 11 sylancr ⊢ F : A ⟶ ℂ ∧ A ⊆ ℂ ∧ B ∈ ℂ ∧ G ∈ J CnP K ⁡ B → K ↾ 𝑡 A ∪ B ∈ TopOn ⁡ A ∪ B
13 1 12 eqeltrid ⊢ F : A ⟶ ℂ ∧ A ⊆ ℂ ∧ B ∈ ℂ ∧ G ∈ J CnP K ⁡ B → J ∈ TopOn ⁡ A ∪ B
14 6 a1i ⊢ F : A ⟶ ℂ ∧ A ⊆ ℂ ∧ B ∈ ℂ ∧ G ∈ J CnP K ⁡ B → K ∈ TopOn ⁡ ℂ
15 simpr ⊢ F : A ⟶ ℂ ∧ A ⊆ ℂ ∧ B ∈ ℂ ∧ G ∈ J CnP K ⁡ B → G ∈ J CnP K ⁡ B
16 cnpf2 ⊢ J ∈ TopOn ⁡ A ∪ B ∧ K ∈ TopOn ⁡ ℂ ∧ G ∈ J CnP K ⁡ B → G : A ∪ B ⟶ ℂ
17 13 14 15 16 syl3anc ⊢ F : A ⟶ ℂ ∧ A ⊆ ℂ ∧ B ∈ ℂ ∧ G ∈ J CnP K ⁡ B → G : A ∪ B ⟶ ℂ
18 3 fmpt ⊢ ∀ z ∈ A ∪ B if z = B C F ⁡ z ∈ ℂ ↔ G : A ∪ B ⟶ ℂ
19 17 18 sylibr ⊢ F : A ⟶ ℂ ∧ A ⊆ ℂ ∧ B ∈ ℂ ∧ G ∈ J CnP K ⁡ B → ∀ z ∈ A ∪ B if z = B C F ⁡ z ∈ ℂ
20 ssun2 ⊢ B ⊆ A ∪ B
21 snssg ⊢ B ∈ ℂ → B ∈ A ∪ B ↔ B ⊆ A ∪ B
22 8 21 syl ⊢ F : A ⟶ ℂ ∧ A ⊆ ℂ ∧ B ∈ ℂ ∧ G ∈ J CnP K ⁡ B → B ∈ A ∪ B ↔ B ⊆ A ∪ B
23 20 22 mpbiri ⊢ F : A ⟶ ℂ ∧ A ⊆ ℂ ∧ B ∈ ℂ ∧ G ∈ J CnP K ⁡ B → B ∈ A ∪ B
24 5 19 23 rspcdva ⊢ F : A ⟶ ℂ ∧ A ⊆ ℂ ∧ B ∈ ℂ ∧ G ∈ J CnP K ⁡ B → C ∈ ℂ
25 24 ex ⊢ F : A ⟶ ℂ ∧ A ⊆ ℂ ∧ B ∈ ℂ → G ∈ J CnP K ⁡ B → C ∈ ℂ