Theorem sspred

Description: Another subset/predecessor class relationship. (Contributed by Scott Fenton, 6-Feb-2011)

	Ref	Expression
Assertion	sspred	$$⊢\left(B\subseteq A\wedge Pred\left(R,A,X\right)\subseteq B\right)\to Pred\left(R,A,X\right)=Pred\left(R,B,X\right)$$

Proof

Step	Hyp	Ref	Expression
1		sseqin2	$$⊢B\subseteq A\leftrightarrow A\cap B=B$$
2		df-pred	$$⊢Pred\left(R,A,X\right)=A\cap R^{-1}\left[\left\{X\right\}\right]$$
3	2	sseq1i	$$⊢Pred\left(R,A,X\right)\subseteq B\leftrightarrow A\cap R^{-1}\left[\left\{X\right\}\right]\subseteq B$$
4		df-ss	$$⊢A\cap R^{-1}\left[\left\{X\right\}\right]\subseteq B\leftrightarrow \left(A\cap R^{-1}\left[\left\{X\right\}\right]\right)\cap B=A\cap R^{-1}\left[\left\{X\right\}\right]$$
5		in32	$$⊢\left(A\cap R^{-1}\left[\left\{X\right\}\right]\right)\cap B=\left(A\cap B\right)\cap R^{-1}\left[\left\{X\right\}\right]$$
6	5	eqeq1i	$$⊢\left(A\cap R^{-1}\left[\left\{X\right\}\right]\right)\cap B=A\cap R^{-1}\left[\left\{X\right\}\right]\leftrightarrow \left(A\cap B\right)\cap R^{-1}\left[\left\{X\right\}\right]=A\cap R^{-1}\left[\left\{X\right\}\right]$$
7	3 4 6	3bitri	$$⊢Pred\left(R,A,X\right)\subseteq B\leftrightarrow \left(A\cap B\right)\cap R^{-1}\left[\left\{X\right\}\right]=A\cap R^{-1}\left[\left\{X\right\}\right]$$
8		ineq1	$$⊢A\cap B=B\to \left(A\cap B\right)\cap R^{-1}\left[\left\{X\right\}\right]=B\cap R^{-1}\left[\left\{X\right\}\right]$$
9	8	eqeq1d	$$⊢A\cap B=B\to \left(\left(A\cap B\right)\cap R^{-1}\left[\left\{X\right\}\right]=A\cap R^{-1}\left[\left\{X\right\}\right]\leftrightarrow B\cap R^{-1}\left[\left\{X\right\}\right]=A\cap R^{-1}\left[\left\{X\right\}\right]\right)$$
10	9	biimpa	$$⊢\left(A\cap B=B\wedge \left(A\cap B\right)\cap R^{-1}\left[\left\{X\right\}\right]=A\cap R^{-1}\left[\left\{X\right\}\right]\right)\to B\cap R^{-1}\left[\left\{X\right\}\right]=A\cap R^{-1}\left[\left\{X\right\}\right]$$
11		df-pred	$$⊢Pred\left(R,B,X\right)=B\cap R^{-1}\left[\left\{X\right\}\right]$$
12	10 11 2	3eqtr4g	$$⊢\left(A\cap B=B\wedge \left(A\cap B\right)\cap R^{-1}\left[\left\{X\right\}\right]=A\cap R^{-1}\left[\left\{X\right\}\right]\right)\to Pred\left(R,B,X\right)=Pred\left(R,A,X\right)$$
13	12	eqcomd	$$⊢\left(A\cap B=B\wedge \left(A\cap B\right)\cap R^{-1}\left[\left\{X\right\}\right]=A\cap R^{-1}\left[\left\{X\right\}\right]\right)\to Pred\left(R,A,X\right)=Pred\left(R,B,X\right)$$
14	1 7 13	syl2anb	$$⊢\left(B\subseteq A\wedge Pred\left(R,A,X\right)\subseteq B\right)\to Pred\left(R,A,X\right)=Pred\left(R,B,X\right)$$