Theorem dftrpred4g

Description: Another recursive expression for the transitive predecessors. (Contributed by Scott Fenton, 27-Apr-2012) (Revised by Mario Carneiro, 26-Jun-2015)

	Ref	Expression
Assertion	dftrpred4g	|- ( ( X e. A /\ R Se A ) -> TrPred ( R , A , X ) = U_ y e. Pred ( R , A , X ) ( { y } u. TrPred ( R , A , y ) ) )

Proof

Step	Hyp	Ref	Expression
1		dftrpred3g	|- ( ( X e. A /\ R Se A ) -> TrPred ( R , A , X ) = ( Pred ( R , A , X ) u. U_ y e. Pred ( R , A , X ) TrPred ( R , A , y ) ) )
2		iunun	|- U_ y e. Pred ( R , A , X ) ( { y } u. TrPred ( R , A , y ) ) = ( U_ y e. Pred ( R , A , X ) { y } u. U_ y e. Pred ( R , A , X ) TrPred ( R , A , y ) )
3		iunid	|- U_ y e. Pred ( R , A , X ) { y } = Pred ( R , A , X )
4	3	uneq1i	|- ( U_ y e. Pred ( R , A , X ) { y } u. U_ y e. Pred ( R , A , X ) TrPred ( R , A , y ) ) = ( Pred ( R , A , X ) u. U_ y e. Pred ( R , A , X ) TrPred ( R , A , y ) )
5	2 4	eqtri	|- U_ y e. Pred ( R , A , X ) ( { y } u. TrPred ( R , A , y ) ) = ( Pred ( R , A , X ) u. U_ y e. Pred ( R , A , X ) TrPred ( R , A , y ) )
6	1 5	eqtr4di	|- ( ( X e. A /\ R Se A ) -> TrPred ( R , A , X ) = U_ y e. Pred ( R , A , X ) ( { y } u. TrPred ( R , A , y ) ) )