Theorem elpredim

Description: Membership in a predecessor class - implicative version. (Contributed by Scott Fenton, 9-May-2012)

	Ref	Expression
Hypothesis	elpredim.1	$$⊢X\in \mathrm{V}$$
Assertion	elpredim	$$⊢Y\in Pred\left(R,A,X\right)\to YRX$$

Proof

Step	Hyp	Ref	Expression
1		elpredim.1	$$⊢X\in \mathrm{V}$$
2		df-pred	$$⊢Pred\left(R,A,X\right)=A\cap R^{-1}\left[\left\{X\right\}\right]$$
3	2	elin2	$$⊢Y\in Pred\left(R,A,X\right)\leftrightarrow \left(Y\in A\wedge Y\in R^{-1}\left[\left\{X\right\}\right]\right)$$
4		elimasng	$$⊢\left(X\in \mathrm{V}\wedge Y\in R^{-1}\left[\left\{X\right\}\right]\right)\to \left(Y\in R^{-1}\left[\left\{X\right\}\right]\leftrightarrow ⟨X,Y⟩\in R^{-1}\right)$$
5		opelcnvg	$$⊢\left(X\in \mathrm{V}\wedge Y\in R^{-1}\left[\left\{X\right\}\right]\right)\to \left(⟨X,Y⟩\in R^{-1}\leftrightarrow ⟨Y,X⟩\in R\right)$$
6	4 5	bitrd	$$⊢\left(X\in \mathrm{V}\wedge Y\in R^{-1}\left[\left\{X\right\}\right]\right)\to \left(Y\in R^{-1}\left[\left\{X\right\}\right]\leftrightarrow ⟨Y,X⟩\in R\right)$$
7	1 6	mpan	$$⊢Y\in R^{-1}\left[\left\{X\right\}\right]\to \left(Y\in R^{-1}\left[\left\{X\right\}\right]\leftrightarrow ⟨Y,X⟩\in R\right)$$
8	7	ibi	$$⊢Y\in R^{-1}\left[\left\{X\right\}\right]\to ⟨Y,X⟩\in R$$
9		df-br	$$⊢YRX\leftrightarrow ⟨Y,X⟩\in R$$
10	8 9	sylibr	$$⊢Y\in R^{-1}\left[\left\{X\right\}\right]\to YRX$$
11	3 10	simplbiim	$$⊢Y\in Pred\left(R,A,X\right)\to YRX$$