Definition df-trpred 31718

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

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cR	. . 3 class R
3		cX	. . 3 class X
4	1, 2, 3	ctrpred 31717	. 2 class TrPred ( R , A , X )
5		va	. . . . . . 7 setvar a
6		cvv 3200	. . . . . . 7 class _V
7		vy	. . . . . . . 8 setvar y
8	5	cv 1482	. . . . . . . 8 class a
9	7	cv 1482	. . . . . . . . 9 class y
10	1, 2, 9	cpred 5679	. . . . . . . 8 class Pred ( R , A , y )
11	7, 8, 10	ciun 4520	. . . . . . 7 class U_ y e. a Pred ( R , A , y )
12	5, 6, 11	cmpt 4729	. . . . . 6 class ( a e. _V |-> U_ y e. a Pred ( R , A , y ) )
13	1, 2, 3	cpred 5679	. . . . . 6 class Pred ( R , A , X )
14	12, 13	crdg 7505	. . . . 5 class rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) )
15		com 7065	. . . . 5 class om
16	14, 15	cres 5116	. . . 4 class ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` om )
17	16	crn 5115	. . 3 class ran ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` om )
18	17	cuni 4436	. 2 class U. ran ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` om )
19	4, 18	wceq 1483	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 )

This definition is referenced by:  dftrpred2  31719  trpredeq1  31720  trpredeq2  31721  trpredeq3  31722  trpredpred  31728  trpredex  31737