Metamath Proof Explorer

Theorem cncfval

Description: The value of the continuous complex function operation is the set of continuous functions from A to B . (Contributed by Paul Chapman, 11-Oct-2007) (Revised by Mario Carneiro, 9-Nov-2013)

Ref Expression
Assertion cncfval ⊢ A ⊆ ℂ ∧ B ⊆ ℂ → A ⟶cn B = f ∈ B A | ∀ x ∈ A ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ A x − w < z → f ⁡ x − f ⁡ w < y

Proof

Step Hyp Ref Expression
1 cnex ⊢ ℂ ∈ V
2 1 elpw2 ⊢ A ∈ 𝒫 ℂ ↔ A ⊆ ℂ
3 1 elpw2 ⊢ B ∈ 𝒫 ℂ ↔ B ⊆ ℂ
4 oveq2 ⊢ a = A → b a = b A
5 raleq ⊢ a = A → ∀ w ∈ a x − w < z → f ⁡ x − f ⁡ w < y ↔ ∀ w ∈ A x − w < z → f ⁡ x − f ⁡ w < y
6 5 rexbidv ⊢ a = A → ∃ z ∈ ℝ + ∀ w ∈ a x − w < z → f ⁡ x − f ⁡ w < y ↔ ∃ z ∈ ℝ + ∀ w ∈ A x − w < z → f ⁡ x − f ⁡ w < y
7 6 ralbidv ⊢ a = A → ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ a x − w < z → f ⁡ x − f ⁡ w < y ↔ ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ A x − w < z → f ⁡ x − f ⁡ w < y
8 7 raleqbi1dv ⊢ a = A → ∀ x ∈ a ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ a x − w < z → f ⁡ x − f ⁡ w < y ↔ ∀ x ∈ A ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ A x − w < z → f ⁡ x − f ⁡ w < y
9 4 8 rabeqbidv ⊢ a = A → f ∈ b a | ∀ x ∈ a ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ a x − w < z → f ⁡ x − f ⁡ w < y = f ∈ b A | ∀ x ∈ A ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ A x − w < z → f ⁡ x − f ⁡ w < y
10 oveq1 ⊢ b = B → b A = B A
11 10 rabeqdv ⊢ b = B → f ∈ b A | ∀ x ∈ A ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ A x − w < z → f ⁡ x − f ⁡ w < y = f ∈ B A | ∀ x ∈ A ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ A x − w < z → f ⁡ x − f ⁡ w < y
12 df-cncf ⊢ ⟶cn = a ∈ 𝒫 ℂ , b ∈ 𝒫 ℂ ⟼ f ∈ b a | ∀ x ∈ a ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ a x − w < z → f ⁡ x − f ⁡ w < y
13 ovex ⊢ B A ∈ V
14 13 rabex ⊢ f ∈ B A | ∀ x ∈ A ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ A x − w < z → f ⁡ x − f ⁡ w < y ∈ V
15 9 11 12 14 ovmpo ⊢ A ∈ 𝒫 ℂ ∧ B ∈ 𝒫 ℂ → A ⟶cn B = f ∈ B A | ∀ x ∈ A ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ A x − w < z → f ⁡ x − f ⁡ w < y
16 2 3 15 syl2anbr ⊢ A ⊆ ℂ ∧ B ⊆ ℂ → A ⟶cn B = f ∈ B A | ∀ x ∈ A ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ A x − w < z → f ⁡ x − f ⁡ w < y