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