Theorem trpredeq3

Description: Equality theorem for transitive predecessors. (Contributed by Scott Fenton, 2-Feb-2011)

	Ref	Expression
Assertion	trpredeq3	⊢ ( 𝑋 = 𝑌 → TrPred ( 𝑅 , 𝐴 , 𝑋 ) = TrPred ( 𝑅 , 𝐴 , 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		predeq3	⊢ ( 𝑋 = 𝑌 → Pred ( 𝑅 , 𝐴 , 𝑋 ) = Pred ( 𝑅 , 𝐴 , 𝑌 ) )
2		rdgeq2	⊢ ( Pred ( 𝑅 , 𝐴 , 𝑋 ) = Pred ( 𝑅 , 𝐴 , 𝑌 ) → rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) = rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑌 ) ) )
3	1 2	syl	⊢ ( 𝑋 = 𝑌 → rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) = rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑌 ) ) )
4	3	reseq1d	⊢ ( 𝑋 = 𝑌 → ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) = ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑌 ) ) ↾ ω ) )
5	4	rneqd	⊢ ( 𝑋 = 𝑌 → ran ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) = ran ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑌 ) ) ↾ ω ) )
6	5	unieqd	⊢ ( 𝑋 = 𝑌 → ∪ ran ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) = ∪ ran ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑌 ) ) ↾ ω ) )
7		df-trpred	⊢ TrPred ( 𝑅 , 𝐴 , 𝑋 ) = ∪ ran ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω )
8		df-trpred	⊢ TrPred ( 𝑅 , 𝐴 , 𝑌 ) = ∪ ran ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑌 ) ) ↾ ω )
9	6 7 8	3eqtr4g	⊢ ( 𝑋 = 𝑌 → TrPred ( 𝑅 , 𝐴 , 𝑋 ) = TrPred ( 𝑅 , 𝐴 , 𝑌 ) )