Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-trpred Unicode version

Definition df-trpred 24221
Description: Define the transitive predecessors of a class  X under a relationship  R and a class  A. This class can be thought of as the "smallest" class containing all elements of  A that are linked to  X by a chain of  R relationships (see trpredtr 24233 and trpredmintr 24234). Definition based off of Lemma 4.2 of Don Monk's notes for Advanced Set Theory, which can be found at http://euclid.colorado.edu/~monkd/settheory (check The Internet Archive for it now as Prof. Monk appears to have rewritten his website). (Contributed by Scott Fenton, 2-Feb-2011.)
Assertion
Ref Expression
df-trpred  |-  TrPred ( R ,  A ,  X
)  =  U. ran  ( rec ( ( a  e.  _V  |->  U_ y  e.  a  Pred ( R ,  A ,  y ) ) ,  Pred ( R ,  A ,  X ) )  |`  om )
Distinct variable groups:    R, a,
y    A, a, y    X, a, y

Detailed syntax breakdown of Definition df-trpred
StepHypRef Expression
1 cA . . 3  class  A
2 cR . . 3  class  R
3 cX . . 3  class  X
41, 2, 3ctrpred 24220 . 2  class  TrPred ( R ,  A ,  X
)
5 va . . . . . . 7  set  a
6 cvv 2788 . . . . . . 7  class  _V
7 vy . . . . . . . 8  set  y
85cv 1622 . . . . . . . 8  class  a
97cv 1622 . . . . . . . . 9  class  y
101, 2, 9cpred 24167 . . . . . . . 8  class  Pred ( R ,  A , 
y )
117, 8, 10ciun 3905 . . . . . . 7  class  U_ y  e.  a  Pred ( R ,  A ,  y )
125, 6, 11cmpt 4077 . . . . . 6  class  ( a  e.  _V  |->  U_ y  e.  a  Pred ( R ,  A ,  y ) )
131, 2, 3cpred 24167 . . . . . 6  class  Pred ( R ,  A ,  X )
1412, 13crdg 6422 . . . . 5  class  rec (
( a  e.  _V  |->  U_ y  e.  a  Pred ( R ,  A , 
y ) ) , 
Pred ( R ,  A ,  X )
)
15 com 4656 . . . . 5  class  om
1614, 15cres 4691 . . . 4  class  ( rec ( ( a  e. 
_V  |->  U_ y  e.  a 
Pred ( R ,  A ,  y )
) ,  Pred ( R ,  A ,  X ) )  |`  om )
1716crn 4690 . . 3  class  ran  ( rec ( ( a  e. 
_V  |->  U_ y  e.  a 
Pred ( R ,  A ,  y )
) ,  Pred ( R ,  A ,  X ) )  |`  om )
1817cuni 3827 . 2  class  U. ran  ( rec ( ( a  e.  _V  |->  U_ y  e.  a  Pred ( R ,  A ,  y ) ) ,  Pred ( R ,  A ,  X ) )  |`  om )
194, 18wceq 1623 1  wff  TrPred ( R ,  A ,  X
)  =  U. ran  ( rec ( ( a  e.  _V  |->  U_ y  e.  a  Pred ( R ,  A ,  y ) ) ,  Pred ( R ,  A ,  X ) )  |`  om )
Colors of variables: wff set class
This definition is referenced by:  dftrpred2  24222  trpredeq1  24223  trpredeq2  24224  trpredeq3  24225  trpredpred  24231  trpredex  24240
  Copyright terms: Public domain W3C validator