Definition df-wlimOLD 31759

Description: Define the class of limit points of a well-founded set. (Contributed by Scott Fenton, 15-Jun-2018.) Obsolete version of df-wlim 31758 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

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cR	. . 3 class 𝑅
3	1, 2	cwlimOLD 31755	. 2 class WLimOLD(𝑅, 𝐴)
4		vx	. . . . . 6 setvar 𝑥
5	4	cv 1482	. . . . 5 class 𝑥
6	2	ccnv 5113	. . . . . 6 class ◡𝑅
7	1, 1, 6	csup 8346	. . . . 5 class sup(𝐴, 𝐴, ◡𝑅)
8	5, 7	wne 2794	. . . 4 wff 𝑥 ≠ sup(𝐴, 𝐴, ◡𝑅)
9	1, 2, 5	cpred 5679	. . . . . 6 class Pred(𝑅, 𝐴, 𝑥)
10	9, 1, 2	csup 8346	. . . . 5 class sup(Pred(𝑅, 𝐴, 𝑥), 𝐴, 𝑅)
11	5, 10	wceq 1483	. . . 4 wff 𝑥 = sup(Pred(𝑅, 𝐴, 𝑥), 𝐴, 𝑅)
12	8, 11	wa 384	. . 3 wff (𝑥 ≠ sup(𝐴, 𝐴, ◡𝑅) ∧ 𝑥 = sup(Pred(𝑅, 𝐴, 𝑥), 𝐴, 𝑅))
13	12, 4, 1	crab 2916	. 2 class {𝑥 ∈ 𝐴 ∣ (𝑥 ≠ sup(𝐴, 𝐴, ◡𝑅) ∧ 𝑥 = sup(Pred(𝑅, 𝐴, 𝑥), 𝐴, 𝑅))}
14	3, 13	wceq 1483	1 wff WLimOLD(𝑅, 𝐴) = {𝑥 ∈ 𝐴 ∣ (𝑥 ≠ sup(𝐴, 𝐴, ◡𝑅) ∧ 𝑥 = sup(Pred(𝑅, 𝐴, 𝑥), 𝐴, 𝑅))}

This definition is referenced by:  elwlimOLD  31770