Step |
Hyp |
Ref |
Expression |
1 |
|
resoprab |
|- ( { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ ph ) } |` ( C X. D ) ) = { <. <. x , y >. , z >. | ( ( x e. C /\ y e. D ) /\ ( ( x e. A /\ y e. B ) /\ ph ) ) } |
2 |
|
anass |
|- ( ( ( ( x e. C /\ y e. D ) /\ ( x e. A /\ y e. B ) ) /\ ph ) <-> ( ( x e. C /\ y e. D ) /\ ( ( x e. A /\ y e. B ) /\ ph ) ) ) |
3 |
|
an4 |
|- ( ( ( x e. C /\ y e. D ) /\ ( x e. A /\ y e. B ) ) <-> ( ( x e. C /\ x e. A ) /\ ( y e. D /\ y e. B ) ) ) |
4 |
|
ssel |
|- ( C C_ A -> ( x e. C -> x e. A ) ) |
5 |
4
|
pm4.71d |
|- ( C C_ A -> ( x e. C <-> ( x e. C /\ x e. A ) ) ) |
6 |
5
|
bicomd |
|- ( C C_ A -> ( ( x e. C /\ x e. A ) <-> x e. C ) ) |
7 |
|
ssel |
|- ( D C_ B -> ( y e. D -> y e. B ) ) |
8 |
7
|
pm4.71d |
|- ( D C_ B -> ( y e. D <-> ( y e. D /\ y e. B ) ) ) |
9 |
8
|
bicomd |
|- ( D C_ B -> ( ( y e. D /\ y e. B ) <-> y e. D ) ) |
10 |
6 9
|
bi2anan9 |
|- ( ( C C_ A /\ D C_ B ) -> ( ( ( x e. C /\ x e. A ) /\ ( y e. D /\ y e. B ) ) <-> ( x e. C /\ y e. D ) ) ) |
11 |
3 10
|
syl5bb |
|- ( ( C C_ A /\ D C_ B ) -> ( ( ( x e. C /\ y e. D ) /\ ( x e. A /\ y e. B ) ) <-> ( x e. C /\ y e. D ) ) ) |
12 |
11
|
anbi1d |
|- ( ( C C_ A /\ D C_ B ) -> ( ( ( ( x e. C /\ y e. D ) /\ ( x e. A /\ y e. B ) ) /\ ph ) <-> ( ( x e. C /\ y e. D ) /\ ph ) ) ) |
13 |
2 12
|
bitr3id |
|- ( ( C C_ A /\ D C_ B ) -> ( ( ( x e. C /\ y e. D ) /\ ( ( x e. A /\ y e. B ) /\ ph ) ) <-> ( ( x e. C /\ y e. D ) /\ ph ) ) ) |
14 |
13
|
oprabbidv |
|- ( ( C C_ A /\ D C_ B ) -> { <. <. x , y >. , z >. | ( ( x e. C /\ y e. D ) /\ ( ( x e. A /\ y e. B ) /\ ph ) ) } = { <. <. x , y >. , z >. | ( ( x e. C /\ y e. D ) /\ ph ) } ) |
15 |
1 14
|
eqtrid |
|- ( ( C C_ A /\ D C_ B ) -> ( { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ ph ) } |` ( C X. D ) ) = { <. <. x , y >. , z >. | ( ( x e. C /\ y e. D ) /\ ph ) } ) |