Theorem predun

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

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

Proof

Step	Hyp	Ref	Expression
1		indir	$$⊢\left(A\cup B\right)\cap R^{-1}\left[\left\{X\right\}\right]=\left(A\cap R^{-1}\left[\left\{X\right\}\right]\right)\cup \left(B\cap R^{-1}\left[\left\{X\right\}\right]\right)$$
2		df-pred	$$⊢Pred\left(R,\left(A\cup B\right),X\right)=\left(A\cup 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	uneq12i	$$⊢Pred\left(R,A,X\right)\cup Pred\left(R,B,X\right)=\left(A\cap R^{-1}\left[\left\{X\right\}\right]\right)\cup \left(B\cap R^{-1}\left[\left\{X\right\}\right]\right)$$
6	1 2 5	3eqtr4i	$$⊢Pred\left(R,\left(A\cup B\right),X\right)=Pred\left(R,A,X\right)\cup Pred\left(R,B,X\right)$$