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 𝐾 ) ‘ 𝐵 ) → 𝐶 ∈ ℂ ) )