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

Metamath Proof Explorer

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 ‘ ( ( 𝑓 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) }