Metamath Proof Explorer

Theorem elcncf2

Description: Version of elcncf with arguments commuted. (Contributed by Mario Carneiro, 28-Apr-2014)

Ref Expression
Assertion elcncf2 ⊢ A ⊆ ℂ ∧ B ⊆ ℂ → F : A ⟶cn B ↔ F : A ⟶ B ∧ ∀ x ∈ A ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ A w − x < z → F ⁡ w − F ⁡ x < y

Proof

Step Hyp Ref Expression
1 elcncf ⊢ A ⊆ ℂ ∧ B ⊆ ℂ → F : A ⟶cn B ↔ F : A ⟶ B ∧ ∀ x ∈ A ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ A x − w < z → F ⁡ x − F ⁡ w < y
2 simplll ⊢ A ⊆ ℂ ∧ B ⊆ ℂ ∧ F : A ⟶ B ∧ x ∈ A ∧ w ∈ A → A ⊆ ℂ
3 simprl ⊢ A ⊆ ℂ ∧ B ⊆ ℂ ∧ F : A ⟶ B ∧ x ∈ A ∧ w ∈ A → x ∈ A
4 2 3 sseldd ⊢ A ⊆ ℂ ∧ B ⊆ ℂ ∧ F : A ⟶ B ∧ x ∈ A ∧ w ∈ A → x ∈ ℂ
5 simprr ⊢ A ⊆ ℂ ∧ B ⊆ ℂ ∧ F : A ⟶ B ∧ x ∈ A ∧ w ∈ A → w ∈ A
6 2 5 sseldd ⊢ A ⊆ ℂ ∧ B ⊆ ℂ ∧ F : A ⟶ B ∧ x ∈ A ∧ w ∈ A → w ∈ ℂ
7 4 6 abssubd ⊢ A ⊆ ℂ ∧ B ⊆ ℂ ∧ F : A ⟶ B ∧ x ∈ A ∧ w ∈ A → x − w = w − x
8 7 breq1d ⊢ A ⊆ ℂ ∧ B ⊆ ℂ ∧ F : A ⟶ B ∧ x ∈ A ∧ w ∈ A → x − w < z ↔ w − x < z
9 simpllr ⊢ A ⊆ ℂ ∧ B ⊆ ℂ ∧ F : A ⟶ B ∧ x ∈ A ∧ w ∈ A → B ⊆ ℂ
10 simplr ⊢ A ⊆ ℂ ∧ B ⊆ ℂ ∧ F : A ⟶ B ∧ x ∈ A ∧ w ∈ A → F : A ⟶ B
11 10 3 ffvelcdmd ⊢ A ⊆ ℂ ∧ B ⊆ ℂ ∧ F : A ⟶ B ∧ x ∈ A ∧ w ∈ A → F ⁡ x ∈ B
12 9 11 sseldd ⊢ A ⊆ ℂ ∧ B ⊆ ℂ ∧ F : A ⟶ B ∧ x ∈ A ∧ w ∈ A → F ⁡ x ∈ ℂ
13 10 5 ffvelcdmd ⊢ A ⊆ ℂ ∧ B ⊆ ℂ ∧ F : A ⟶ B ∧ x ∈ A ∧ w ∈ A → F ⁡ w ∈ B
14 9 13 sseldd ⊢ A ⊆ ℂ ∧ B ⊆ ℂ ∧ F : A ⟶ B ∧ x ∈ A ∧ w ∈ A → F ⁡ w ∈ ℂ
15 12 14 abssubd ⊢ A ⊆ ℂ ∧ B ⊆ ℂ ∧ F : A ⟶ B ∧ x ∈ A ∧ w ∈ A → F ⁡ x − F ⁡ w = F ⁡ w − F ⁡ x
16 15 breq1d ⊢ A ⊆ ℂ ∧ B ⊆ ℂ ∧ F : A ⟶ B ∧ x ∈ A ∧ w ∈ A → F ⁡ x − F ⁡ w < y ↔ F ⁡ w − F ⁡ x < y
17 8 16 imbi12d ⊢ A ⊆ ℂ ∧ B ⊆ ℂ ∧ F : A ⟶ B ∧ x ∈ A ∧ w ∈ A → x − w < z → F ⁡ x − F ⁡ w < y ↔ w − x < z → F ⁡ w − F ⁡ x < y
18 17 anassrs ⊢ A ⊆ ℂ ∧ B ⊆ ℂ ∧ F : A ⟶ B ∧ x ∈ A ∧ w ∈ A → x − w < z → F ⁡ x − F ⁡ w < y ↔ w − x < z → F ⁡ w − F ⁡ x < y
19 18 ralbidva ⊢ A ⊆ ℂ ∧ B ⊆ ℂ ∧ F : A ⟶ B ∧ x ∈ A → ∀ w ∈ A x − w < z → F ⁡ x − F ⁡ w < y ↔ ∀ w ∈ A w − x < z → F ⁡ w − F ⁡ x < y
20 19 rexbidv ⊢ A ⊆ ℂ ∧ B ⊆ ℂ ∧ F : A ⟶ B ∧ x ∈ A → ∃ z ∈ ℝ + ∀ w ∈ A x − w < z → F ⁡ x − F ⁡ w < y ↔ ∃ z ∈ ℝ + ∀ w ∈ A w − x < z → F ⁡ w − F ⁡ x < y
21 20 ralbidv ⊢ A ⊆ ℂ ∧ B ⊆ ℂ ∧ F : A ⟶ B ∧ x ∈ A → ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ A x − w < z → F ⁡ x − F ⁡ w < y ↔ ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ A w − x < z → F ⁡ w − F ⁡ x < y
22 21 ralbidva ⊢ A ⊆ ℂ ∧ B ⊆ ℂ ∧ F : A ⟶ B → ∀ x ∈ A ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ A x − w < z → F ⁡ x − F ⁡ w < y ↔ ∀ x ∈ A ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ A w − x < z → F ⁡ w − F ⁡ x < y
23 22 pm5.32da ⊢ A ⊆ ℂ ∧ B ⊆ ℂ → F : A ⟶ B ∧ ∀ x ∈ A ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ A x − w < z → F ⁡ x − F ⁡ w < y ↔ F : A ⟶ B ∧ ∀ x ∈ A ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ A w − x < z → F ⁡ w − F ⁡ x < y
24 1 23 bitrd ⊢ A ⊆ ℂ ∧ B ⊆ ℂ → F : A ⟶cn B ↔ F : A ⟶ B ∧ ∀ x ∈ A ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ A w − x < z → F ⁡ w − F ⁡ x < y