Metamath Proof Explorer


Definition df-trpred

Description: Define the transitive predecessors of a class X under a relation R in a class A . This class can be thought of as the "smallest" class containing all elements of A that are linked to X by an R -chain (see trpredtr and trpredmintr ). Definition based on Theorem 8.4 of Don Monk's notes for Advanced Set Theory, which can be found at https://euclid.colorado.edu/~monkd/setth.pdf . (Contributed by Scott Fenton, 2-Feb-2011)

Ref Expression
Assertion 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 )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cR
 |-  R
1 cA
 |-  A
2 cX
 |-  X
3 1 0 2 ctrpred
 |-  TrPred ( R , A , X )
4 va
 |-  a
5 cvv
 |-  _V
6 vy
 |-  y
7 4 cv
 |-  a
8 6 cv
 |-  y
9 1 0 8 cpred
 |-  Pred ( R , A , y )
10 6 7 9 ciun
 |-  U_ y e. a Pred ( R , A , y )
11 4 5 10 cmpt
 |-  ( a e. _V |-> U_ y e. a Pred ( R , A , y ) )
12 1 0 2 cpred
 |-  Pred ( R , A , X )
13 11 12 crdg
 |-  rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) )
14 com
 |-  _om
15 13 14 cres
 |-  ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om )
16 15 crn
 |-  ran ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om )
17 16 cuni
 |-  U. ran ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om )
18 3 17 wceq
 |-  TrPred ( R , A , X ) = U. ran ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om )