MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rlimrel Structured version   Visualization version   GIF version

Theorem rlimrel 15067
Description: The limit relation is a relation. (Contributed by Mario Carneiro, 24-Sep-2014.)
Assertion
Ref Expression
rlimrel Rel ⇝𝑟

Proof of Theorem rlimrel
Dummy variables 𝑤 𝑥 𝑦 𝑧 𝑓 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-rlim 15063 . 2 𝑟 = {⟨𝑓, 𝑥⟩ ∣ ((𝑓 ∈ (ℂ ↑pm ℝ) ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ ∀𝑤 ∈ dom 𝑓(𝑧𝑤 → (abs‘((𝑓𝑤) − 𝑥)) < 𝑦))}
21relopabiv 5699 1 Rel ⇝𝑟
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  wcel 2111  wral 3062  wrex 3063   class class class wbr 5062  dom cdm 5560  Rel wrel 5565  cfv 6389  (class class class)co 7222  pm cpm 8518  cc 10740  cr 10741   < clt 10880  cle 10881  cmin 11075  +crp 12599  abscabs 14810  𝑟 crli 15059
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2113  ax-9 2121  ax-ext 2709
This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2072  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3417  df-in 3882  df-ss 3892  df-opab 5125  df-xp 5566  df-rel 5567  df-rlim 15063
This theorem is referenced by:  rlim  15069  rlimpm  15074  rlimdm  15125  caucvgrlem2  15251  caucvgr  15252  rlimdmafv  44356  rlimdmafv2  44437
  Copyright terms: Public domain W3C validator