This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ov

Description: The value of an operation class abstraction. (Contributed by NM, 16-May-1995) (Revised by David Abernethy, 19-Jun-2012)

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

Proof

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