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

Proof

Step Hyp Ref Expression
1 rlim2.1 ⊢φ→∀z∈AB∈ℂ
2 rlim2.2 ⊢φ→A⊆ℝ
3 rlim2.3 ⊢φ→C∈ℂ
4 eqid ⊢z∈A⟼B=z∈A⟼B
5 4 fmpt ⊢∀z∈AB∈ℂ↔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∈Ay≤w→z∈A⟼B⁡w−C<x
9 3 biantrurd ⊢φ→∀x∈ℝ+∃y∈ℝ∀w∈Ay≤w→z∈A⟼B⁡w−C<x↔C∈ℂ∧∀x∈ℝ+∃y∈ℝ∀w∈Ay≤w→z∈A⟼B⁡w−C<x
10 nfv ⊢Ⅎzy≤w
11 nfcv ⊢Ⅎ_zabs
12 nffvmpt1 ⊢Ⅎ_zz∈A⟼B⁡w
13 nfcv ⊢Ⅎ_z−
14 nfcv ⊢Ⅎ_zC
15 12 13 14 nfov ⊢Ⅎ_zz∈A⟼B⁡w−C
16 11 15 nffv ⊢Ⅎ_zz∈A⟼B⁡w−C
17 nfcv ⊢Ⅎ_z<
18 nfcv ⊢Ⅎ_zx
19 16 17 18 nfbr ⊢Ⅎzz∈A⟼B⁡w−C<x
20 10 19 nfim ⊢Ⅎzy≤w→z∈A⟼B⁡w−C<x
21 nfv ⊢Ⅎwy≤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∈Ay≤w→z∈A⟼B⁡w−C<x↔∀z∈Ay≤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∈AB∈ℂ→∀z∈Ay≤z→z∈A⟼B⁡z−C<x↔y≤z→B−C<x
30 ralbi ⊢∀z∈Ay≤z→z∈A⟼B⁡z−C<x↔y≤z→B−C<x→∀z∈Ay≤z→z∈A⟼B⁡z−C<x↔∀z∈Ay≤z→B−C<x
31 1 29 30 3syl ⊢φ→∀z∈Ay≤z→z∈A⟼B⁡z−C<x↔∀z∈Ay≤z→B−C<x
32 24 31 bitrid ⊢φ→∀w∈Ay≤w→z∈A⟼B⁡w−C<x↔∀z∈Ay≤z→B−C<x
33 32 rexbidv ⊢φ→∃y∈ℝ∀w∈Ay≤w→z∈A⟼B⁡w−C<x↔∃y∈ℝ∀z∈Ay≤z→B−C<x
34 33 ralbidv ⊢φ→∀x∈ℝ+∃y∈ℝ∀w∈Ay≤w→z∈A⟼B⁡w−C<x↔∀x∈ℝ+∃y∈ℝ∀z∈Ay≤z→B−C<x
35 8 9 34 3bitr2d ⊢φ→z∈A⟼B⇝ℝC↔∀x∈ℝ+∃y∈ℝ∀z∈Ay≤z→B−C<x