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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cR	|- R
1		cA	|- A
2	1 0	cwlim	|- WLim ( R , A )
3		vx	|- x
4	3	cv	|- x
5	1 1 0	cinf	|- inf ( A , A , R )
6	4 5	wne	|- x =/= inf ( A , A , R )
7	1 0 4	cpred	|- Pred ( R , A , x )
8	7 1 0	csup	|- sup ( Pred ( R , A , x ) , A , R )
9	4 8	wceq	|- x = sup ( Pred ( R , A , x ) , A , R )
10	6 9	wa	|- ( x =/= inf ( A , A , R ) /\ x = sup ( Pred ( R , A , x ) , A , R ) )
11	10 3 1	crab	|- { x e. A | ( x =/= inf ( A , A , R ) /\ x = sup ( Pred ( R , A , x ) , A , R ) ) }
12	2 11	wceq	|- WLim ( R , A ) = { x e. A | ( x =/= inf ( A , A , R ) /\ x = sup ( Pred ( R , A , x ) , A , R ) ) }