Metamath Proof Explorer

Theorem trpredeq2

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

		Ref	Expression
	Assertion	trpredeq2	$⊢ A = B \to TrPred (R, A, X) = TrPred (R, B, X)$

Proof

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