Definition df-wlim 33100

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 33098	. 2 class WLim(𝑅, 𝐴)
4		vx	. . . . . 6 setvar 𝑥
5	4	cv 1532	. . . . 5 class 𝑥
6	1, 1, 2	cinf 8904	. . . . 5 class inf(𝐴, 𝐴, 𝑅)
7	5, 6	wne 3016	. . . 4 wff 𝑥 ≠ inf(𝐴, 𝐴, 𝑅)
8	1, 2, 5	cpred 6146	. . . . . 6 class Pred(𝑅, 𝐴, 𝑥)
9	8, 1, 2	csup 8903	. . . . 5 class sup(Pred(𝑅, 𝐴, 𝑥), 𝐴, 𝑅)
10	5, 9	wceq 1533	. . . 4 wff 𝑥 = sup(Pred(𝑅, 𝐴, 𝑥), 𝐴, 𝑅)
11	7, 10	wa 398	. . 3 wff (𝑥 ≠ inf(𝐴, 𝐴, 𝑅) ∧ 𝑥 = sup(Pred(𝑅, 𝐴, 𝑥), 𝐴, 𝑅))
12	11, 4, 1	crab 3142	. 2 class {𝑥 ∈ 𝐴 ∣ (𝑥 ≠ inf(𝐴, 𝐴, 𝑅) ∧ 𝑥 = sup(Pred(𝑅, 𝐴, 𝑥), 𝐴, 𝑅))}
13	3, 12	wceq 1533	1 wff WLim(𝑅, 𝐴) = {𝑥 ∈ 𝐴 ∣ (𝑥 ≠ inf(𝐴, 𝐴, 𝑅) ∧ 𝑥 = sup(Pred(𝑅, 𝐴, 𝑥), 𝐴, 𝑅))}

This definition is referenced by:  wlimeq12  33106  nfwlim  33109  elwlim  33110  wlimss  33116