Theorem elcncf2

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

	Ref	Expression
Assertion	elcncf2	⊢ ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) → ( 𝐹 ∈ ( 𝐴 –cn→ 𝐵 ) ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < 𝑦 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		elcncf	⊢ ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) → ( 𝐹 ∈ ( 𝐴 –cn→ 𝐵 ) ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑤 ) ) ) < 𝑦 ) ) ) )
2		simplll	⊢ ( ( ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → 𝐴 ⊆ ℂ )
3		simprl	⊢ ( ( ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → 𝑥 ∈ 𝐴 )
4	2 3	sseldd	⊢ ( ( ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → 𝑥 ∈ ℂ )
5		simprr	⊢ ( ( ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → 𝑤 ∈ 𝐴 )
6	2 5	sseldd	⊢ ( ( ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → 𝑤 ∈ ℂ )
7	4 6	abssubd	⊢ ( ( ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( abs ‘ ( 𝑥 − 𝑤 ) ) = ( abs ‘ ( 𝑤 − 𝑥 ) ) )
8	7	breq1d	⊢ ( ( ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑧 ↔ ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 ) )
9		simpllr	⊢ ( ( ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → 𝐵 ⊆ ℂ )
10		simplr	⊢ ( ( ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → 𝐹 : 𝐴 ⟶ 𝐵 )
11	10 3	ffvelrnd	⊢ ( ( ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 )
12	9 11	sseldd	⊢ ( ( ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
13	10 5	ffvelrnd	⊢ ( ( ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( 𝐹 ‘ 𝑤 ) ∈ 𝐵 )
14	9 13	sseldd	⊢ ( ( ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( 𝐹 ‘ 𝑤 ) ∈ ℂ )
15	12 14	abssubd	⊢ ( ( ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑤 ) ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) )
16	15	breq1d	⊢ ( ( ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑤 ) ) ) < 𝑦 ↔ ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < 𝑦 ) )
17	8 16	imbi12d	⊢ ( ( ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑤 ) ) ) < 𝑦 ) ↔ ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < 𝑦 ) ) )
18	17	anassrs	⊢ ( ( ( ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐴 ) → ( ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑤 ) ) ) < 𝑦 ) ↔ ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < 𝑦 ) ) )
19	18	ralbidva	⊢ ( ( ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑤 ) ) ) < 𝑦 ) ↔ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < 𝑦 ) ) )
20	19	rexbidv	⊢ ( ( ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑤 ) ) ) < 𝑦 ) ↔ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < 𝑦 ) ) )
21	20	ralbidv	⊢ ( ( ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑤 ) ) ) < 𝑦 ) ↔ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < 𝑦 ) ) )
22	21	ralbidva	⊢ ( ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑤 ) ) ) < 𝑦 ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < 𝑦 ) ) )
23	22	pm5.32da	⊢ ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) → ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑤 ) ) ) < 𝑦 ) ) ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < 𝑦 ) ) ) )
24	1 23	bitrd	⊢ ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) → ( 𝐹 ∈ ( 𝐴 –cn→ 𝐵 ) ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < 𝑦 ) ) ) )