Definition df-trpred

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 and trpredmintr ). 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)

	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 )