trpredeq3

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

		Ref	Expression
	Assertion	trpredeq3	$⊢ X = Y \to TrPred (R, A, X) = TrPred (R, A, Y)$

Step	Hyp	Ref	Expression
1		predeq3	$⊢ X = Y \to Pred (R, A, X) = Pred (R, A, Y)$
2		rdgeq2	$⊢ Pred (R, A, X) = Pred (R, A, Y) \to rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) = rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, Y))$
3	1 2	syl	$⊢ X = Y \to rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) = rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, Y))$
4	3	reseq1d	$⊢ X = Y \to {rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω} = {rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, Y)) ↾}_{ω}$
5	4	rneqd	$⊢ X = Y \to ran ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) = ran ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, Y)) ↾}_{ω})$
6	5	unieqd	$⊢ X = Y \to ⋃ ran ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) = ⋃ ran ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, Y)) ↾}_{ω})$
7		df-trpred	$⊢ TrPred (R, A, X) = ⋃ ran ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω})$
8		df-trpred	$⊢ TrPred (R, A, Y) = ⋃ ran ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, Y)) ↾}_{ω})$
9	6 7 8	3eqtr4g	$⊢ X = Y \to TrPred (R, A, X) = TrPred (R, A, Y)$

Metamath Proof Explorer