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

Theorem rlimrel 15437
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 15433 . 2 𝑟 = {⟨𝑓, 𝑥⟩ ∣ ((𝑓 ∈ (ℂ ↑pm ℝ) ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ ∀𝑤 ∈ dom 𝑓(𝑧𝑤 → (abs‘((𝑓𝑤) − 𝑥)) < 𝑦))}
21relopabiv 5821 1 Rel ⇝𝑟
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  wcel 2107  wral 3062  wrex 3071   class class class wbr 5149  dom cdm 5677  Rel wrel 5682  cfv 6544  (class class class)co 7409  pm cpm 8821  cc 11108  cr 11109   < clt 11248  cle 11249  cmin 11444  +crp 12974  abscabs 15181  𝑟 crli 15429
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966  df-opab 5212  df-xp 5683  df-rel 5684  df-rlim 15433
This theorem is referenced by:  rlim  15439  rlimpm  15444  rlimdm  15495  caucvgrlem2  15621  caucvgr  15622  rlimdmafv  45933  rlimdmafv2  46014
  Copyright terms: Public domain W3C validator