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 ⊢ F : A ⟶cn B ∧ C ∈ A ∧ R ∈ ℝ + → ∃ z ∈ ℝ + ∀ w ∈ A w − C < z → F ⁡ w − F ⁡ C < R

Proof

Step Hyp Ref Expression
1 cncfrss ⊢ F : A ⟶cn B → A ⊆ ℂ
2 cncfrss2 ⊢ F : A ⟶cn B → B ⊆ ℂ
3 elcncf2 ⊢ A ⊆ ℂ ∧ B ⊆ ℂ → F : A ⟶cn B ↔ F : A ⟶ B ∧ ∀ x ∈ A ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ A w − x < z → F ⁡ w − F ⁡ x < y
4 1 2 3 syl2anc ⊢ F : A ⟶cn B → F : A ⟶cn B ↔ F : A ⟶ B ∧ ∀ x ∈ A ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ A w − x < z → F ⁡ w − F ⁡ x < y
5 4 ibi ⊢ F : A ⟶cn B → F : A ⟶ B ∧ ∀ x ∈ A ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ A w − x < z → F ⁡ w − F ⁡ x < y
6 5 simprd ⊢ F : A ⟶cn B → ∀ x ∈ A ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ A w − x < z → F ⁡ w − F ⁡ x < y
7 oveq2 ⊢ x = C → w − x = w − C
8 7 fveq2d ⊢ x = C → w − x = w − C
9 8 breq1d ⊢ x = C → w − x < z ↔ w − C < z
10 fveq2 ⊢ x = C → F ⁡ x = F ⁡ C
11 10 oveq2d ⊢ x = C → F ⁡ w − F ⁡ x = F ⁡ w − F ⁡ C
12 11 fveq2d ⊢ x = C → F ⁡ w − F ⁡ x = F ⁡ w − F ⁡ C
13 12 breq1d ⊢ x = C → F ⁡ w − F ⁡ x < y ↔ F ⁡ w − F ⁡ C < y
14 9 13 imbi12d ⊢ x = C → w − x < z → F ⁡ w − F ⁡ x < y ↔ w − C < z → F ⁡ w − F ⁡ C < y
15 14 rexralbidv ⊢ x = C → ∃ z ∈ ℝ + ∀ w ∈ A w − x < z → F ⁡ w − F ⁡ x < y ↔ ∃ z ∈ ℝ + ∀ w ∈ A w − C < z → F ⁡ w − F ⁡ C < y
16 breq2 ⊢ y = R → F ⁡ w − F ⁡ C < y ↔ F ⁡ w − F ⁡ C < R
17 16 imbi2d ⊢ y = R → w − C < z → F ⁡ w − F ⁡ C < y ↔ w − C < z → F ⁡ w − F ⁡ C < R
18 17 rexralbidv ⊢ y = R → ∃ z ∈ ℝ + ∀ w ∈ A w − C < z → F ⁡ w − F ⁡ C < y ↔ ∃ z ∈ ℝ + ∀ w ∈ A w − C < z → F ⁡ w − F ⁡ C < R
19 15 18 rspc2v ⊢ C ∈ A ∧ R ∈ ℝ + → ∀ x ∈ A ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ A w − x < z → F ⁡ w − F ⁡ x < y → ∃ z ∈ ℝ + ∀ w ∈ A w − C < z → F ⁡ w − F ⁡ C < R
20 6 19 mpan9 ⊢ F : A ⟶cn B ∧ C ∈ A ∧ R ∈ ℝ + → ∃ z ∈ ℝ + ∀ w ∈ A w − C < z → F ⁡ w − F ⁡ C < R
21 20 3impb ⊢ F : A ⟶cn B ∧ C ∈ A ∧ R ∈ ℝ + → ∃ z ∈ ℝ + ∀ w ∈ A w − C < z → F ⁡ w − F ⁡ C < R