Mathbox for Scott Fenton < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-wlim Structured version   Visualization version   GIF version

Definition df-wlim 31002
 Description: Define the class of limit points of a well-founded set. (Contributed by Scott Fenton, 15-Jun-2018.) (Revised by AV, 10-Oct-2021.)
Assertion
Ref Expression
df-wlim WLim(𝑅, 𝐴) = {𝑥𝐴 ∣ (𝑥 ≠ inf(𝐴, 𝐴, 𝑅) ∧ 𝑥 = sup(Pred(𝑅, 𝐴, 𝑥), 𝐴, 𝑅))}
Distinct variable groups:   𝑥,𝑅   𝑥,𝐴

Detailed syntax breakdown of Definition df-wlim
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cR . . 3 class 𝑅
31, 2cwlim 30998 . 2 class WLim(𝑅, 𝐴)
4 vx . . . . . 6 setvar 𝑥
54cv 1474 . . . . 5 class 𝑥
61, 1, 2cinf 8230 . . . . 5 class inf(𝐴, 𝐴, 𝑅)
75, 6wne 2780 . . . 4 wff 𝑥 ≠ inf(𝐴, 𝐴, 𝑅)
81, 2, 5cpred 5596 . . . . . 6 class Pred(𝑅, 𝐴, 𝑥)
98, 1, 2csup 8229 . . . . 5 class sup(Pred(𝑅, 𝐴, 𝑥), 𝐴, 𝑅)
105, 9wceq 1475 . . . 4 wff 𝑥 = sup(Pred(𝑅, 𝐴, 𝑥), 𝐴, 𝑅)
117, 10wa 383 . . 3 wff (𝑥 ≠ inf(𝐴, 𝐴, 𝑅) ∧ 𝑥 = sup(Pred(𝑅, 𝐴, 𝑥), 𝐴, 𝑅))
1211, 4, 1crab 2900 . 2 class {𝑥𝐴 ∣ (𝑥 ≠ inf(𝐴, 𝐴, 𝑅) ∧ 𝑥 = sup(Pred(𝑅, 𝐴, 𝑥), 𝐴, 𝑅))}
133, 12wceq 1475 1 wff WLim(𝑅, 𝐴) = {𝑥𝐴 ∣ (𝑥 ≠ inf(𝐴, 𝐴, 𝑅) ∧ 𝑥 = sup(Pred(𝑅, 𝐴, 𝑥), 𝐴, 𝑅))}
 Colors of variables: wff setvar class This definition is referenced by:  wlimeq12  31009  nfwlim  31012  elwlim  31013  wlimss  31022
 Copyright terms: Public domain W3C validator