Step |
Hyp |
Ref |
Expression |
1 |
|
ovg.1 |
|- ( x = A -> ( ph <-> ps ) ) |
2 |
|
ovg.2 |
|- ( y = B -> ( ps <-> ch ) ) |
3 |
|
ovg.3 |
|- ( z = C -> ( ch <-> th ) ) |
4 |
|
ovg.4 |
|- ( ( ta /\ ( x e. R /\ y e. S ) ) -> E! z ph ) |
5 |
|
ovg.5 |
|- F = { <. <. x , y >. , z >. | ( ( x e. R /\ y e. S ) /\ ph ) } |
6 |
|
df-ov |
|- ( A F B ) = ( F ` <. A , B >. ) |
7 |
5
|
fveq1i |
|- ( F ` <. A , B >. ) = ( { <. <. x , y >. , z >. | ( ( x e. R /\ y e. S ) /\ ph ) } ` <. A , B >. ) |
8 |
6 7
|
eqtri |
|- ( A F B ) = ( { <. <. x , y >. , z >. | ( ( x e. R /\ y e. S ) /\ ph ) } ` <. A , B >. ) |
9 |
8
|
eqeq1i |
|- ( ( A F B ) = C <-> ( { <. <. x , y >. , z >. | ( ( x e. R /\ y e. S ) /\ ph ) } ` <. A , B >. ) = C ) |
10 |
|
eqeq2 |
|- ( c = C -> ( ( { <. <. x , y >. , z >. | ( ( x e. R /\ y e. S ) /\ ph ) } ` <. A , B >. ) = c <-> ( { <. <. x , y >. , z >. | ( ( x e. R /\ y e. S ) /\ ph ) } ` <. A , B >. ) = C ) ) |
11 |
|
opeq2 |
|- ( c = C -> <. <. A , B >. , c >. = <. <. A , B >. , C >. ) |
12 |
11
|
eleq1d |
|- ( c = C -> ( <. <. A , B >. , c >. e. { <. <. x , y >. , z >. | ( ( x e. R /\ y e. S ) /\ ph ) } <-> <. <. A , B >. , C >. e. { <. <. x , y >. , z >. | ( ( x e. R /\ y e. S ) /\ ph ) } ) ) |
13 |
10 12
|
bibi12d |
|- ( c = C -> ( ( ( { <. <. 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 ) } ) <-> ( ( { <. <. 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 ) } ) ) ) |
14 |
13
|
imbi2d |
|- ( c = C -> ( ( ( ta /\ ( 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 ) } ) ) <-> ( ( ta /\ ( 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 ) } ) ) ) ) |
15 |
4
|
ex |
|- ( ta -> ( ( x e. R /\ y e. S ) -> E! z ph ) ) |
16 |
15
|
alrimivv |
|- ( ta -> A. x A. y ( ( x e. R /\ y e. S ) -> E! z ph ) ) |
17 |
|
fnoprabg |
|- ( A. x A. y ( ( x e. R /\ y e. S ) -> E! z ph ) -> { <. <. x , y >. , z >. | ( ( x e. R /\ y e. S ) /\ ph ) } Fn { <. x , y >. | ( x e. R /\ y e. S ) } ) |
18 |
16 17
|
syl |
|- ( ta -> { <. <. x , y >. , z >. | ( ( x e. R /\ y e. S ) /\ ph ) } Fn { <. x , y >. | ( x e. R /\ y e. S ) } ) |
19 |
|
eleq1 |
|- ( x = A -> ( x e. R <-> A e. R ) ) |
20 |
19
|
anbi1d |
|- ( x = A -> ( ( x e. R /\ y e. S ) <-> ( A e. R /\ y e. S ) ) ) |
21 |
|
eleq1 |
|- ( y = B -> ( y e. S <-> B e. S ) ) |
22 |
21
|
anbi2d |
|- ( y = B -> ( ( A e. R /\ y e. S ) <-> ( A e. R /\ B e. S ) ) ) |
23 |
20 22
|
opelopabg |
|- ( ( A e. R /\ B e. S ) -> ( <. A , B >. e. { <. x , y >. | ( x e. R /\ y e. S ) } <-> ( A e. R /\ B e. S ) ) ) |
24 |
23
|
ibir |
|- ( ( A e. R /\ B e. S ) -> <. A , B >. e. { <. x , y >. | ( x e. R /\ y e. S ) } ) |
25 |
|
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 ) } ) ) |
26 |
18 24 25
|
syl2an |
|- ( ( ta /\ ( 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 ) } ) ) |
27 |
14 26
|
vtoclg |
|- ( C e. D -> ( ( ta /\ ( 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 ) } ) ) ) |
28 |
27
|
com12 |
|- ( ( ta /\ ( A e. R /\ B e. S ) ) -> ( C e. D -> ( ( { <. <. 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 ) } ) ) ) |
29 |
28
|
exp32 |
|- ( ta -> ( A e. R -> ( B e. S -> ( C e. D -> ( ( { <. <. 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 ) } ) ) ) ) ) |
30 |
29
|
3imp2 |
|- ( ( ta /\ ( A e. R /\ B e. S /\ C e. D ) ) -> ( ( { <. <. 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 ) } ) ) |
31 |
20 1
|
anbi12d |
|- ( x = A -> ( ( ( x e. R /\ y e. S ) /\ ph ) <-> ( ( A e. R /\ y e. S ) /\ ps ) ) ) |
32 |
22 2
|
anbi12d |
|- ( y = B -> ( ( ( A e. R /\ y e. S ) /\ ps ) <-> ( ( A e. R /\ B e. S ) /\ ch ) ) ) |
33 |
3
|
anbi2d |
|- ( z = C -> ( ( ( A e. R /\ B e. S ) /\ ch ) <-> ( ( A e. R /\ B e. S ) /\ th ) ) ) |
34 |
31 32 33
|
eloprabg |
|- ( ( A e. R /\ B e. S /\ C e. D ) -> ( <. <. A , B >. , C >. e. { <. <. x , y >. , z >. | ( ( x e. R /\ y e. S ) /\ ph ) } <-> ( ( A e. R /\ B e. S ) /\ th ) ) ) |
35 |
34
|
adantl |
|- ( ( ta /\ ( A e. R /\ B e. S /\ C e. D ) ) -> ( <. <. A , B >. , C >. e. { <. <. x , y >. , z >. | ( ( x e. R /\ y e. S ) /\ ph ) } <-> ( ( A e. R /\ B e. S ) /\ th ) ) ) |
36 |
30 35
|
bitrd |
|- ( ( ta /\ ( A e. R /\ B e. S /\ C e. D ) ) -> ( ( { <. <. x , y >. , z >. | ( ( x e. R /\ y e. S ) /\ ph ) } ` <. A , B >. ) = C <-> ( ( A e. R /\ B e. S ) /\ th ) ) ) |
37 |
9 36
|
syl5bb |
|- ( ( ta /\ ( A e. R /\ B e. S /\ C e. D ) ) -> ( ( A F B ) = C <-> ( ( A e. R /\ B e. S ) /\ th ) ) ) |
38 |
|
biidd |
|- ( ( A e. R /\ B e. S ) -> ( ( ( A e. R /\ B e. S ) /\ th ) <-> ( ( A e. R /\ B e. S ) /\ th ) ) ) |
39 |
38
|
bianabs |
|- ( ( A e. R /\ B e. S ) -> ( ( ( A e. R /\ B e. S ) /\ th ) <-> th ) ) |
40 |
39
|
3adant3 |
|- ( ( A e. R /\ B e. S /\ C e. D ) -> ( ( ( A e. R /\ B e. S ) /\ th ) <-> th ) ) |
41 |
40
|
adantl |
|- ( ( ta /\ ( A e. R /\ B e. S /\ C e. D ) ) -> ( ( ( A e. R /\ B e. S ) /\ th ) <-> th ) ) |
42 |
37 41
|
bitrd |
|- ( ( ta /\ ( A e. R /\ B e. S /\ C e. D ) ) -> ( ( A F B ) = C <-> th ) ) |