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 eqtrid
 |-  ( ( ( A e. G /\ B e. H /\ <. A , B >. e. C ) /\ S e. J ) -> ( A F B ) = S )