Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-wsuc Structured version   Visualization version   GIF version

Definition df-wsuc 35245
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.)
Assertion
Ref Expression
df-wsuc wsuc(𝑅, 𝐴, 𝑋) = inf(Pred(𝑅, 𝐴, 𝑋), 𝐴, 𝑅)

Detailed syntax breakdown of Definition df-wsuc
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cR . . 3 class 𝑅
3 cX . . 3 class 𝑋
41, 2, 3cwsuc 35243 . 2 class wsuc(𝑅, 𝐴, 𝑋)
52ccnv 5665 . . . 4 class 𝑅
61, 5, 3cpred 6289 . . 3 class Pred(𝑅, 𝐴, 𝑋)
76, 1, 2cinf 9431 . 2 class inf(Pred(𝑅, 𝐴, 𝑋), 𝐴, 𝑅)
84, 7wceq 1533 1 wff wsuc(𝑅, 𝐴, 𝑋) = inf(Pred(𝑅, 𝐴, 𝑋), 𝐴, 𝑅)
Colors of variables: wff setvar class
This definition is referenced by:  wsuceq123  35247  nfwsuc  35251  wsucex  35259  wsuccl  35260  wsuclb  35261
  Copyright terms: Public domain W3C validator