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 31882
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 31880 . 2 class wsuc(𝑅, 𝐴, 𝑋)
52ccnv 5142 . . . 4 class 𝑅
61, 5, 3cpred 5717 . . 3 class Pred(𝑅, 𝐴, 𝑋)
76, 1, 2cinf 8388 . 2 class inf(Pred(𝑅, 𝐴, 𝑋), 𝐴, 𝑅)
84, 7wceq 1523 1 wff wsuc(𝑅, 𝐴, 𝑋) = inf(Pred(𝑅, 𝐴, 𝑋), 𝐴, 𝑅)
Colors of variables: wff setvar class
This definition is referenced by:  wsuceq123  31884  nfwsuc  31888  wsucex  31896  wsuccl  31897  wsuclb  31898
  Copyright terms: Public domain W3C validator