predidm

Description: Idempotent law for the predecessor class. (Contributed by Scott Fenton, 29-Mar-2011)

		Ref	Expression
	Assertion	predidm	$⊢ Pred (R, Pred (R, A, X), X) = Pred (R, A, X)$

Step	Hyp	Ref	Expression
1		df-pred	$⊢ Pred (R, Pred (R, A, X), X) = Pred (R, A, X) \cap R^{-1} [\{X\}]$
2		df-pred	$⊢ Pred (R, A, X) = A \cap R^{-1} [\{X\}]$
3		inidm	$⊢ R^{-1} [\{X\}] \cap R^{-1} [\{X\}] = R^{-1} [\{X\}]$
4	3	ineq2i	$⊢ A \cap (R^{-1} [\{X\}] \cap R^{-1} [\{X\}]) = A \cap R^{-1} [\{X\}]$
5	2 4	eqtr4i	$⊢ Pred (R, A, X) = A \cap (R^{-1} [\{X\}] \cap R^{-1} [\{X\}])$
6		inass	$⊢ (A \cap R^{-1} [\{X\}]) \cap R^{-1} [\{X\}] = A \cap (R^{-1} [\{X\}] \cap R^{-1} [\{X\}])$
7	5 6	eqtr4i	$⊢ Pred (R, A, X) = (A \cap R^{-1} [\{X\}]) \cap R^{-1} [\{X\}]$
8	2	ineq1i	$⊢ Pred (R, A, X) \cap R^{-1} [\{X\}] = (A \cap R^{-1} [\{X\}]) \cap R^{-1} [\{X\}]$
9	7 8	eqtr4i	$⊢ Pred (R, A, X) = Pred (R, A, X) \cap R^{-1} [\{X\}]$
10	1 9	eqtr4i	$⊢ Pred (R, Pred (R, A, X), X) = Pred (R, A, X)$

Metamath Proof Explorer