Metamath Proof Explorer

Theorem trpredeq1

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

		Ref	Expression
	Assertion	trpredeq1	$⊢ R = S \to TrPred (R, A, X) = TrPred (S, A, X)$

Proof

Step	Hyp	Ref	Expression
1		predeq1	$⊢ R = S \to Pred (R, A, y) = Pred (S, A, y)$
2	1	iuneq2d	$⊢ R = S \to ⋃_{y \in a} Pred (R, A, y) = ⋃_{y \in a} Pred (S, A, y)$
3	2	mpteq2dv	$⊢ R = S \to (a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)) = (a \in V ⟼ ⋃_{y \in a} Pred (S, A, y))$
4		predeq1	$⊢ R = S \to Pred (R, A, X) = Pred (S, A, X)$
5		rdgeq12	$⊢ ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)) = (a \in V ⟼ ⋃_{y \in a} Pred (S, A, y)) \land Pred (R, A, X) = Pred (S, A, X)) \to rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) = rec ((a \in V ⟼ ⋃_{y \in a} Pred (S, A, y)), Pred (S, A, X))$
6	3 4 5	syl2anc	$⊢ R = S \to rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) = rec ((a \in V ⟼ ⋃_{y \in a} Pred (S, A, y)), Pred (S, A, X))$
7	6	reseq1d	$⊢ R = S \to {rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω} = {rec ((a \in V ⟼ ⋃_{y \in a} Pred (S, A, y)), Pred (S, A, X)) ↾}_{ω}$
8	7	rneqd	$⊢ R = S \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 (S, A, y)), Pred (S, A, X)) ↾}_{ω})$
9	8	unieqd	$⊢ R = S \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 (S, A, y)), Pred (S, A, X)) ↾}_{ω})$
10		df-trpred	$⊢ TrPred (R, A, X) = ⋃ ran ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω})$
11		df-trpred	$⊢ TrPred (S, A, X) = ⋃ ran ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (S, A, y)), Pred (S, A, X)) ↾}_{ω})$
12	9 10 11	3eqtr4g	$⊢ R = S \to TrPred (R, A, X) = TrPred (S, A, X)$