This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem supeq3

Description: Equality theorem for supremum. (Contributed by Scott Fenton, 13-Jun-2018)

Ref Expression
Assertion supeq3 
|- ( R = S -> sup ( A , B , R ) = sup ( A , B , S ) )

Proof

Step Hyp Ref Expression
1 breq 
 |-  ( R = S -> ( x R y <-> x S y ) )
2 1 notbid 
 |-  ( R = S -> ( -. x R y <-> -. x S y ) )
3 2 ralbidv 
 |-  ( R = S -> ( A. y e. A -. x R y <-> A. y e. A -. x S y ) )
4 breq 
 |-  ( R = S -> ( y R x <-> y S x ) )
5 breq 
 |-  ( R = S -> ( y R z <-> y S z ) )
6 5 rexbidv 
 |-  ( R = S -> ( E. z e. A y R z <-> E. z e. A y S z ) )
7 4 6 imbi12d 
 |-  ( R = S -> ( ( y R x -> E. z e. A y R z ) <-> ( y S x -> E. z e. A y S z ) ) )
8 7 ralbidv 
 |-  ( R = S -> ( A. y e. B ( y R x -> E. z e. A y R z ) <-> A. y e. B ( y S x -> E. z e. A y S z ) ) )
9 3 8 anbi12d 
 |-  ( R = S -> ( ( A. y e. A -. x R y /\ A. y e. B ( y R x -> E. z e. A y R z ) ) <-> ( A. y e. A -. x S y /\ A. y e. B ( y S x -> E. z e. A y S z ) ) ) )
10 9 rabbidv 
 |-  ( R = S -> { x e. B | ( A. y e. A -. x R y /\ A. y e. B ( y R x -> E. z e. A y R z ) ) } = { x e. B | ( A. y e. A -. x S y /\ A. y e. B ( y S x -> E. z e. A y S z ) ) } )
11 10 unieqd 
 |-  ( R = S -> U. { x e. B | ( A. y e. A -. x R y /\ A. y e. B ( y R x -> E. z e. A y R z ) ) } = U. { x e. B | ( A. y e. A -. x S y /\ A. y e. B ( y S x -> E. z e. A y S z ) ) } )
12 df-sup 
 |-  sup ( A , B , R ) = U. { x e. B | ( A. y e. A -. x R y /\ A. y e. B ( y R x -> E. z e. A y R z ) ) }
13 df-sup 
 |-  sup ( A , B , S ) = U. { x e. B | ( A. y e. A -. x S y /\ A. y e. B ( y S x -> E. z e. A y S z ) ) }
14 11 12 13 3eqtr4g 
 |-  ( R = S -> sup ( A , B , R ) = sup ( A , B , S ) )