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 TrPredRAX=ranrecaVyaPredRAyPredRAXω

Detailed syntax breakdown

Step Hyp Ref Expression
0 cR classR
1 cA classA
2 cX classX
3 1 0 2 ctrpred classTrPredRAX
4 va setvara
5 cvv classV
6 vy setvary
7 4 cv setvara
8 6 cv setvary
9 1 0 8 cpred classPredRAy
10 6 7 9 ciun classyaPredRAy
11 4 5 10 cmpt classaVyaPredRAy
12 1 0 2 cpred classPredRAX
13 11 12 crdg classrecaVyaPredRAyPredRAX
14 com classω
15 13 14 cres classrecaVyaPredRAyPredRAXω
16 15 crn classranrecaVyaPredRAyPredRAXω
17 16 cuni classranrecaVyaPredRAyPredRAXω
18 3 17 wceq wffTrPredRAX=ranrecaVyaPredRAyPredRAXω