Metamath Proof Explorer


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 ( 𝑅 , 𝐴 )