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

Theorem rlimrel 14600
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 14596 . 2 𝑟 = {⟨𝑓, 𝑥⟩ ∣ ((𝑓 ∈ (ℂ ↑pm ℝ) ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ ∀𝑤 ∈ dom 𝑓(𝑧𝑤 → (abs‘((𝑓𝑤) − 𝑥)) < 𝑦))}
21relopabi 5477 1 Rel ⇝𝑟
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 386  wcel 2166  wral 3116  wrex 3117   class class class wbr 4872  dom cdm 5341  Rel wrel 5346  cfv 6122  (class class class)co 6904  pm cpm 8122  cc 10249  cr 10250   < clt 10390  cle 10391  cmin 10584  +crp 12111  abscabs 14350  𝑟 crli 14592
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2390  ax-ext 2802
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2811  df-cleq 2817  df-clel 2820  df-nfc 2957  df-rab 3125  df-v 3415  df-dif 3800  df-un 3802  df-in 3804  df-ss 3811  df-nul 4144  df-if 4306  df-sn 4397  df-pr 4399  df-op 4403  df-opab 4935  df-xp 5347  df-rel 5348  df-rlim 14596
This theorem is referenced by:  rlim  14602  rlimpm  14607  rlimdm  14658  caucvgrlem2  14781  caucvgr  14782  rlimdmafv  42078  rlimdmafv2  42159
  Copyright terms: Public domain W3C validator