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⟼ifz=BCF⁡z
Assertion limcvallem ⊢F:A⟶ℂ∧A⊆ℂ∧B∈ℂ→G∈JCnPK⁡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⟼ifz=BCF⁡z
4 iftrue ⊢z=B→ifz=BCF⁡z=C
5 4 eleq1d ⊢z=B→ifz=BCF⁡z∈ℂ↔C∈ℂ
6 2 cnfldtopon ⊢K∈TopOn⁡ℂ
7 simpl2 ⊢F:A⟶ℂ∧A⊆ℂ∧B∈ℂ∧G∈JCnPK⁡B→A⊆ℂ
8 simpl3 ⊢F:A⟶ℂ∧A⊆ℂ∧B∈ℂ∧G∈JCnPK⁡B→B∈ℂ
9 8 snssd ⊢F:A⟶ℂ∧A⊆ℂ∧B∈ℂ∧G∈JCnPK⁡B→B⊆ℂ
10 7 9 unssd ⊢F:A⟶ℂ∧A⊆ℂ∧B∈ℂ∧G∈JCnPK⁡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∈JCnPK⁡B→K↾𝑡A∪B∈TopOn⁡A∪B
13 1 12 eqeltrid ⊢F:A⟶ℂ∧A⊆ℂ∧B∈ℂ∧G∈JCnPK⁡B→J∈TopOn⁡A∪B
14 6 a1i ⊢F:A⟶ℂ∧A⊆ℂ∧B∈ℂ∧G∈JCnPK⁡B→K∈TopOn⁡ℂ
15 simpr ⊢F:A⟶ℂ∧A⊆ℂ∧B∈ℂ∧G∈JCnPK⁡B→G∈JCnPK⁡B
16 cnpf2 ⊢J∈TopOn⁡A∪B∧K∈TopOn⁡ℂ∧G∈JCnPK⁡B→G:A∪B⟶ℂ
17 13 14 15 16 syl3anc ⊢F:A⟶ℂ∧A⊆ℂ∧B∈ℂ∧G∈JCnPK⁡B→G:A∪B⟶ℂ
18 3 fmpt ⊢∀z∈A∪Bifz=BCF⁡z∈ℂ↔G:A∪B⟶ℂ
19 17 18 sylibr ⊢F:A⟶ℂ∧A⊆ℂ∧B∈ℂ∧G∈JCnPK⁡B→∀z∈A∪Bifz=BCF⁡z∈ℂ
20 ssun2 ⊢B⊆A∪B
21 snssg ⊢B∈ℂ→B∈A∪B↔B⊆A∪B
22 8 21 syl ⊢F:A⟶ℂ∧A⊆ℂ∧B∈ℂ∧G∈JCnPK⁡B→B∈A∪B↔B⊆A∪B
23 20 22 mpbiri ⊢F:A⟶ℂ∧A⊆ℂ∧B∈ℂ∧G∈JCnPK⁡B→B∈A∪B
24 5 19 23 rspcdva ⊢F:A⟶ℂ∧A⊆ℂ∧B∈ℂ∧G∈JCnPK⁡B→C∈ℂ
25 24 ex ⊢F:A⟶ℂ∧A⊆ℂ∧B∈ℂ→G∈JCnPK⁡B→C∈ℂ