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

Metamath Proof Explorer

Theorem rlim2

Description: Rewrite rlim for a mapping operation. (Contributed by Mario Carneiro, 16-Sep-2014) (Revised by Mario Carneiro, 28-Feb-2015)

Ref Expression
Hypotheses rlim2.1 ⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝐴 𝐵 ∈ ℂ )
rlim2.2 ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
rlim2.3 ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
Assertion rlim2 ( 𝜑 → ( ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 𝐶 ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 rlim2.1 ⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝐴 𝐵 ∈ ℂ )
2 rlim2.2 ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
3 rlim2.3 ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
4 eqid ⊢ ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑧 ∈ 𝐴 ↦ 𝐵 )
5 4 fmpt ⊢ ( ∀ 𝑧 ∈ 𝐴 𝐵 ∈ ℂ ↔ ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ℂ )
6 1 5 sylib ⊢ ( 𝜑 → ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ℂ )
7 eqidd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑤 ) = ( ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑤 ) )
8 6 2 7 rlim ⊢ ( 𝜑 → ( ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 𝐶 ↔ ( 𝐶 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ ∀ 𝑤 ∈ 𝐴 ( 𝑦 ≤ 𝑤 → ( abs ‘ ( ( ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑤 ) − 𝐶 ) ) < 𝑥 ) ) ) )
9 3 biantrurd ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ ∀ 𝑤 ∈ 𝐴 ( 𝑦 ≤ 𝑤 → ( abs ‘ ( ( ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑤 ) − 𝐶 ) ) < 𝑥 ) ↔ ( 𝐶 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ ∀ 𝑤 ∈ 𝐴 ( 𝑦 ≤ 𝑤 → ( abs ‘ ( ( ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑤 ) − 𝐶 ) ) < 𝑥 ) ) ) )
10 nfv ⊢ Ⅎ 𝑧 𝑦 ≤ 𝑤
11 nfcv ⊢ Ⅎ 𝑧 abs
12 nffvmpt1 ⊢ Ⅎ 𝑧 ( ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑤 )
13 nfcv ⊢ Ⅎ 𝑧 −
14 nfcv ⊢ Ⅎ 𝑧 𝐶
15 12 13 14 nfov ⊢ Ⅎ 𝑧 ( ( ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑤 ) − 𝐶 )
16 11 15 nffv ⊢ Ⅎ 𝑧 ( abs ‘ ( ( ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑤 ) − 𝐶 ) )
17 nfcv ⊢ Ⅎ 𝑧 <
18 nfcv ⊢ Ⅎ 𝑧 𝑥
19 16 17 18 nfbr ⊢ Ⅎ 𝑧 ( abs ‘ ( ( ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑤 ) − 𝐶 ) ) < 𝑥
20 10 19 nfim ⊢ Ⅎ 𝑧 ( 𝑦 ≤ 𝑤 → ( abs ‘ ( ( ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑤 ) − 𝐶 ) ) < 𝑥 )
21 nfv ⊢ Ⅎ 𝑤 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 )
22 breq2 ⊢ ( 𝑤 = 𝑧 → ( 𝑦 ≤ 𝑤 ↔ 𝑦 ≤ 𝑧 ) )
23 22 imbrov2fvoveq ⊢ ( 𝑤 = 𝑧 → ( ( 𝑦 ≤ 𝑤 → ( abs ‘ ( ( ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑤 ) − 𝐶 ) ) < 𝑥 ) ↔ ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ) ) )
24 20 21 23 cbvralw ⊢ ( ∀ 𝑤 ∈ 𝐴 ( 𝑦 ≤ 𝑤 → ( abs ‘ ( ( ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑤 ) − 𝐶 ) ) < 𝑥 ) ↔ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ) )
25 4 fvmpt2 ⊢ ( ( 𝑧 ∈ 𝐴 ∧ 𝐵 ∈ ℂ ) → ( ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) = 𝐵 )
26 25 fvoveq1d ⊢ ( ( 𝑧 ∈ 𝐴 ∧ 𝐵 ∈ ℂ ) → ( abs ‘ ( ( ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) − 𝐶 ) ) = ( abs ‘ ( 𝐵 − 𝐶 ) ) )
27 26 breq1d ⊢ ( ( 𝑧 ∈ 𝐴 ∧ 𝐵 ∈ ℂ ) → ( ( abs ‘ ( ( ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ↔ ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) )
28 27 imbi2d ⊢ ( ( 𝑧 ∈ 𝐴 ∧ 𝐵 ∈ ℂ ) → ( ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ) ↔ ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ) )
29 28 ralimiaa ⊢ ( ∀ 𝑧 ∈ 𝐴 𝐵 ∈ ℂ → ∀ 𝑧 ∈ 𝐴 ( ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ) ↔ ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ) )
30 ralbi ⊢ ( ∀ 𝑧 ∈ 𝐴 ( ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ) ↔ ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ) → ( ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ) ↔ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ) )
31 1 29 30 3syl ⊢ ( 𝜑 → ( ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ) ↔ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ) )
32 24 31 bitrid ⊢ ( 𝜑 → ( ∀ 𝑤 ∈ 𝐴 ( 𝑦 ≤ 𝑤 → ( abs ‘ ( ( ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑤 ) − 𝐶 ) ) < 𝑥 ) ↔ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ) )
33 32 rexbidv ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑤 ∈ 𝐴 ( 𝑦 ≤ 𝑤 → ( abs ‘ ( ( ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑤 ) − 𝐶 ) ) < 𝑥 ) ↔ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ) )
34 33 ralbidv ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ ∀ 𝑤 ∈ 𝐴 ( 𝑦 ≤ 𝑤 → ( abs ‘ ( ( ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑤 ) − 𝐶 ) ) < 𝑥 ) ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ) )
35 8 9 34 3bitr2d ⊢ ( 𝜑 → ( ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 𝐶 ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ) )