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

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 ) )