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

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cR	. . 3 class 𝑅
3	1, 2	cwlim 30998	. 2 class WLim(𝑅, 𝐴)
4		vx	. . . . . 6 setvar 𝑥
5	4	cv 1474	. . . . 5 class 𝑥
6	1, 1, 2	cinf 8230	. . . . 5 class inf(𝐴, 𝐴, 𝑅)
7	5, 6	wne 2780	. . . 4 wff 𝑥 ≠ inf(𝐴, 𝐴, 𝑅)
8	1, 2, 5	cpred 5596	. . . . . 6 class Pred(𝑅, 𝐴, 𝑥)
9	8, 1, 2	csup 8229	. . . . 5 class sup(Pred(𝑅, 𝐴, 𝑥), 𝐴, 𝑅)
10	5, 9	wceq 1475	. . . 4 wff 𝑥 = sup(Pred(𝑅, 𝐴, 𝑥), 𝐴, 𝑅)
11	7, 10	wa 383	. . 3 wff (𝑥 ≠ inf(𝐴, 𝐴, 𝑅) ∧ 𝑥 = sup(Pred(𝑅, 𝐴, 𝑥), 𝐴, 𝑅))
12	11, 4, 1	crab 2900	. 2 class {𝑥 ∈ 𝐴 ∣ (𝑥 ≠ inf(𝐴, 𝐴, 𝑅) ∧ 𝑥 = sup(Pred(𝑅, 𝐴, 𝑥), 𝐴, 𝑅))}
13	3, 12	wceq 1475	1 wff WLim(𝑅, 𝐴) = {𝑥 ∈ 𝐴 ∣ (𝑥 ≠ inf(𝐴, 𝐴, 𝑅) ∧ 𝑥 = sup(Pred(𝑅, 𝐴, 𝑥), 𝐴, 𝑅))}

This definition is referenced by:  wlimeq12  31009  nfwlim  31012  elwlim  31013  wlimss  31022