This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ffvelcdmd ⊢ ( ( ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 )
12 9 11 sseldd ⊢ ( ( ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
13 10 5 ffvelcdmd ⊢ ( ( ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( 𝐹 ‘ 𝑤 ) ∈ 𝐵 )
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 ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < 𝑦 ) ) ) )