Metamath Proof Explorer

Theorem ov6g

Description: The value of an operation class abstraction. Special case. (Contributed by NM, 13-Nov-2006)

Ref Expression
Hypotheses ov6g.1 
|- ( <. x , y >. = <. A , B >. -> R = S )
ov6g.2 
|- F = { <. <. x , y >. , z >. | ( <. x , y >. e. C /\ z = R ) }
Assertion ov6g 
|- ( ( ( A e. G /\ B e. H /\ <. A , B >. e. C ) /\ S e. J ) -> ( A F B ) = S )

Proof

Step Hyp Ref Expression
1 ov6g.1 
 |-  ( <. x , y >. = <. A , B >. -> R = S )
2 ov6g.2 
 |-  F = { <. <. x , y >. , z >. | ( <. x , y >. e. C /\ z = R ) }
3 df-ov 
 |-  ( A F B ) = ( F ` <. A , B >. )
4 eqid 
 |-  S = S
5 biidd 
 |-  ( ( x = A /\ y = B ) -> ( S = S <-> S = S ) )
6 5 copsex2g 
 |-  ( ( A e. G /\ B e. H ) -> ( E. x E. y ( <. A , B >. = <. x , y >. /\ S = S ) <-> S = S ) )
7 4 6 mpbiri 
 |-  ( ( A e. G /\ B e. H ) -> E. x E. y ( <. A , B >. = <. x , y >. /\ S = S ) )
8 7 3adant3 
 |-  ( ( A e. G /\ B e. H /\ <. A , B >. e. C ) -> E. x E. y ( <. A , B >. = <. x , y >. /\ S = S ) )
9 8 adantr 
 |-  ( ( ( A e. G /\ B e. H /\ <. A , B >. e. C ) /\ S e. J ) -> E. x E. y ( <. A , B >. = <. x , y >. /\ S = S ) )
10 eqeq1 
 |-  ( w = <. A , B >. -> ( w = <. x , y >. <-> <. A , B >. = <. x , y >. ) )
11 10 anbi1d 
 |-  ( w = <. A , B >. -> ( ( w = <. x , y >. /\ z = R ) <-> ( <. A , B >. = <. x , y >. /\ z = R ) ) )
12 1 eqeq2d 
 |-  ( <. x , y >. = <. A , B >. -> ( z = R <-> z = S ) )
13 12 eqcoms 
 |-  ( <. A , B >. = <. x , y >. -> ( z = R <-> z = S ) )
14 13 pm5.32i 
 |-  ( ( <. A , B >. = <. x , y >. /\ z = R ) <-> ( <. A , B >. = <. x , y >. /\ z = S ) )
15 11 14 bitrdi 
 |-  ( w = <. A , B >. -> ( ( w = <. x , y >. /\ z = R ) <-> ( <. A , B >. = <. x , y >. /\ z = S ) ) )
16 15 2exbidv 
 |-  ( w = <. A , B >. -> ( E. x E. y ( w = <. x , y >. /\ z = R ) <-> E. x E. y ( <. A , B >. = <. x , y >. /\ z = S ) ) )
17 eqeq1 
 |-  ( z = S -> ( z = S <-> S = S ) )
18 17 anbi2d 
 |-  ( z = S -> ( ( <. A , B >. = <. x , y >. /\ z = S ) <-> ( <. A , B >. = <. x , y >. /\ S = S ) ) )
19 18 2exbidv 
 |-  ( z = S -> ( E. x E. y ( <. A , B >. = <. x , y >. /\ z = S ) <-> E. x E. y ( <. A , B >. = <. x , y >. /\ S = S ) ) )
20 moeq 
 |-  E* z z = R
21 20 mosubop 
 |-  E* z E. x E. y ( w = <. x , y >. /\ z = R )
22 21 a1i 
 |-  ( w e. C -> E* z E. x E. y ( w = <. x , y >. /\ z = R ) )
23 dfoprab2 
 |-  { <. <. x , y >. , z >. | ( <. x , y >. e. C /\ z = R ) } = { <. w , z >. | E. x E. y ( w = <. x , y >. /\ ( <. x , y >. e. C /\ z = R ) ) }
24 eleq1 
 |-  ( w = <. x , y >. -> ( w e. C <-> <. x , y >. e. C ) )
25 24 anbi1d 
 |-  ( w = <. x , y >. -> ( ( w e. C /\ z = R ) <-> ( <. x , y >. e. C /\ z = R ) ) )
26 25 pm5.32i 
 |-  ( ( w = <. x , y >. /\ ( w e. C /\ z = R ) ) <-> ( w = <. x , y >. /\ ( <. x , y >. e. C /\ z = R ) ) )
27 an12 
 |-  ( ( w = <. x , y >. /\ ( w e. C /\ z = R ) ) <-> ( w e. C /\ ( w = <. x , y >. /\ z = R ) ) )
28 26 27 bitr3i 
 |-  ( ( w = <. x , y >. /\ ( <. x , y >. e. C /\ z = R ) ) <-> ( w e. C /\ ( w = <. x , y >. /\ z = R ) ) )
29 28 2exbii 
 |-  ( E. x E. y ( w = <. x , y >. /\ ( <. x , y >. e. C /\ z = R ) ) <-> E. x E. y ( w e. C /\ ( w = <. x , y >. /\ z = R ) ) )
30 19.42vv 
 |-  ( E. x E. y ( w e. C /\ ( w = <. x , y >. /\ z = R ) ) <-> ( w e. C /\ E. x E. y ( w = <. x , y >. /\ z = R ) ) )
31 29 30 bitri 
 |-  ( E. x E. y ( w = <. x , y >. /\ ( <. x , y >. e. C /\ z = R ) ) <-> ( w e. C /\ E. x E. y ( w = <. x , y >. /\ z = R ) ) )
32 31 opabbii 
 |-  { <. w , z >. | E. x E. y ( w = <. x , y >. /\ ( <. x , y >. e. C /\ z = R ) ) } = { <. w , z >. | ( w e. C /\ E. x E. y ( w = <. x , y >. /\ z = R ) ) }
33 2 23 32 3eqtri 
 |-  F = { <. w , z >. | ( w e. C /\ E. x E. y ( w = <. x , y >. /\ z = R ) ) }
34 16 19 22 33 fvopab3ig 
 |-  ( ( <. A , B >. e. C /\ S e. J ) -> ( E. x E. y ( <. A , B >. = <. x , y >. /\ S = S ) -> ( F ` <. A , B >. ) = S ) )
35 34 3ad2antl3 
 |-  ( ( ( A e. G /\ B e. H /\ <. A , B >. e. C ) /\ S e. J ) -> ( E. x E. y ( <. A , B >. = <. x , y >. /\ S = S ) -> ( F ` <. A , B >. ) = S ) )
36 9 35 mpd 
 |-  ( ( ( A e. G /\ B e. H /\ <. A , B >. e. C ) /\ S e. J ) -> ( F ` <. A , B >. ) = S )
37 3 36 syl5eq 
 |-  ( ( ( A e. G /\ B e. H /\ <. A , B >. e. C ) /\ S e. J ) -> ( A F B ) = S )