Metamath Proof Explorer

Theorem cncfi

Description: Defining property of a continuous function. (Contributed by Mario Carneiro, 30-Apr-2014) (Revised by Mario Carneiro, 25-Aug-2014)

Ref Expression
Assertion cncfi ( ( 𝐹 ∈ ( 𝐴 –cn→ 𝐵 ) ∧ 𝐶 ∈ 𝐴 ∧ 𝑅 ∈ ℝ+ ) → ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑤 − 𝐶 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝑅 ) )

Proof

Step Hyp Ref Expression
1 cncfrss ⊢ ( 𝐹 ∈ ( 𝐴 –cn→ 𝐵 ) → 𝐴 ⊆ ℂ )
2 cncfrss2 ⊢ ( 𝐹 ∈ ( 𝐴 –cn→ 𝐵 ) → 𝐵 ⊆ ℂ )
3 elcncf2 ⊢ ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) → ( 𝐹 ∈ ( 𝐴 –cn→ 𝐵 ) ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < 𝑦 ) ) ) )
4 1 2 3 syl2anc ⊢ ( 𝐹 ∈ ( 𝐴 –cn→ 𝐵 ) → ( 𝐹 ∈ ( 𝐴 –cn→ 𝐵 ) ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < 𝑦 ) ) ) )
5 4 ibi ⊢ ( 𝐹 ∈ ( 𝐴 –cn→ 𝐵 ) → ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < 𝑦 ) ) )
6 5 simprd ⊢ ( 𝐹 ∈ ( 𝐴 –cn→ 𝐵 ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < 𝑦 ) )
7 oveq2 ⊢ ( 𝑥 = 𝐶 → ( 𝑤 − 𝑥 ) = ( 𝑤 − 𝐶 ) )
8 7 fveq2d ⊢ ( 𝑥 = 𝐶 → ( abs ‘ ( 𝑤 − 𝑥 ) ) = ( abs ‘ ( 𝑤 − 𝐶 ) ) )
9 8 breq1d ⊢ ( 𝑥 = 𝐶 → ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 ↔ ( abs ‘ ( 𝑤 − 𝐶 ) ) < 𝑧 ) )
10 fveq2 ⊢ ( 𝑥 = 𝐶 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝐶 ) )
11 10 oveq2d ⊢ ( 𝑥 = 𝐶 → ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝐶 ) ) )
12 11 fveq2d ⊢ ( 𝑥 = 𝐶 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝐶 ) ) ) )
13 12 breq1d ⊢ ( 𝑥 = 𝐶 → ( ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < 𝑦 ↔ ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝑦 ) )
14 9 13 imbi12d ⊢ ( 𝑥 = 𝐶 → ( ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < 𝑦 ) ↔ ( ( abs ‘ ( 𝑤 − 𝐶 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝑦 ) ) )
15 14 rexralbidv ⊢ ( 𝑥 = 𝐶 → ( ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < 𝑦 ) ↔ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑤 − 𝐶 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝑦 ) ) )
16 breq2 ⊢ ( 𝑦 = 𝑅 → ( ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝑦 ↔ ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝑅 ) )
17 16 imbi2d ⊢ ( 𝑦 = 𝑅 → ( ( ( abs ‘ ( 𝑤 − 𝐶 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝑦 ) ↔ ( ( abs ‘ ( 𝑤 − 𝐶 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝑅 ) ) )
18 17 rexralbidv ⊢ ( 𝑦 = 𝑅 → ( ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑤 − 𝐶 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝑦 ) ↔ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑤 − 𝐶 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝑅 ) ) )
19 15 18 rspc2v ⊢ ( ( 𝐶 ∈ 𝐴 ∧ 𝑅 ∈ ℝ+ ) → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < 𝑦 ) → ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑤 − 𝐶 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝑅 ) ) )
20 6 19 mpan9 ⊢ ( ( 𝐹 ∈ ( 𝐴 –cn→ 𝐵 ) ∧ ( 𝐶 ∈ 𝐴 ∧ 𝑅 ∈ ℝ+ ) ) → ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑤 − 𝐶 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝑅 ) )
21 20 3impb ⊢ ( ( 𝐹 ∈ ( 𝐴 –cn→ 𝐵 ) ∧ 𝐶 ∈ 𝐴 ∧ 𝑅 ∈ ℝ+ ) → ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑤 − 𝐶 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝑅 ) )