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 ⊢ φ → ∀ z ∈ A B ∈ ℂ
rlim2.2 ⊢ φ → A ⊆ ℝ
rlim2.3 ⊢ φ → C ∈ ℂ
Assertion rlim2 ⊢ φ → z ∈ A ⟼ B ⇝ℝ C ↔ ∀ x ∈ ℝ + ∃ y ∈ ℝ ∀ z ∈ A y ≤ z → B − C < x

Proof

Step Hyp Ref Expression
1 rlim2.1 ⊢ φ → ∀ z ∈ A B ∈ ℂ
2 rlim2.2 ⊢ φ → A ⊆ ℝ
3 rlim2.3 ⊢ φ → C ∈ ℂ
4 eqid ⊢ z ∈ A ⟼ B = z ∈ A ⟼ B
5 4 fmpt ⊢ ∀ z ∈ A B ∈ ℂ ↔ z ∈ A ⟼ B : A ⟶ ℂ
6 1 5 sylib ⊢ φ → z ∈ A ⟼ B : A ⟶ ℂ
7 eqidd ⊢ φ ∧ w ∈ A → z ∈ A ⟼ B ⁡ w = z ∈ A ⟼ B ⁡ w
8 6 2 7 rlim ⊢ φ → z ∈ A ⟼ B ⇝ℝ C ↔ C ∈ ℂ ∧ ∀ x ∈ ℝ + ∃ y ∈ ℝ ∀ w ∈ A y ≤ w → z ∈ A ⟼ B ⁡ w − C < x
9 3 biantrurd ⊢ φ → ∀ x ∈ ℝ + ∃ y ∈ ℝ ∀ w ∈ A y ≤ w → z ∈ A ⟼ B ⁡ w − C < x ↔ C ∈ ℂ ∧ ∀ x ∈ ℝ + ∃ y ∈ ℝ ∀ w ∈ A y ≤ w → z ∈ A ⟼ B ⁡ w − C < x
10 nfv ⊢ Ⅎ z y ≤ w
11 nfcv ⊢ Ⅎ _ z abs
12 nffvmpt1 ⊢ Ⅎ _ z z ∈ A ⟼ B ⁡ w
13 nfcv ⊢ Ⅎ _ z −
14 nfcv ⊢ Ⅎ _ z C
15 12 13 14 nfov ⊢ Ⅎ _ z z ∈ A ⟼ B ⁡ w − C
16 11 15 nffv ⊢ Ⅎ _ z z ∈ A ⟼ B ⁡ w − C
17 nfcv ⊢ Ⅎ _ z <
18 nfcv ⊢ Ⅎ _ z x
19 16 17 18 nfbr ⊢ Ⅎ z z ∈ A ⟼ B ⁡ w − C < x
20 10 19 nfim ⊢ Ⅎ z y ≤ w → z ∈ A ⟼ B ⁡ w − C < x
21 nfv ⊢ Ⅎ w y ≤ z → z ∈ A ⟼ B ⁡ z − C < x
22 breq2 ⊢ w = z → y ≤ w ↔ y ≤ z
23 22 imbrov2fvoveq ⊢ w = z → y ≤ w → z ∈ A ⟼ B ⁡ w − C < x ↔ y ≤ z → z ∈ A ⟼ B ⁡ z − C < x
24 20 21 23 cbvralw ⊢ ∀ w ∈ A y ≤ w → z ∈ A ⟼ B ⁡ w − C < x ↔ ∀ z ∈ A y ≤ z → z ∈ A ⟼ B ⁡ z − C < x
25 4 fvmpt2 ⊢ z ∈ A ∧ B ∈ ℂ → z ∈ A ⟼ B ⁡ z = B
26 25 fvoveq1d ⊢ z ∈ A ∧ B ∈ ℂ → z ∈ A ⟼ B ⁡ z − C = B − C
27 26 breq1d ⊢ z ∈ A ∧ B ∈ ℂ → z ∈ A ⟼ B ⁡ z − C < x ↔ B − C < x
28 27 imbi2d ⊢ z ∈ A ∧ B ∈ ℂ → y ≤ z → z ∈ A ⟼ B ⁡ z − C < x ↔ y ≤ z → B − C < x
29 28 ralimiaa ⊢ ∀ z ∈ A B ∈ ℂ → ∀ z ∈ A y ≤ z → z ∈ A ⟼ B ⁡ z − C < x ↔ y ≤ z → B − C < x
30 ralbi ⊢ ∀ z ∈ A y ≤ z → z ∈ A ⟼ B ⁡ z − C < x ↔ y ≤ z → B − C < x → ∀ z ∈ A y ≤ z → z ∈ A ⟼ B ⁡ z − C < x ↔ ∀ z ∈ A y ≤ z → B − C < x
31 1 29 30 3syl ⊢ φ → ∀ z ∈ A y ≤ z → z ∈ A ⟼ B ⁡ z − C < x ↔ ∀ z ∈ A y ≤ z → B − C < x
32 24 31 syl5bb ⊢ φ → ∀ w ∈ A y ≤ w → z ∈ A ⟼ B ⁡ w − C < x ↔ ∀ z ∈ A y ≤ z → B − C < x
33 32 rexbidv ⊢ φ → ∃ y ∈ ℝ ∀ w ∈ A y ≤ w → z ∈ A ⟼ B ⁡ w − C < x ↔ ∃ y ∈ ℝ ∀ z ∈ A y ≤ z → B − C < x
34 33 ralbidv ⊢ φ → ∀ x ∈ ℝ + ∃ y ∈ ℝ ∀ w ∈ A y ≤ w → z ∈ A ⟼ B ⁡ w − C < x ↔ ∀ x ∈ ℝ + ∃ y ∈ ℝ ∀ z ∈ A y ≤ z → B − C < x
35 8 9 34 3bitr2d ⊢ φ → z ∈ A ⟼ B ⇝ℝ C ↔ ∀ x ∈ ℝ + ∃ y ∈ ℝ ∀ z ∈ A y ≤ z → B − C < x