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