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	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → TrPred ( 𝑅 , 𝐴 , 𝑋 ) = ∪ 𝑦 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ( { 𝑦 } ∪ TrPred ( 𝑅 , 𝐴 , 𝑦 ) ) )

Proof

Step	Hyp	Ref	Expression
1		dftrpred3g	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → TrPred ( 𝑅 , 𝐴 , 𝑋 ) = ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∪ ∪ 𝑦 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) TrPred ( 𝑅 , 𝐴 , 𝑦 ) ) )
2		iunun	⊢ ∪ 𝑦 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ( { 𝑦 } ∪ TrPred ( 𝑅 , 𝐴 , 𝑦 ) ) = ( ∪ 𝑦 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) { 𝑦 } ∪ ∪ 𝑦 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) TrPred ( 𝑅 , 𝐴 , 𝑦 ) )
3		iunid	⊢ ∪ 𝑦 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) { 𝑦 } = Pred ( 𝑅 , 𝐴 , 𝑋 )
4	3	uneq1i	⊢ ( ∪ 𝑦 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) { 𝑦 } ∪ ∪ 𝑦 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) TrPred ( 𝑅 , 𝐴 , 𝑦 ) ) = ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∪ ∪ 𝑦 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) TrPred ( 𝑅 , 𝐴 , 𝑦 ) )
5	2 4	eqtri	⊢ ∪ 𝑦 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ( { 𝑦 } ∪ TrPred ( 𝑅 , 𝐴 , 𝑦 ) ) = ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∪ ∪ 𝑦 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) TrPred ( 𝑅 , 𝐴 , 𝑦 ) )
6	1 5	eqtr4di	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → TrPred ( 𝑅 , 𝐴 , 𝑋 ) = ∪ 𝑦 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ( { 𝑦 } ∪ TrPred ( 𝑅 , 𝐴 , 𝑦 ) ) )