This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem limcvallem

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

Ref Expression
Hypotheses limcval.j ⊢ 𝐽 = ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) )
limcval.k ⊢ 𝐾 = ( TopOpen ‘ ℂfld )
limcvallem.g ⊢ 𝐺 = ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) )
Assertion limcvallem ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐺 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) → 𝐶 ∈ ℂ ) )

Proof

Step Hyp Ref Expression
1 limcval.j ⊢ 𝐽 = ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) )
2 limcval.k ⊢ 𝐾 = ( TopOpen ‘ ℂfld )
3 limcvallem.g ⊢ 𝐺 = ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) )
4 iftrue ⊢ ( 𝑧 = 𝐵 → if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) = 𝐶 )
5 4 eleq1d ⊢ ( 𝑧 = 𝐵 → ( if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ∈ ℂ ↔ 𝐶 ∈ ℂ ) )
6 2 cnfldtopon ⊢ 𝐾 ∈ ( TopOn ‘ ℂ )
7 simpl2 ⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝐺 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) ) → 𝐴 ⊆ ℂ )
8 simpl3 ⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝐺 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) ) → 𝐵 ∈ ℂ )
9 8 snssd ⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝐺 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) ) → { 𝐵 } ⊆ ℂ )
10 7 9 unssd ⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝐺 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) ) → ( 𝐴 ∪ { 𝐵 } ) ⊆ ℂ )
11 resttopon ⊢ ( ( 𝐾 ∈ ( TopOn ‘ ℂ ) ∧ ( 𝐴 ∪ { 𝐵 } ) ⊆ ℂ ) → ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) ∈ ( TopOn ‘ ( 𝐴 ∪ { 𝐵 } ) ) )
12 6 10 11 sylancr ⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝐺 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) ) → ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) ∈ ( TopOn ‘ ( 𝐴 ∪ { 𝐵 } ) ) )
13 1 12 eqeltrid ⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝐺 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) ) → 𝐽 ∈ ( TopOn ‘ ( 𝐴 ∪ { 𝐵 } ) ) )
14 6 a1i ⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝐺 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) ) → 𝐾 ∈ ( TopOn ‘ ℂ ) )
15 simpr ⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝐺 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) ) → 𝐺 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) )
16 cnpf2 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ ( 𝐴 ∪ { 𝐵 } ) ) ∧ 𝐾 ∈ ( TopOn ‘ ℂ ) ∧ 𝐺 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) ) → 𝐺 : ( 𝐴 ∪ { 𝐵 } ) ⟶ ℂ )
17 13 14 15 16 syl3anc ⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝐺 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) ) → 𝐺 : ( 𝐴 ∪ { 𝐵 } ) ⟶ ℂ )
18 3 fmpt ⊢ ( ∀ 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ∈ ℂ ↔ 𝐺 : ( 𝐴 ∪ { 𝐵 } ) ⟶ ℂ )
19 17 18 sylibr ⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝐺 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) ) → ∀ 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ∈ ℂ )
20 ssun2 ⊢ { 𝐵 } ⊆ ( 𝐴 ∪ { 𝐵 } )
21 snssg ⊢ ( 𝐵 ∈ ℂ → ( 𝐵 ∈ ( 𝐴 ∪ { 𝐵 } ) ↔ { 𝐵 } ⊆ ( 𝐴 ∪ { 𝐵 } ) ) )
22 8 21 syl ⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝐺 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) ) → ( 𝐵 ∈ ( 𝐴 ∪ { 𝐵 } ) ↔ { 𝐵 } ⊆ ( 𝐴 ∪ { 𝐵 } ) ) )
23 20 22 mpbiri ⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝐺 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) ) → 𝐵 ∈ ( 𝐴 ∪ { 𝐵 } ) )
24 5 19 23 rspcdva ⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝐺 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) ) → 𝐶 ∈ ℂ )
25 24 ex ⊢ ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐺 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) → 𝐶 ∈ ℂ ) )