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	syl5bb	⊢ ( 𝜑 → ( ∀ 𝑤 ∈ 𝐴 ( 𝑦 ≤ 𝑤 → ( abs ‘ ( ( ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑤 ) − 𝐶 ) ) < 𝑥 ) ↔ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ) )
33	32	rexbidv	⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑤 ∈ 𝐴 ( 𝑦 ≤ 𝑤 → ( abs ‘ ( ( ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑤 ) − 𝐶 ) ) < 𝑥 ) ↔ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ) )
34	33	ralbidv	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑦 ∈ ℝ ∀ 𝑤 ∈ 𝐴 ( 𝑦 ≤ 𝑤 → ( abs ‘ ( ( ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑤 ) − 𝐶 ) ) < 𝑥 ) ↔ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ) )
35	8 9 34	3bitr2d	⊢ ( 𝜑 → ( ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ⇝_𝑟 𝐶 ↔ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ) )

Metamath Proof Explorer

Theorem rlim2

Proof