Metamath Proof Explorer

Theorem elcnfn

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

Ref Expression
Assertion elcnfn ⊢ T ∈ ContFn ↔ T : ℋ ⟶ ℂ ∧ ∀ x ∈ ℋ ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ ℋ norm ℎ ⁡ w - ℎ x < z → T ⁡ w − T ⁡ x < y

Proof

Step Hyp Ref Expression
1 fveq1 ⊢ t = T → t ⁡ w = T ⁡ w
2 fveq1 ⊢ t = T → t ⁡ x = T ⁡ x
3 1 2 oveq12d ⊢ t = T → t ⁡ w − t ⁡ x = T ⁡ w − T ⁡ x
4 3 fveq2d ⊢ t = T → t ⁡ w − t ⁡ x = T ⁡ w − T ⁡ x
5 4 breq1d ⊢ t = T → t ⁡ w − t ⁡ x < y ↔ T ⁡ w − T ⁡ x < y
6 5 imbi2d ⊢ t = T → norm ℎ ⁡ w - ℎ x < z → t ⁡ w − t ⁡ x < y ↔ norm ℎ ⁡ w - ℎ x < z → T ⁡ w − T ⁡ x < y
7 6 rexralbidv ⊢ t = T → ∃ z ∈ ℝ + ∀ w ∈ ℋ norm ℎ ⁡ w - ℎ x < z → t ⁡ w − t ⁡ x < y ↔ ∃ z ∈ ℝ + ∀ w ∈ ℋ norm ℎ ⁡ w - ℎ x < z → T ⁡ w − T ⁡ x < y
8 7 2ralbidv ⊢ t = T → ∀ x ∈ ℋ ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ ℋ norm ℎ ⁡ w - ℎ x < z → t ⁡ w − t ⁡ x < y ↔ ∀ x ∈ ℋ ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ ℋ norm ℎ ⁡ w - ℎ x < z → T ⁡ w − T ⁡ x < y
9 df-cnfn ⊢ ContFn = t ∈ ℂ ℋ | ∀ x ∈ ℋ ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ ℋ norm ℎ ⁡ w - ℎ x < z → t ⁡ w − t ⁡ x < y
10 8 9 elrab2 ⊢ T ∈ ContFn ↔ T ∈ ℂ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ ℋ norm ℎ ⁡ w - ℎ x < z → T ⁡ w − T ⁡ x < y
11 cnex ⊢ ℂ ∈ V
12 ax-hilex ⊢ ℋ ∈ V
13 11 12 elmap ⊢ T ∈ ℂ ℋ ↔ T : ℋ ⟶ ℂ
14 13 anbi1i ⊢ T ∈ ℂ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ ℋ norm ℎ ⁡ w - ℎ x < z → T ⁡ w − T ⁡ x < y ↔ T : ℋ ⟶ ℂ ∧ ∀ x ∈ ℋ ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ ℋ norm ℎ ⁡ w - ℎ x < z → T ⁡ w − T ⁡ x < y
15 10 14 bitri ⊢ T ∈ ContFn ↔ T : ℋ ⟶ ℂ ∧ ∀ x ∈ ℋ ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ ℋ norm ℎ ⁡ w - ℎ x < z → T ⁡ w − T ⁡ x < y