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) = ⋃ ran ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω})$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cR	$class R$
1		cA	$class A$
2		cX	$class X$
3	1 0 2	ctrpred	$class TrPred (R, A, X)$
4		va	$setvar a$
5		cvv	$class V$
6		vy	$setvar y$
7	4	cv	$setvar a$
8	6	cv	$setvar y$
9	1 0 8	cpred	$class Pred (R, A, y)$
10	6 7 9	ciun	$class ⋃_{y \in a} Pred (R, A, y)$
11	4 5 10	cmpt	$class (a \in V ⟼ ⋃_{y \in a} Pred (R, A, y))$
12	1 0 2	cpred	$class Pred (R, A, X)$
13	11 12	crdg	$class rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X))$
14		com	$class ω$
15	13 14	cres	$class ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω})$
16	15	crn	$class ran ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω})$
17	16	cuni	$class ⋃ ran ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω})$
18	3 17	wceq	$wff TrPred (R, A, X) = ⋃ ran ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω})$

Metamath Proof Explorer

Definition df-trpred

Detailed syntax breakdown