Definition df-wlim 36752

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 36750	. 2 class WLim(𝑅, 𝐴)
4		vx	. . . . . 6 setvar 𝑥
5	4	cv 1569	. . . . 5 class 𝑥
6	1, 1, 2	cinf 9457	. . . . 5 class inf(𝐴, 𝐴, 𝑅)
7	5, 6	wne 2959	. . . 4 wff 𝑥 ≠ inf(𝐴, 𝐴, 𝑅)
8	1, 2, 5	cpred 6318	. . . . . 6 class Pred(𝑅, 𝐴, 𝑥)
9	8, 1, 2	csup 9456	. . . . 5 class sup(Pred(𝑅, 𝐴, 𝑥), 𝐴, 𝑅)
10	5, 9	wceq 1570	. . . 4 wff 𝑥 = sup(Pred(𝑅, 𝐴, 𝑥), 𝐴, 𝑅)
11	7, 10	wa 401	. . 3 wff (𝑥 ≠ inf(𝐴, 𝐴, 𝑅) ∧ 𝑥 = sup(Pred(𝑅, 𝐴, 𝑥), 𝐴, 𝑅))
12	11, 4, 1	crab 3416	. 2 class {𝑥 ∈ 𝐴 ∣ (𝑥 ≠ inf(𝐴, 𝐴, 𝑅) ∧ 𝑥 = sup(Pred(𝑅, 𝐴, 𝑥), 𝐴, 𝑅))}
13	3, 12	wceq 1570	1 wff WLim(𝑅, 𝐴) = {𝑥 ∈ 𝐴 ∣ (𝑥 ≠ inf(𝐴, 𝐴, 𝑅) ∧ 𝑥 = sup(Pred(𝑅, 𝐴, 𝑥), 𝐴, 𝑅))}

This definition is used by:  wlimeq12  36758  nfwlim  36761  elwlim  36762  wlimss  36768