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

Definition df-trpred 30032
 Description: Define the transitive predecessors of a class under a relationship and a class . This class can be thought of as the "smallest" class containing all elements of that are linked to by a chain of relationships (see trpredtr 30044 and trpredmintr 30045). 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
Distinct variable groups:   ,,   ,,   ,,

Detailed syntax breakdown of Definition df-trpred
StepHypRef Expression
1 cA . . 3
2 cR . . 3
3 cX . . 3
41, 2, 3ctrpred 30031 . 2
5 va . . . . . . 7
6 cvv 3059 . . . . . . 7
7 vy . . . . . . . 8
85cv 1404 . . . . . . . 8
97cv 1404 . . . . . . . . 9
101, 2, 9cpred 5366 . . . . . . . 8
117, 8, 10ciun 4271 . . . . . . 7
125, 6, 11cmpt 4453 . . . . . 6
131, 2, 3cpred 5366 . . . . . 6
1412, 13crdg 7112 . . . . 5
15 com 6683 . . . . 5
1614, 15cres 4825 . . . 4
1716crn 4824 . . 3
1817cuni 4191 . 2
194, 18wceq 1405 1
 Colors of variables: wff setvar class This definition is referenced by:  dftrpred2  30033  trpredeq1  30034  trpredeq2  30035  trpredeq3  30036  trpredpred  30042  trpredex  30051
 Copyright terms: Public domain W3C validator