Definition df-rlim

Description: Define the limit relation for partial functions on the reals. See rlim for its relational expression. (Contributed by Mario Carneiro, 16-Sep-2014)

	Ref	Expression
Assertion	df-rlim	⊢ ⇝𝑟 = { ⟨ 𝑓 , 𝑥 ⟩ ∣ ( ( 𝑓 ∈ ( ℂ ↑pm ℝ ) ∧ 𝑥 ∈ ℂ ) ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ ∀ 𝑤 ∈ dom 𝑓 ( 𝑧 ≤ 𝑤 → ( abs ‘ ( ( 𝑓 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crli	⊢ ⇝𝑟
1		vf	⊢ 𝑓
2		vx	⊢ 𝑥
3	1	cv	⊢ 𝑓
4		cc	⊢ ℂ
5		cpm	⊢ ↑pm
6		cr	⊢ ℝ
7	4 6 5	co	⊢ ( ℂ ↑pm ℝ )
8	3 7	wcel	⊢ 𝑓 ∈ ( ℂ ↑pm ℝ )
9	2	cv	⊢ 𝑥
10	9 4	wcel	⊢ 𝑥 ∈ ℂ
11	8 10	wa	⊢ ( 𝑓 ∈ ( ℂ ↑pm ℝ ) ∧ 𝑥 ∈ ℂ )
12		vy	⊢ 𝑦
13		crp	⊢ ℝ+
14		vz	⊢ 𝑧
15		vw	⊢ 𝑤
16	3	cdm	⊢ dom 𝑓
17	14	cv	⊢ 𝑧
18		cle	⊢ ≤
19	15	cv	⊢ 𝑤
20	17 19 18	wbr	⊢ 𝑧 ≤ 𝑤
21		cabs	⊢ abs
22	19 3	cfv	⊢ ( 𝑓 ‘ 𝑤 )
23		cmin	⊢ −
24	22 9 23	co	⊢ ( ( 𝑓 ‘ 𝑤 ) − 𝑥 )
25	24 21	cfv	⊢ ( abs ‘ ( ( 𝑓 ‘ 𝑤 ) − 𝑥 ) )
26		clt	⊢ <
27	12	cv	⊢ 𝑦
28	25 27 26	wbr	⊢ ( abs ‘ ( ( 𝑓 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦
29	20 28	wi	⊢ ( 𝑧 ≤ 𝑤 → ( abs ‘ ( ( 𝑓 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 )
30	29 15 16	wral	⊢ ∀ 𝑤 ∈ dom 𝑓 ( 𝑧 ≤ 𝑤 → ( abs ‘ ( ( 𝑓 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 )
31	30 14 6	wrex	⊢ ∃ 𝑧 ∈ ℝ ∀ 𝑤 ∈ dom 𝑓 ( 𝑧 ≤ 𝑤 → ( abs ‘ ( ( 𝑓 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 )
32	31 12 13	wral	⊢ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ ∀ 𝑤 ∈ dom 𝑓 ( 𝑧 ≤ 𝑤 → ( abs ‘ ( ( 𝑓 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 )
33	11 32	wa	⊢ ( ( 𝑓 ∈ ( ℂ ↑pm ℝ ) ∧ 𝑥 ∈ ℂ ) ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ ∀ 𝑤 ∈ dom 𝑓 ( 𝑧 ≤ 𝑤 → ( abs ‘ ( ( 𝑓 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) )
34	33 1 2	copab	⊢ { ⟨ 𝑓 , 𝑥 ⟩ ∣ ( ( 𝑓 ∈ ( ℂ ↑pm ℝ ) ∧ 𝑥 ∈ ℂ ) ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ ∀ 𝑤 ∈ dom 𝑓 ( 𝑧 ≤ 𝑤 → ( abs ‘ ( ( 𝑓 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) }
35	0 34	wceq	⊢ ⇝𝑟 = { ⟨ 𝑓 , 𝑥 ⟩ ∣ ( ( 𝑓 ∈ ( ℂ ↑pm ℝ ) ∧ 𝑥 ∈ ℂ ) ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ ∀ 𝑤 ∈ dom 𝑓 ( 𝑧 ≤ 𝑤 → ( abs ‘ ( ( 𝑓 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) }