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	⊢ Ⅎ 𝑥 𝑅
	nfwlim.2	⊢ Ⅎ 𝑥 𝐴
Assertion	nfwlim	⊢ Ⅎ 𝑥 WLim ( 𝑅 , 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		nfwlim.1	⊢ Ⅎ 𝑥 𝑅
2		nfwlim.2	⊢ Ⅎ 𝑥 𝐴
3		df-wlim	⊢ WLim ( 𝑅 , 𝐴 ) = { 𝑦 ∈ 𝐴 ∣ ( 𝑦 ≠ inf ( 𝐴 , 𝐴 , 𝑅 ) ∧ 𝑦 = sup ( Pred ( 𝑅 , 𝐴 , 𝑦 ) , 𝐴 , 𝑅 ) ) }
4		nfcv	⊢ Ⅎ 𝑥 𝑦
5	2 2 1	nfinf	⊢ Ⅎ 𝑥 inf ( 𝐴 , 𝐴 , 𝑅 )
6	4 5	nfne	⊢ Ⅎ 𝑥 𝑦 ≠ inf ( 𝐴 , 𝐴 , 𝑅 )
7	1 2 4	nfpred	⊢ Ⅎ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 )
8	7 2 1	nfsup	⊢ Ⅎ 𝑥 sup ( Pred ( 𝑅 , 𝐴 , 𝑦 ) , 𝐴 , 𝑅 )
9	8	nfeq2	⊢ Ⅎ 𝑥 𝑦 = sup ( Pred ( 𝑅 , 𝐴 , 𝑦 ) , 𝐴 , 𝑅 )
10	6 9	nfan	⊢ Ⅎ 𝑥 ( 𝑦 ≠ inf ( 𝐴 , 𝐴 , 𝑅 ) ∧ 𝑦 = sup ( Pred ( 𝑅 , 𝐴 , 𝑦 ) , 𝐴 , 𝑅 ) )
11	10 2	nfrabw	⊢ Ⅎ 𝑥 { 𝑦 ∈ 𝐴 ∣ ( 𝑦 ≠ inf ( 𝐴 , 𝐴 , 𝑅 ) ∧ 𝑦 = sup ( Pred ( 𝑅 , 𝐴 , 𝑦 ) , 𝐴 , 𝑅 ) ) }
12	3 11	nfcxfr	⊢ Ⅎ 𝑥 WLim ( 𝑅 , 𝐴 )