Metamath Proof Explorer

Theorem cnfnc

Description: Basic continuity property of a continuous functional. (Contributed by NM, 11-Feb-2006) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

Ref Expression
Assertion cnfnc ⊢ T ∈ ContFn ∧ A ∈ ℋ ∧ B ∈ ℝ + → ∃ x ∈ ℝ + ∀ y ∈ ℋ norm ℎ ⁡ y - ℎ A < x → T ⁡ y − T ⁡ A < B

Proof

Step Hyp Ref Expression
1 elcnfn ⊢ T ∈ ContFn ↔ T : ℋ ⟶ ℂ ∧ ∀ z ∈ ℋ ∀ w ∈ ℝ + ∃ x ∈ ℝ + ∀ y ∈ ℋ norm ℎ ⁡ y - ℎ z < x → T ⁡ y − T ⁡ z < w
2 1 simprbi ⊢ T ∈ ContFn → ∀ z ∈ ℋ ∀ w ∈ ℝ + ∃ x ∈ ℝ + ∀ y ∈ ℋ norm ℎ ⁡ y - ℎ z < x → T ⁡ y − T ⁡ z < w
3 oveq2 ⊢ z = A → y - ℎ z = y - ℎ A
4 3 fveq2d ⊢ z = A → norm ℎ ⁡ y - ℎ z = norm ℎ ⁡ y - ℎ A
5 4 breq1d ⊢ z = A → norm ℎ ⁡ y - ℎ z < x ↔ norm ℎ ⁡ y - ℎ A < x
6 fveq2 ⊢ z = A → T ⁡ z = T ⁡ A
7 6 oveq2d ⊢ z = A → T ⁡ y − T ⁡ z = T ⁡ y − T ⁡ A
8 7 fveq2d ⊢ z = A → T ⁡ y − T ⁡ z = T ⁡ y − T ⁡ A
9 8 breq1d ⊢ z = A → T ⁡ y − T ⁡ z < w ↔ T ⁡ y − T ⁡ A < w
10 5 9 imbi12d ⊢ z = A → norm ℎ ⁡ y - ℎ z < x → T ⁡ y − T ⁡ z < w ↔ norm ℎ ⁡ y - ℎ A < x → T ⁡ y − T ⁡ A < w
11 10 rexralbidv ⊢ z = A → ∃ x ∈ ℝ + ∀ y ∈ ℋ norm ℎ ⁡ y - ℎ z < x → T ⁡ y − T ⁡ z < w ↔ ∃ x ∈ ℝ + ∀ y ∈ ℋ norm ℎ ⁡ y - ℎ A < x → T ⁡ y − T ⁡ A < w
12 breq2 ⊢ w = B → T ⁡ y − T ⁡ A < w ↔ T ⁡ y − T ⁡ A < B
13 12 imbi2d ⊢ w = B → norm ℎ ⁡ y - ℎ A < x → T ⁡ y − T ⁡ A < w ↔ norm ℎ ⁡ y - ℎ A < x → T ⁡ y − T ⁡ A < B
14 13 rexralbidv ⊢ w = B → ∃ x ∈ ℝ + ∀ y ∈ ℋ norm ℎ ⁡ y - ℎ A < x → T ⁡ y − T ⁡ A < w ↔ ∃ x ∈ ℝ + ∀ y ∈ ℋ norm ℎ ⁡ y - ℎ A < x → T ⁡ y − T ⁡ A < B
15 11 14 rspc2v ⊢ A ∈ ℋ ∧ B ∈ ℝ + → ∀ z ∈ ℋ ∀ w ∈ ℝ + ∃ x ∈ ℝ + ∀ y ∈ ℋ norm ℎ ⁡ y - ℎ z < x → T ⁡ y − T ⁡ z < w → ∃ x ∈ ℝ + ∀ y ∈ ℋ norm ℎ ⁡ y - ℎ A < x → T ⁡ y − T ⁡ A < B
16 2 15 syl5com ⊢ T ∈ ContFn → A ∈ ℋ ∧ B ∈ ℝ + → ∃ x ∈ ℝ + ∀ y ∈ ℋ norm ℎ ⁡ y - ℎ A < x → T ⁡ y − T ⁡ A < B
17 16 3impib ⊢ T ∈ ContFn ∧ A ∈ ℋ ∧ B ∈ ℝ + → ∃ x ∈ ℝ + ∀ y ∈ ℋ norm ℎ ⁡ y - ℎ A < x → T ⁡ y − T ⁡ A < B