Definition df-wsuc

Description: Define the concept of a successor in a well-founded set. (Contributed by Scott Fenton, 13-Jun-2018) (Revised by AV, 10-Oct-2021)

	Ref	Expression
Assertion	df-wsuc	$$⊢wsuc\left(R,A,X\right)=sup\left(Pred\left(R^{-1},A,X\right),A,R\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cR	$$classR$$
1		cA	$$classA$$
2		cX	$$classX$$
3	1 0 2	cwsuc	$$classwsuc\left(R,A,X\right)$$
4	0	ccnv	$$class{R}^{-1}$$
5	1 4 2	cpred	$$classPred\left(R^{-1},A,X\right)$$
6	5 1 0	cinf	$$classsup\left(Pred\left(R^{-1},A,X\right),A,R\right)$$
7	3 6	wceq	$$wffwsuc\left(R,A,X\right)=sup\left(Pred\left(R^{-1},A,X\right),A,R\right)$$