Theorem trpredeq2

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

	Ref	Expression
Assertion	trpredeq2	⊢ ( 𝐴 = 𝐵 → TrPred ( 𝑅 , 𝐴 , 𝑋 ) = TrPred ( 𝑅 , 𝐵 , 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		predeq2	⊢ ( 𝐴 = 𝐵 → Pred ( 𝑅 , 𝐴 , 𝑦 ) = Pred ( 𝑅 , 𝐵 , 𝑦 ) )
2	1	iuneq2d	⊢ ( 𝐴 = 𝐵 → ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) = ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐵 , 𝑦 ) )
3	2	mpteq2dv	⊢ ( 𝐴 = 𝐵 → ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) = ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐵 , 𝑦 ) ) )
4		predeq2	⊢ ( 𝐴 = 𝐵 → Pred ( 𝑅 , 𝐴 , 𝑋 ) = Pred ( 𝑅 , 𝐵 , 𝑋 ) )
5		rdgeq12	⊢ ( ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) = ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐵 , 𝑦 ) ) ∧ Pred ( 𝑅 , 𝐴 , 𝑋 ) = Pred ( 𝑅 , 𝐵 , 𝑋 ) ) → rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) = rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐵 , 𝑦 ) ) , Pred ( 𝑅 , 𝐵 , 𝑋 ) ) )
6	5	reseq1d	⊢ ( ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) = ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐵 , 𝑦 ) ) ∧ Pred ( 𝑅 , 𝐴 , 𝑋 ) = Pred ( 𝑅 , 𝐵 , 𝑋 ) ) → ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) = ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐵 , 𝑦 ) ) , Pred ( 𝑅 , 𝐵 , 𝑋 ) ) ↾ ω ) )
7	3 4 6	syl2anc	⊢ ( 𝐴 = 𝐵 → ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) = ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐵 , 𝑦 ) ) , Pred ( 𝑅 , 𝐵 , 𝑋 ) ) ↾ ω ) )
8	7	rneqd	⊢ ( 𝐴 = 𝐵 → ran ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) = ran ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐵 , 𝑦 ) ) , Pred ( 𝑅 , 𝐵 , 𝑋 ) ) ↾ ω ) )
9	8	unieqd	⊢ ( 𝐴 = 𝐵 → ∪ ran ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) = ∪ ran ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐵 , 𝑦 ) ) , Pred ( 𝑅 , 𝐵 , 𝑋 ) ) ↾ ω ) )
10		df-trpred	⊢ TrPred ( 𝑅 , 𝐴 , 𝑋 ) = ∪ ran ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω )
11		df-trpred	⊢ TrPred ( 𝑅 , 𝐵 , 𝑋 ) = ∪ ran ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐵 , 𝑦 ) ) , Pred ( 𝑅 , 𝐵 , 𝑋 ) ) ↾ ω )
12	9 10 11	3eqtr4g	⊢ ( 𝐴 = 𝐵 → TrPred ( 𝑅 , 𝐴 , 𝑋 ) = TrPred ( 𝑅 , 𝐵 , 𝑋 ) )