Theorem nfwlim

Description: Bound-variable hypothesis builder for the limit class. (Contributed by Scott Fenton, 15-Jun-2018) (Proof shortened by AV, 10-Oct-2021)

	Ref	Expression
Hypotheses	nfwlim.1	$$⊢\underset{\_}{Ⅎ}xR$$
	nfwlim.2	$$⊢\underset{\_}{Ⅎ}xA$$
Assertion	nfwlim	$$⊢\underset{\_}{Ⅎ}xWLim\left(R,A\right)$$

Proof

Step	Hyp	Ref	Expression
1		nfwlim.1	$$⊢\underset{\_}{Ⅎ}xR$$
2		nfwlim.2	$$⊢\underset{\_}{Ⅎ}xA$$
3		df-wlim	$$⊢WLim\left(R,A\right)=\left\{y\in A|\left(y\ne inf\left(A,A,R\right)\wedge y=sup\left(Pred\left(R,A,y\right),A,R\right)\right)\right\}$$
4		nfcv	$$⊢\underset{\_}{Ⅎ}xy$$
5	2 2 1	nfinf	$$⊢\underset{\_}{Ⅎ}xinf\left(A,A,R\right)$$
6	4 5	nfne	$$⊢Ⅎxy\ne inf\left(A,A,R\right)$$
7	1 2 4	nfpred	$$⊢\underset{\_}{Ⅎ}xPred\left(R,A,y\right)$$
8	7 2 1	nfsup	$$⊢\underset{\_}{Ⅎ}xsup\left(Pred\left(R,A,y\right),A,R\right)$$
9	8	nfeq2	$$⊢Ⅎxy=sup\left(Pred\left(R,A,y\right),A,R\right)$$
10	6 9	nfan	$$⊢Ⅎx\left(y\ne inf\left(A,A,R\right)\wedge y=sup\left(Pred\left(R,A,y\right),A,R\right)\right)$$
11	10 2	nfrabw	$$⊢\underset{\_}{Ⅎ}x\left\{y\in A|\left(y\ne inf\left(A,A,R\right)\wedge y=sup\left(Pred\left(R,A,y\right),A,R\right)\right)\right\}$$
12	3 11	nfcxfr	$$⊢\underset{\_}{Ⅎ}xWLim\left(R,A\right)$$