Theorem elwlim

Description: Membership in the limit class. (Contributed by Scott Fenton, 15-Jun-2018) (Revised by AV, 10-Oct-2021)

	Ref	Expression
Assertion	elwlim	$$⊢X\in WLim\left(R,A\right)\leftrightarrow \left(X\in A\wedge X\ne inf\left(A,A,R\right)\wedge X=sup\left(Pred\left(R,A,X\right),A,R\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		neeq1	$$⊢x=X\to \left(x\ne inf\left(A,A,R\right)\leftrightarrow X\ne inf\left(A,A,R\right)\right)$$
2		id	$$⊢x=X\to x=X$$
3		predeq3	$$⊢x=X\to Pred\left(R,A,x\right)=Pred\left(R,A,X\right)$$
4	3	supeq1d	$$⊢x=X\to sup\left(Pred\left(R,A,x\right),A,R\right)=sup\left(Pred\left(R,A,X\right),A,R\right)$$
5	2 4	eqeq12d	$$⊢x=X\to \left(x=sup\left(Pred\left(R,A,x\right),A,R\right)\leftrightarrow X=sup\left(Pred\left(R,A,X\right),A,R\right)\right)$$
6	1 5	anbi12d	$$⊢x=X\to \left(\left(x\ne inf\left(A,A,R\right)\wedge x=sup\left(Pred\left(R,A,x\right),A,R\right)\right)\leftrightarrow \left(X\ne inf\left(A,A,R\right)\wedge X=sup\left(Pred\left(R,A,X\right),A,R\right)\right)\right)$$
7		df-wlim	$$⊢WLim\left(R,A\right)=\left\{x\in A|\left(x\ne inf\left(A,A,R\right)\wedge x=sup\left(Pred\left(R,A,x\right),A,R\right)\right)\right\}$$
8	6 7	elrab2	$$⊢X\in WLim\left(R,A\right)\leftrightarrow \left(X\in A\wedge \left(X\ne inf\left(A,A,R\right)\wedge X=sup\left(Pred\left(R,A,X\right),A,R\right)\right)\right)$$
9		3anass	$$⊢\left(X\in A\wedge X\ne inf\left(A,A,R\right)\wedge X=sup\left(Pred\left(R,A,X\right),A,R\right)\right)\leftrightarrow \left(X\in A\wedge \left(X\ne inf\left(A,A,R\right)\wedge X=sup\left(Pred\left(R,A,X\right),A,R\right)\right)\right)$$
10	8 9	bitr4i	$$⊢X\in WLim\left(R,A\right)\leftrightarrow \left(X\in A\wedge X\ne inf\left(A,A,R\right)\wedge X=sup\left(Pred\left(R,A,X\right),A,R\right)\right)$$