Step |
Hyp |
Ref |
Expression |
1 |
|
ov.1 |
|- C e. _V |
2 |
|
ov.2 |
|- ( x = A -> ( ph <-> ps ) ) |
3 |
|
ov.3 |
|- ( y = B -> ( ps <-> ch ) ) |
4 |
|
ov.4 |
|- ( z = C -> ( ch <-> th ) ) |
5 |
|
ov.5 |
|- ( ( x e. R /\ y e. S ) -> E! z ph ) |
6 |
|
ov.6 |
|- F = { <. <. x , y >. , z >. | ( ( x e. R /\ y e. S ) /\ ph ) } |
7 |
|
df-ov |
|- ( A F B ) = ( F ` <. A , B >. ) |
8 |
6
|
fveq1i |
|- ( F ` <. A , B >. ) = ( { <. <. x , y >. , z >. | ( ( x e. R /\ y e. S ) /\ ph ) } ` <. A , B >. ) |
9 |
7 8
|
eqtri |
|- ( A F B ) = ( { <. <. x , y >. , z >. | ( ( x e. R /\ y e. S ) /\ ph ) } ` <. A , B >. ) |
10 |
9
|
eqeq1i |
|- ( ( A F B ) = C <-> ( { <. <. x , y >. , z >. | ( ( x e. R /\ y e. S ) /\ ph ) } ` <. A , B >. ) = C ) |
11 |
5
|
fnoprab |
|- { <. <. x , y >. , z >. | ( ( x e. R /\ y e. S ) /\ ph ) } Fn { <. x , y >. | ( x e. R /\ y e. S ) } |
12 |
|
eleq1 |
|- ( x = A -> ( x e. R <-> A e. R ) ) |
13 |
12
|
anbi1d |
|- ( x = A -> ( ( x e. R /\ y e. S ) <-> ( A e. R /\ y e. S ) ) ) |
14 |
|
eleq1 |
|- ( y = B -> ( y e. S <-> B e. S ) ) |
15 |
14
|
anbi2d |
|- ( y = B -> ( ( A e. R /\ y e. S ) <-> ( A e. R /\ B e. S ) ) ) |
16 |
13 15
|
opelopabg |
|- ( ( A e. R /\ B e. S ) -> ( <. A , B >. e. { <. x , y >. | ( x e. R /\ y e. S ) } <-> ( A e. R /\ B e. S ) ) ) |
17 |
16
|
ibir |
|- ( ( A e. R /\ B e. S ) -> <. A , B >. e. { <. x , y >. | ( x e. R /\ y e. S ) } ) |
18 |
|
fnopfvb |
|- ( ( { <. <. x , y >. , z >. | ( ( x e. R /\ y e. S ) /\ ph ) } Fn { <. x , y >. | ( x e. R /\ y e. S ) } /\ <. A , B >. e. { <. x , y >. | ( x e. R /\ y e. S ) } ) -> ( ( { <. <. x , y >. , z >. | ( ( x e. R /\ y e. S ) /\ ph ) } ` <. A , B >. ) = C <-> <. <. A , B >. , C >. e. { <. <. x , y >. , z >. | ( ( x e. R /\ y e. S ) /\ ph ) } ) ) |
19 |
11 17 18
|
sylancr |
|- ( ( A e. R /\ B e. S ) -> ( ( { <. <. x , y >. , z >. | ( ( x e. R /\ y e. S ) /\ ph ) } ` <. A , B >. ) = C <-> <. <. A , B >. , C >. e. { <. <. x , y >. , z >. | ( ( x e. R /\ y e. S ) /\ ph ) } ) ) |
20 |
13 2
|
anbi12d |
|- ( x = A -> ( ( ( x e. R /\ y e. S ) /\ ph ) <-> ( ( A e. R /\ y e. S ) /\ ps ) ) ) |
21 |
15 3
|
anbi12d |
|- ( y = B -> ( ( ( A e. R /\ y e. S ) /\ ps ) <-> ( ( A e. R /\ B e. S ) /\ ch ) ) ) |
22 |
4
|
anbi2d |
|- ( z = C -> ( ( ( A e. R /\ B e. S ) /\ ch ) <-> ( ( A e. R /\ B e. S ) /\ th ) ) ) |
23 |
20 21 22
|
eloprabg |
|- ( ( A e. R /\ B e. S /\ C e. _V ) -> ( <. <. A , B >. , C >. e. { <. <. x , y >. , z >. | ( ( x e. R /\ y e. S ) /\ ph ) } <-> ( ( A e. R /\ B e. S ) /\ th ) ) ) |
24 |
1 23
|
mp3an3 |
|- ( ( A e. R /\ B e. S ) -> ( <. <. A , B >. , C >. e. { <. <. x , y >. , z >. | ( ( x e. R /\ y e. S ) /\ ph ) } <-> ( ( A e. R /\ B e. S ) /\ th ) ) ) |
25 |
19 24
|
bitrd |
|- ( ( A e. R /\ B e. S ) -> ( ( { <. <. x , y >. , z >. | ( ( x e. R /\ y e. S ) /\ ph ) } ` <. A , B >. ) = C <-> ( ( A e. R /\ B e. S ) /\ th ) ) ) |
26 |
10 25
|
syl5bb |
|- ( ( A e. R /\ B e. S ) -> ( ( A F B ) = C <-> ( ( A e. R /\ B e. S ) /\ th ) ) ) |
27 |
26
|
bianabs |
|- ( ( A e. R /\ B e. S ) -> ( ( A F B ) = C <-> th ) ) |