Step |
Hyp |
Ref |
Expression |
1 |
|
neeq1 |
|- ( x = X -> ( x =/= inf ( A , A , R ) <-> X =/= inf ( 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 =/= inf ( A , A , R ) /\ x = sup ( Pred ( R , A , x ) , A , R ) ) <-> ( X =/= inf ( A , A , R ) /\ X = sup ( Pred ( R , A , X ) , A , R ) ) ) ) |
7 |
|
df-wlim |
|- WLim ( R , A ) = { x e. A | ( x =/= inf ( A , A , R ) /\ x = sup ( Pred ( R , A , x ) , A , R ) ) } |
8 |
6 7
|
elrab2 |
|- ( X e. WLim ( R , A ) <-> ( X e. A /\ ( X =/= inf ( A , A , R ) /\ X = sup ( Pred ( R , A , X ) , A , R ) ) ) ) |
9 |
|
3anass |
|- ( ( X e. A /\ X =/= inf ( A , A , R ) /\ X = sup ( Pred ( R , A , X ) , A , R ) ) <-> ( X e. A /\ ( X =/= inf ( A , A , R ) /\ X = sup ( Pred ( R , A , X ) , A , R ) ) ) ) |
10 |
8 9
|
bitr4i |
|- ( X e. WLim ( R , A ) <-> ( X e. A /\ X =/= inf ( A , A , R ) /\ X = sup ( Pred ( R , A , X ) , A , R ) ) ) |