Definition df-wlim

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)

	Ref	Expression
Assertion	df-wlim	$$⊢WLim\left(R,A\right)=\left\{x\in A|\left(x\ne inf\left(A,A,R\right)\wedge x=sup\left(Pred\left(R,A,x\right),A,R\right)\right)\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cR	$$classR$$
1		cA	$$classA$$
2	1 0	cwlim	$$classWLim\left(R,A\right)$$
3		vx	$$setvarx$$
4	3	cv	$$setvarx$$
5	1 1 0	cinf	$$classinf\left(A,A,R\right)$$
6	4 5	wne	$$wffx\ne inf\left(A,A,R\right)$$
7	1 0 4	cpred	$$classPred\left(R,A,x\right)$$
8	7 1 0	csup	$$classsup\left(Pred\left(R,A,x\right),A,R\right)$$
9	4 8	wceq	$$wffx=sup\left(Pred\left(R,A,x\right),A,R\right)$$
10	6 9	wa	$$wff\left(x\ne inf\left(A,A,R\right)\wedge x=sup\left(Pred\left(R,A,x\right),A,R\right)\right)$$
11	10 3 1	crab	$$class\left\{x\in A|\left(x\ne inf\left(A,A,R\right)\wedge x=sup\left(Pred\left(R,A,x\right),A,R\right)\right)\right\}$$
12	2 11	wceq	$$wffWLim\left(R,A\right)=\left\{x\in A|\left(x\ne inf\left(A,A,R\right)\wedge x=sup\left(Pred\left(R,A,x\right),A,R\right)\right)\right\}$$