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⟶cnB↔F:A⟶B∧∀x∈A∀y∈ℝ+∃z∈ℝ+∀w∈Aw−x<z→F⁡w−F⁡x<y

Proof

Step Hyp Ref Expression
1 elcncf ⊢A⊆ℂ∧B⊆ℂ→F:A⟶cnB↔F:A⟶B∧∀x∈A∀y∈ℝ+∃z∈ℝ+∀w∈Ax−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∈Ax−w<z→F⁡x−F⁡w<y↔∀w∈Aw−x<z→F⁡w−F⁡x<y
20 19 rexbidv ⊢A⊆ℂ∧B⊆ℂ∧F:A⟶B∧x∈A→∃z∈ℝ+∀w∈Ax−w<z→F⁡x−F⁡w<y↔∃z∈ℝ+∀w∈Aw−x<z→F⁡w−F⁡x<y
21 20 ralbidv ⊢A⊆ℂ∧B⊆ℂ∧F:A⟶B∧x∈A→∀y∈ℝ+∃z∈ℝ+∀w∈Ax−w<z→F⁡x−F⁡w<y↔∀y∈ℝ+∃z∈ℝ+∀w∈Aw−x<z→F⁡w−F⁡x<y
22 21 ralbidva ⊢A⊆ℂ∧B⊆ℂ∧F:A⟶B→∀x∈A∀y∈ℝ+∃z∈ℝ+∀w∈Ax−w<z→F⁡x−F⁡w<y↔∀x∈A∀y∈ℝ+∃z∈ℝ+∀w∈Aw−x<z→F⁡w−F⁡x<y
23 22 pm5.32da ⊢A⊆ℂ∧B⊆ℂ→F:A⟶B∧∀x∈A∀y∈ℝ+∃z∈ℝ+∀w∈Ax−w<z→F⁡x−F⁡w<y↔F:A⟶B∧∀x∈A∀y∈ℝ+∃z∈ℝ+∀w∈Aw−x<z→F⁡w−F⁡x<y
24 1 23 bitrd ⊢A⊆ℂ∧B⊆ℂ→F:A⟶cnB↔F:A⟶B∧∀x∈A∀y∈ℝ+∃z∈ℝ+∀w∈Aw−x<z→F⁡w−F⁡x<y