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

Definition df-wlimOLD 31733
Description: Define the class of limit points of a well-founded set. (Contributed by Scott Fenton, 15-Jun-2018.) Obsolete version of df-wlim 31732 as of 10-Oct-2021. (New usage is discouraged.)
Assertion
Ref Expression
df-wlimOLD WLimOLD(𝑅, 𝐴) = {𝑥𝐴 ∣ (𝑥 ≠ sup(𝐴, 𝐴, 𝑅) ∧ 𝑥 = sup(Pred(𝑅, 𝐴, 𝑥), 𝐴, 𝑅))}
Distinct variable groups:   𝑥,𝑅   𝑥,𝐴

Detailed syntax breakdown of Definition df-wlimOLD
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cR . . 3 class 𝑅
31, 2cwlimOLD 31729 . 2 class WLimOLD(𝑅, 𝐴)
4 vx . . . . . 6 setvar 𝑥
54cv 1480 . . . . 5 class 𝑥
62ccnv 5103 . . . . . 6 class 𝑅
71, 1, 6csup 8331 . . . . 5 class sup(𝐴, 𝐴, 𝑅)
85, 7wne 2791 . . . 4 wff 𝑥 ≠ sup(𝐴, 𝐴, 𝑅)
91, 2, 5cpred 5667 . . . . . 6 class Pred(𝑅, 𝐴, 𝑥)
109, 1, 2csup 8331 . . . . 5 class sup(Pred(𝑅, 𝐴, 𝑥), 𝐴, 𝑅)
115, 10wceq 1481 . . . 4 wff 𝑥 = sup(Pred(𝑅, 𝐴, 𝑥), 𝐴, 𝑅)
128, 11wa 384 . . 3 wff (𝑥 ≠ sup(𝐴, 𝐴, 𝑅) ∧ 𝑥 = sup(Pred(𝑅, 𝐴, 𝑥), 𝐴, 𝑅))
1312, 4, 1crab 2913 . 2 class {𝑥𝐴 ∣ (𝑥 ≠ sup(𝐴, 𝐴, 𝑅) ∧ 𝑥 = sup(Pred(𝑅, 𝐴, 𝑥), 𝐴, 𝑅))}
143, 13wceq 1481 1 wff WLimOLD(𝑅, 𝐴) = {𝑥𝐴 ∣ (𝑥 ≠ sup(𝐴, 𝐴, 𝑅) ∧ 𝑥 = sup(Pred(𝑅, 𝐴, 𝑥), 𝐴, 𝑅))}
Colors of variables: wff setvar class
This definition is referenced by:  elwlimOLD  31744
  Copyright terms: Public domain W3C validator