Metamath Proof Explorer

Theorem wlimeq12

Description: Equality theorem for the limit class. (Contributed by Scott Fenton, 15-Jun-2018) (Proof shortened by AV, 10-Oct-2021)

Ref Expression
Assertion wlimeq12 
|- ( ( R = S /\ A = B ) -> WLim ( R , A ) = WLim ( S , B ) )

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( R = S /\ A = B ) -> A = B )
2 simpl 
 |-  ( ( R = S /\ A = B ) -> R = S )
3 1 1 2 infeq123d 
 |-  ( ( R = S /\ A = B ) -> inf ( A , A , R ) = inf ( B , B , S ) )
4 3 neeq2d 
 |-  ( ( R = S /\ A = B ) -> ( x =/= inf ( A , A , R ) <-> x =/= inf ( B , B , S ) ) )
5 equid 
 |-  x = x
6 predeq123 
 |-  ( ( R = S /\ A = B /\ x = x ) -> Pred ( R , A , x ) = Pred ( S , B , x ) )
7 5 6 mp3an3 
 |-  ( ( R = S /\ A = B ) -> Pred ( R , A , x ) = Pred ( S , B , x ) )
8 7 1 2 supeq123d 
 |-  ( ( R = S /\ A = B ) -> sup ( Pred ( R , A , x ) , A , R ) = sup ( Pred ( S , B , x ) , B , S ) )
9 8 eqeq2d 
 |-  ( ( R = S /\ A = B ) -> ( x = sup ( Pred ( R , A , x ) , A , R ) <-> x = sup ( Pred ( S , B , x ) , B , S ) ) )
10 4 9 anbi12d 
 |-  ( ( R = S /\ A = B ) -> ( ( x =/= inf ( A , A , R ) /\ x = sup ( Pred ( R , A , x ) , A , R ) ) <-> ( x =/= inf ( B , B , S ) /\ x = sup ( Pred ( S , B , x ) , B , S ) ) ) )
11 1 10 rabeqbidv 
 |-  ( ( R = S /\ A = B ) -> { x e. A | ( x =/= inf ( A , A , R ) /\ x = sup ( Pred ( R , A , x ) , A , R ) ) } = { x e. B | ( x =/= inf ( B , B , S ) /\ x = sup ( Pred ( S , B , x ) , B , S ) ) } )
12 df-wlim 
 |-  WLim ( R , A ) = { x e. A | ( x =/= inf ( A , A , R ) /\ x = sup ( Pred ( R , A , x ) , A , R ) ) }
13 df-wlim 
 |-  WLim ( S , B ) = { x e. B | ( x =/= inf ( B , B , S ) /\ x = sup ( Pred ( S , B , x ) , B , S ) ) }
14 11 12 13 3eqtr4g 
 |-  ( ( R = S /\ A = B ) -> WLim ( R , A ) = WLim ( S , B ) )