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	$$⊢\left(X\in A\wedge R\mathrm{Se}A\right)\to TrPred\left(R,A,X\right)=\bigcup _{y\in Pred\left(R,A,X\right)}\left(\left\{y\right\}\cup TrPred\left(R,A,y\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		dftrpred3g	$$⊢\left(X\in A\wedge R\mathrm{Se}A\right)\to TrPred\left(R,A,X\right)=Pred\left(R,A,X\right)\cup \bigcup _{y\in Pred\left(R,A,X\right)}TrPred\left(R,A,y\right)$$
2		iunun	$$⊢\bigcup _{y\in Pred\left(R,A,X\right)}\left(\left\{y\right\}\cup TrPred\left(R,A,y\right)\right)=\bigcup _{y\in Pred\left(R,A,X\right)}\left\{y\right\}\cup \bigcup _{y\in Pred\left(R,A,X\right)}TrPred\left(R,A,y\right)$$
3		iunid	$$⊢\bigcup _{y\in Pred\left(R,A,X\right)}\left\{y\right\}=Pred\left(R,A,X\right)$$
4	3	uneq1i	$$⊢\bigcup _{y\in Pred\left(R,A,X\right)}\left\{y\right\}\cup \bigcup _{y\in Pred\left(R,A,X\right)}TrPred\left(R,A,y\right)=Pred\left(R,A,X\right)\cup \bigcup _{y\in Pred\left(R,A,X\right)}TrPred\left(R,A,y\right)$$
5	2 4	eqtri	$$⊢\bigcup _{y\in Pred\left(R,A,X\right)}\left(\left\{y\right\}\cup TrPred\left(R,A,y\right)\right)=Pred\left(R,A,X\right)\cup \bigcup _{y\in Pred\left(R,A,X\right)}TrPred\left(R,A,y\right)$$
6	1 5	eqtr4di	$$⊢\left(X\in A\wedge R\mathrm{Se}A\right)\to TrPred\left(R,A,X\right)=\bigcup _{y\in Pred\left(R,A,X\right)}\left(\left\{y\right\}\cup TrPred\left(R,A,y\right)\right)$$