Definition df-wlim 31758

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 ( R , A ) = { x e. A | ( x =/= inf ( A , A , R ) /\ x = sup ( Pred ( R , A , x ) , A , R ) ) }

Distinct variable groups:   x, R   x, A

Detailed syntax breakdown of Definition df-wlim

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cR	. . 3 class R
3	1, 2	cwlim 31754	. 2 class WLim ( R , A )
4		vx	. . . . . 6 setvar x
5	4	cv 1482	. . . . 5 class x
6	1, 1, 2	cinf 8347	. . . . 5 class inf ( A , A , R )
7	5, 6	wne 2794	. . . 4 wff x =/= inf ( A , A , R )
8	1, 2, 5	cpred 5679	. . . . . 6 class Pred ( R , A , x )
9	8, 1, 2	csup 8346	. . . . 5 class sup ( Pred ( R , A , x ) , A , R )
10	5, 9	wceq 1483	. . . 4 wff x = sup ( Pred ( R , A , x ) , A , R )
11	7, 10	wa 384	. . 3 wff ( x =/= inf ( A , A , R ) /\ x = sup ( Pred ( R , A , x ) , A , R ) )
12	11, 4, 1	crab 2916	. 2 class { x e. A | ( x =/= inf ( A , A , R ) /\ x = sup ( Pred ( R , A , x ) , A , R ) ) }
13	3, 12	wceq 1483	1 wff WLim ( R , A ) = { x e. A | ( x =/= inf ( A , A , R ) /\ x = sup ( Pred ( R , A , x ) , A , R ) ) }

This definition is referenced by:  wlimeq12  31765  nfwlim  31768  elwlim  31769  wlimss  31778