Theorem cnlimc

Description: F is a continuous function iff the limit of the function at each point equals the value of the function. (Contributed by Mario Carneiro, 28-Dec-2016)

	Ref	Expression
Assertion	cnlimc	⊢ ( 𝐴 ⊆ ℂ → ( 𝐹 ∈ ( 𝐴 –cn→ ℂ ) ↔ ( 𝐹 : 𝐴 ⟶ ℂ ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 limℂ 𝑥 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		ssid	⊢ ℂ ⊆ ℂ
2		eqid	⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
3		eqid	⊢ ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) = ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 )
4	2	cnfldtopon	⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
5	4	toponrestid	⊢ ( TopOpen ‘ ℂfld ) = ( ( TopOpen ‘ ℂfld ) ↾t ℂ )
6	2 3 5	cncfcn	⊢ ( ( 𝐴 ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝐴 –cn→ ℂ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) Cn ( TopOpen ‘ ℂfld ) ) )
7	1 6	mpan2	⊢ ( 𝐴 ⊆ ℂ → ( 𝐴 –cn→ ℂ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) Cn ( TopOpen ‘ ℂfld ) ) )
8	7	eleq2d	⊢ ( 𝐴 ⊆ ℂ → ( 𝐹 ∈ ( 𝐴 –cn→ ℂ ) ↔ 𝐹 ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) Cn ( TopOpen ‘ ℂfld ) ) ) )
9		resttopon	⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ∧ 𝐴 ⊆ ℂ ) → ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) ∈ ( TopOn ‘ 𝐴 ) )
10	4 9	mpan	⊢ ( 𝐴 ⊆ ℂ → ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) ∈ ( TopOn ‘ 𝐴 ) )
11		cncnp	⊢ ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) ∈ ( TopOn ‘ 𝐴 ) ∧ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ) → ( 𝐹 ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) Cn ( TopOpen ‘ ℂfld ) ) ↔ ( 𝐹 : 𝐴 ⟶ ℂ ∧ ∀ 𝑥 ∈ 𝐴 𝐹 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑥 ) ) ) )
12	10 4 11	sylancl	⊢ ( 𝐴 ⊆ ℂ → ( 𝐹 ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) Cn ( TopOpen ‘ ℂfld ) ) ↔ ( 𝐹 : 𝐴 ⟶ ℂ ∧ ∀ 𝑥 ∈ 𝐴 𝐹 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑥 ) ) ) )
13	2 3	cnplimc	⊢ ( ( 𝐴 ⊆ ℂ ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑥 ) ↔ ( 𝐹 : 𝐴 ⟶ ℂ ∧ ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 limℂ 𝑥 ) ) ) )
14	13	baibd	⊢ ( ( ( 𝐴 ⊆ ℂ ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐹 : 𝐴 ⟶ ℂ ) → ( 𝐹 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 limℂ 𝑥 ) ) )
15	14	an32s	⊢ ( ( ( 𝐴 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 limℂ 𝑥 ) ) )
16	15	ralbidva	⊢ ( ( 𝐴 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ) → ( ∀ 𝑥 ∈ 𝐴 𝐹 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 limℂ 𝑥 ) ) )
17	16	pm5.32da	⊢ ( 𝐴 ⊆ ℂ → ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ ∀ 𝑥 ∈ 𝐴 𝐹 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑥 ) ) ↔ ( 𝐹 : 𝐴 ⟶ ℂ ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 limℂ 𝑥 ) ) ) )
18	8 12 17	3bitrd	⊢ ( 𝐴 ⊆ ℂ → ( 𝐹 ∈ ( 𝐴 –cn→ ℂ ) ↔ ( 𝐹 : 𝐴 ⟶ ℂ ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 limℂ 𝑥 ) ) ) )