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

Definition df-trpred 24292
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 24304 and trpredmintr 24305). 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 24291 . 2  class  TrPred ( R ,  A ,  X
)
5 va . . . . . . 7  set  a
6 cvv 2801 . . . . . . 7  class  _V
7 vy . . . . . . . 8  set  y
85cv 1631 . . . . . . . 8  class  a
97cv 1631 . . . . . . . . 9  class  y
101, 2, 9cpred 24238 . . . . . . . 8  class  Pred ( R ,  A , 
y )
117, 8, 10ciun 3921 . . . . . . 7  class  U_ y  e.  a  Pred ( R ,  A ,  y )
125, 6, 11cmpt 4093 . . . . . 6  class  ( a  e.  _V  |->  U_ y  e.  a  Pred ( R ,  A ,  y ) )
131, 2, 3cpred 24238 . . . . . 6  class  Pred ( R ,  A ,  X )
1412, 13crdg 6438 . . . . 5  class  rec (
( a  e.  _V  |->  U_ y  e.  a  Pred ( R ,  A , 
y ) ) , 
Pred ( R ,  A ,  X )
)
15 com 4672 . . . . 5  class  om
1614, 15cres 4707 . . . 4  class  ( rec ( ( a  e. 
_V  |->  U_ y  e.  a 
Pred ( R ,  A ,  y )
) ,  Pred ( R ,  A ,  X ) )  |`  om )
1716crn 4706 . . 3  class  ran  ( rec ( ( a  e. 
_V  |->  U_ y  e.  a 
Pred ( R ,  A ,  y )
) ,  Pred ( R ,  A ,  X ) )  |`  om )
1817cuni 3843 . 2  class  U. ran  ( rec ( ( a  e.  _V  |->  U_ y  e.  a  Pred ( R ,  A ,  y ) ) ,  Pred ( R ,  A ,  X ) )  |`  om )
194, 18wceq 1632 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  24293  trpredeq1  24294  trpredeq2  24295  trpredeq3  24296  trpredpred  24302  trpredex  24311
  Copyright terms: Public domain W3C validator