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	|- F/_ x R
	nfwlim.2	|- F/_ x A
Assertion	nfwlim	|- F/_ x WLim ( R , A )

Proof

Step	Hyp	Ref	Expression
1		nfwlim.1	|- F/_ x R
2		nfwlim.2	|- F/_ x A
3		df-wlim	|- WLim ( R , A ) = { y e. A | ( y =/= inf ( A , A , R ) /\ y = sup ( Pred ( R , A , y ) , A , R ) ) }
4		nfcv	|- F/_ x y
5	2 2 1	nfinf	|- F/_ x inf ( A , A , R )
6	4 5	nfne	|- F/ x y =/= inf ( A , A , R )
7	1 2 4	nfpred	|- F/_ x Pred ( R , A , y )
8	7 2 1	nfsup	|- F/_ x sup ( Pred ( R , A , y ) , A , R )
9	8	nfeq2	|- F/ x y = sup ( Pred ( R , A , y ) , A , R )
10	6 9	nfan	|- F/ x ( y =/= inf ( A , A , R ) /\ y = sup ( Pred ( R , A , y ) , A , R ) )
11	10 2	nfrabw	|- F/_ x { y e. A | ( y =/= inf ( A , A , R ) /\ y = sup ( Pred ( R , A , y ) , A , R ) ) }
12	3 11	nfcxfr	|- F/_ x WLim ( R , A )