Metamath Proof Explorer

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 ( R , A , X ) = inf ( Pred ( `' R , A , X ) , A , R )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cR 
 |-  R
1 cA 
 |-  A
2 cX 
 |-  X
3 1 0 2 cwsuc 
 |-  wsuc ( R , A , X )
4 0 ccnv 
 |-  `' R
5 1 4 2 cpred 
 |-  Pred ( `' R , A , X )
6 5 1 0 cinf 
 |-  inf ( Pred ( `' R , A , X ) , A , R )
7 3 6 wceq 
 |-  wsuc ( R , A , X ) = inf ( Pred ( `' R , A , X ) , A , R )