Metamath Proof Explorer


Theorem elwlim

Description: Membership in the limit class. (Contributed by Scott Fenton, 15-Jun-2018) (Revised by AV, 10-Oct-2021)

Ref Expression
Assertion elwlim X WLim R A X A X sup A A R X = sup Pred R A X A R

Proof

Step Hyp Ref Expression
1 neeq1 x = X x sup A A R X sup A A R
2 id x = X x = X
3 predeq3 x = X Pred R A x = Pred R A X
4 3 supeq1d x = X sup Pred R A x A R = sup Pred R A X A R
5 2 4 eqeq12d x = X x = sup Pred R A x A R X = sup Pred R A X A R
6 1 5 anbi12d x = X x sup A A R x = sup Pred R A x A R X sup A A R X = sup Pred R A X A R
7 df-wlim WLim R A = x A | x sup A A R x = sup Pred R A x A R
8 6 7 elrab2 X WLim R A X A X sup A A R X = sup Pred R A X A R
9 3anass X A X sup A A R X = sup Pred R A X A R X A X sup A A R X = sup Pred R A X A R
10 8 9 bitr4i X WLim R A X A X sup A A R X = sup Pred R A X A R