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

Definition df-trpred 28906
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 28918 and trpredmintr 28919). 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 28905 . 2  class  TrPred ( R ,  A ,  X
)
5 va . . . . . . 7  setvar  a
6 cvv 3113 . . . . . . 7  class  _V
7 vy . . . . . . . 8  setvar  y
85cv 1378 . . . . . . . 8  class  a
97cv 1378 . . . . . . . . 9  class  y
101, 2, 9cpred 28848 . . . . . . . 8  class  Pred ( R ,  A , 
y )
117, 8, 10ciun 4325 . . . . . . 7  class  U_ y  e.  a  Pred ( R ,  A ,  y )
125, 6, 11cmpt 4505 . . . . . 6  class  ( a  e.  _V  |->  U_ y  e.  a  Pred ( R ,  A ,  y ) )
131, 2, 3cpred 28848 . . . . . 6  class  Pred ( R ,  A ,  X )
1412, 13crdg 7075 . . . . 5  class  rec (
( a  e.  _V  |->  U_ y  e.  a  Pred ( R ,  A , 
y ) ) , 
Pred ( R ,  A ,  X )
)
15 com 6684 . . . . 5  class  om
1614, 15cres 5001 . . . 4  class  ( rec ( ( a  e. 
_V  |->  U_ y  e.  a 
Pred ( R ,  A ,  y )
) ,  Pred ( R ,  A ,  X ) )  |`  om )
1716crn 5000 . . 3  class  ran  ( rec ( ( a  e. 
_V  |->  U_ y  e.  a 
Pred ( R ,  A ,  y )
) ,  Pred ( R ,  A ,  X ) )  |`  om )
1817cuni 4245 . 2  class  U. ran  ( rec ( ( a  e.  _V  |->  U_ y  e.  a  Pred ( R ,  A ,  y ) ) ,  Pred ( R ,  A ,  X ) )  |`  om )
194, 18wceq 1379 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 setvar class
This definition is referenced by:  dftrpred2  28907  trpredeq1  28908  trpredeq2  28909  trpredeq3  28910  trpredpred  28916  trpredex  28925
  Copyright terms: Public domain W3C validator