Metamath Proof Explorer

Theorem ovg

Description: The value of an operation class abstraction. (Contributed by Jeff Madsen, 10-Jun-2010)

Ref Expression
Hypotheses ovg.1 
|- ( x = A -> ( ph <-> ps ) )
ovg.2 
|- ( y = B -> ( ps <-> ch ) )
ovg.3 
|- ( z = C -> ( ch <-> th ) )
ovg.4 
|- ( ( ta /\ ( x e. R /\ y e. S ) ) -> E! z ph )
ovg.5 
|- F = { <. <. x , y >. , z >. | ( ( x e. R /\ y e. S ) /\ ph ) }
Assertion ovg 
|- ( ( ta /\ ( A e. R /\ B e. S /\ C e. D ) ) -> ( ( A F B ) = C <-> th ) )

Proof

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