Theorem predin

Description: Intersection law for predecessor classes. (Contributed by Scott Fenton, 29-Mar-2011)

	Ref	Expression
Assertion	predin	$$⊢Pred\left(R,\left(A\cap B\right),X\right)=Pred\left(R,A,X\right)\cap Pred\left(R,B,X\right)$$

Proof

Step	Hyp	Ref	Expression
1		inindir	$$⊢\left(A\cap B\right)\cap R^{-1}\left[\left\{X\right\}\right]=\left(A\cap R^{-1}\left[\left\{X\right\}\right]\right)\cap \left(B\cap R^{-1}\left[\left\{X\right\}\right]\right)$$
2		df-pred	$$⊢Pred\left(R,\left(A\cap B\right),X\right)=\left(A\cap B\right)\cap R^{-1}\left[\left\{X\right\}\right]$$
3		df-pred	$$⊢Pred\left(R,A,X\right)=A\cap R^{-1}\left[\left\{X\right\}\right]$$
4		df-pred	$$⊢Pred\left(R,B,X\right)=B\cap R^{-1}\left[\left\{X\right\}\right]$$
5	3 4	ineq12i	$$⊢Pred\left(R,A,X\right)\cap Pred\left(R,B,X\right)=\left(A\cap R^{-1}\left[\left\{X\right\}\right]\right)\cap \left(B\cap R^{-1}\left[\left\{X\right\}\right]\right)$$
6	1 2 5	3eqtr4i	$$⊢Pred\left(R,\left(A\cap B\right),X\right)=Pred\left(R,A,X\right)\cap Pred\left(R,B,X\right)$$