Metamath Proof Explorer


Theorem supeq123d

Description: Equality deduction for supremum. (Contributed by Stefan O'Rear, 20-Jan-2015)

Ref Expression
Hypotheses supeq123d.a
|- ( ph -> A = D )
supeq123d.b
|- ( ph -> B = E )
supeq123d.c
|- ( ph -> C = F )
Assertion supeq123d
|- ( ph -> sup ( A , B , C ) = sup ( D , E , F ) )

Proof

Step Hyp Ref Expression
1 supeq123d.a
 |-  ( ph -> A = D )
2 supeq123d.b
 |-  ( ph -> B = E )
3 supeq123d.c
 |-  ( ph -> C = F )
4 3 breqd
 |-  ( ph -> ( x C y <-> x F y ) )
5 4 notbid
 |-  ( ph -> ( -. x C y <-> -. x F y ) )
6 1 5 raleqbidv
 |-  ( ph -> ( A. y e. A -. x C y <-> A. y e. D -. x F y ) )
7 3 breqd
 |-  ( ph -> ( y C x <-> y F x ) )
8 3 breqd
 |-  ( ph -> ( y C z <-> y F z ) )
9 1 8 rexeqbidv
 |-  ( ph -> ( E. z e. A y C z <-> E. z e. D y F z ) )
10 7 9 imbi12d
 |-  ( ph -> ( ( y C x -> E. z e. A y C z ) <-> ( y F x -> E. z e. D y F z ) ) )
11 2 10 raleqbidv
 |-  ( ph -> ( A. y e. B ( y C x -> E. z e. A y C z ) <-> A. y e. E ( y F x -> E. z e. D y F z ) ) )
12 6 11 anbi12d
 |-  ( ph -> ( ( A. y e. A -. x C y /\ A. y e. B ( y C x -> E. z e. A y C z ) ) <-> ( A. y e. D -. x F y /\ A. y e. E ( y F x -> E. z e. D y F z ) ) ) )
13 2 12 rabeqbidv
 |-  ( ph -> { x e. B | ( A. y e. A -. x C y /\ A. y e. B ( y C x -> E. z e. A y C z ) ) } = { x e. E | ( A. y e. D -. x F y /\ A. y e. E ( y F x -> E. z e. D y F z ) ) } )
14 13 unieqd
 |-  ( ph -> U. { x e. B | ( A. y e. A -. x C y /\ A. y e. B ( y C x -> E. z e. A y C z ) ) } = U. { x e. E | ( A. y e. D -. x F y /\ A. y e. E ( y F x -> E. z e. D y F z ) ) } )
15 df-sup
 |-  sup ( A , B , C ) = U. { x e. B | ( A. y e. A -. x C y /\ A. y e. B ( y C x -> E. z e. A y C z ) ) }
16 df-sup
 |-  sup ( D , E , F ) = U. { x e. E | ( A. y e. D -. x F y /\ A. y e. E ( y F x -> E. z e. D y F z ) ) }
17 14 15 16 3eqtr4g
 |-  ( ph -> sup ( A , B , C ) = sup ( D , E , F ) )