Definition df-wlim 33734

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 33732	. 2 class WLim(𝑅, 𝐴)
4		vx	. . . . . 6 setvar 𝑥
5	4	cv 1538	. . . . 5 class 𝑥
6	1, 1, 2	cinf 9130	. . . . 5 class inf(𝐴, 𝐴, 𝑅)
7	5, 6	wne 2942	. . . 4 wff 𝑥 ≠ inf(𝐴, 𝐴, 𝑅)
8	1, 2, 5	cpred 6190	. . . . . 6 class Pred(𝑅, 𝐴, 𝑥)
9	8, 1, 2	csup 9129	. . . . 5 class sup(Pred(𝑅, 𝐴, 𝑥), 𝐴, 𝑅)
10	5, 9	wceq 1539	. . . 4 wff 𝑥 = sup(Pred(𝑅, 𝐴, 𝑥), 𝐴, 𝑅)
11	7, 10	wa 395	. . 3 wff (𝑥 ≠ inf(𝐴, 𝐴, 𝑅) ∧ 𝑥 = sup(Pred(𝑅, 𝐴, 𝑥), 𝐴, 𝑅))
12	11, 4, 1	crab 3067	. 2 class {𝑥 ∈ 𝐴 ∣ (𝑥 ≠ inf(𝐴, 𝐴, 𝑅) ∧ 𝑥 = sup(Pred(𝑅, 𝐴, 𝑥), 𝐴, 𝑅))}
13	3, 12	wceq 1539	1 wff WLim(𝑅, 𝐴) = {𝑥 ∈ 𝐴 ∣ (𝑥 ≠ inf(𝐴, 𝐴, 𝑅) ∧ 𝑥 = sup(Pred(𝑅, 𝐴, 𝑥), 𝐴, 𝑅))}

This definition is referenced by:  wlimeq12  33740  nfwlim  33743  elwlim  33744  wlimss  33750