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 ( 𝑅 , 𝐴 , 𝑋 ) = inf ( Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) , 𝐴 , 𝑅 )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cR	⊢ 𝑅
1		cA	⊢ 𝐴
2		cX	⊢ 𝑋
3	1 0 2	cwsuc	⊢ wsuc ( 𝑅 , 𝐴 , 𝑋 )
4	0	ccnv	⊢ ◡ 𝑅
5	1 4 2	cpred	⊢ Pred ( ◡ 𝑅 , 𝐴 , 𝑋 )
6	5 1 0	cinf	⊢ inf ( Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) , 𝐴 , 𝑅 )
7	3 6	wceq	⊢ wsuc ( 𝑅 , 𝐴 , 𝑋 ) = inf ( Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) , 𝐴 , 𝑅 )