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

Theorem rlimrel 15532
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 15528 . 2 𝑟 = {⟨𝑓, 𝑥⟩ ∣ ((𝑓 ∈ (ℂ ↑pm ℝ) ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ ∀𝑤 ∈ dom 𝑓(𝑧𝑤 → (abs‘((𝑓𝑤) − 𝑥)) < 𝑦))}
21relopabiv 5797 1 Rel ⇝𝑟
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 400  wcel 2145  wral 3079  wrex 3089   class class class wbr 5104  dom cdm 5651  Rel wrel 5656  cfv 6525  (class class class)co 7400  pm cpm 8813  cc 11086  cr 11087   < clt 11231  cle 11232  cmin 11429  +crp 13004  abscabs 15273  𝑟 crli 15524
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737
This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-ss 3924  df-opab 5167  df-xp 5657  df-rel 5658  df-rlim 15528
This theorem is referenced by:  rlim  15534  rlimpm  15539  rlimdm  15590  caucvgrlem2  15714  caucvgr  15715  rlimdmafv  47770  rlimdmafv2  47851
  Copyright terms: Public domain W3C validator