Definition df-wlimOLD 31759

Description: Define the class of limit points of a well-founded set. (Contributed by Scott Fenton, 15-Jun-2018.) Obsolete version of df-wlim 31758 as of 10-Oct-2021. (New usage is discouraged.)

Assertion

Ref	Expression
df-wlimOLD	|- WLimOLD ( R , A ) = { x e. A | ( x =/= sup ( A , A , `' R ) /\ x = sup ( Pred ( R , A , x ) , A , R ) ) }

Distinct variable groups:   x, R   x, A

Detailed syntax breakdown of Definition df-wlimOLD

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cR	. . 3 class R
3	1, 2	cwlimOLD 31755	. 2 class WLimOLD ( R , A )
4		vx	. . . . . 6 setvar x
5	4	cv 1482	. . . . 5 class x
6	2	ccnv 5113	. . . . . 6 class `' R
7	1, 1, 6	csup 8346	. . . . 5 class sup ( A , A , `' R )
8	5, 7	wne 2794	. . . 4 wff x =/= sup ( A , A , `' R )
9	1, 2, 5	cpred 5679	. . . . . 6 class Pred ( R , A , x )
10	9, 1, 2	csup 8346	. . . . 5 class sup ( Pred ( R , A , x ) , A , R )
11	5, 10	wceq 1483	. . . 4 wff x = sup ( Pred ( R , A , x ) , A , R )
12	8, 11	wa 384	. . 3 wff ( x =/= sup ( A , A , `' R ) /\ x = sup ( Pred ( R , A , x ) , A , R ) )
13	12, 4, 1	crab 2916	. 2 class { x e. A | ( x =/= sup ( A , A , `' R ) /\ x = sup ( Pred ( R , A , x ) , A , R ) ) }
14	3, 13	wceq 1483	1 wff WLimOLD ( R , A ) = { x e. A | ( x =/= sup ( A , A , `' R ) /\ x = sup ( Pred ( R , A , x ) , A , R ) ) }

This definition is referenced by:  elwlimOLD  31770