Metamath Proof Explorer

Theorem ov3

Description: The value of an operation class abstraction. Special case. (Contributed by NM, 28-May-1995) (Revised by Mario Carneiro, 29-Dec-2014)

Ref Expression
Hypotheses ov3.1 
|- S e. _V
ov3.2 
|- ( ( ( w = A /\ v = B ) /\ ( u = C /\ f = D ) ) -> R = S )
ov3.3 
|- F = { <. <. x , y >. , z >. | ( ( x e. ( H X. H ) /\ y e. ( H X. H ) ) /\ E. w E. v E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = R ) ) }
Assertion ov3 
|- ( ( ( A e. H /\ B e. H ) /\ ( C e. H /\ D e. H ) ) -> ( <. A , B >. F <. C , D >. ) = S )

Proof

Step Hyp Ref Expression
1 ov3.1 
 |-  S e. _V
2 ov3.2 
 |-  ( ( ( w = A /\ v = B ) /\ ( u = C /\ f = D ) ) -> R = S )
3 ov3.3 
 |-  F = { <. <. x , y >. , z >. | ( ( x e. ( H X. H ) /\ y e. ( H X. H ) ) /\ E. w E. v E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = R ) ) }
4 1 isseti 
 |-  E. z z = S
5 nfv 
 |-  F/ z ( ( A e. H /\ B e. H ) /\ ( C e. H /\ D e. H ) )
6 nfcv 
 |-  F/_ z <. A , B >.
7 nfoprab3 
 |-  F/_ z { <. <. x , y >. , z >. | ( ( x e. ( H X. H ) /\ y e. ( H X. H ) ) /\ E. w E. v E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = R ) ) }
8 3 7 nfcxfr 
 |-  F/_ z F
9 nfcv 
 |-  F/_ z <. C , D >.
10 6 8 9 nfov 
 |-  F/_ z ( <. A , B >. F <. C , D >. )
11 10 nfeq1 
 |-  F/ z ( <. A , B >. F <. C , D >. ) = S
12 2 eqeq2d 
 |-  ( ( ( w = A /\ v = B ) /\ ( u = C /\ f = D ) ) -> ( z = R <-> z = S ) )
13 12 copsex4g 
 |-  ( ( ( A e. H /\ B e. H ) /\ ( C e. H /\ D e. H ) ) -> ( E. w E. v E. u E. f ( ( <. A , B >. = <. w , v >. /\ <. C , D >. = <. u , f >. ) /\ z = R ) <-> z = S ) )
14 opelxpi 
 |-  ( ( A e. H /\ B e. H ) -> <. A , B >. e. ( H X. H ) )
15 opelxpi 
 |-  ( ( C e. H /\ D e. H ) -> <. C , D >. e. ( H X. H ) )
16 nfcv 
 |-  F/_ x <. A , B >.
17 nfcv 
 |-  F/_ y <. A , B >.
18 nfcv 
 |-  F/_ y <. C , D >.
19 nfv 
 |-  F/ x E. w E. v E. u E. f ( ( <. A , B >. = <. w , v >. /\ y = <. u , f >. ) /\ z = R )
20 nfoprab1 
 |-  F/_ x { <. <. x , y >. , z >. | ( ( x e. ( H X. H ) /\ y e. ( H X. H ) ) /\ E. w E. v E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = R ) ) }
21 3 20 nfcxfr 
 |-  F/_ x F
22 nfcv 
 |-  F/_ x y
23 16 21 22 nfov 
 |-  F/_ x ( <. A , B >. F y )
24 23 nfeq1 
 |-  F/ x ( <. A , B >. F y ) = z
25 19 24 nfim 
 |-  F/ x ( E. w E. v E. u E. f ( ( <. A , B >. = <. w , v >. /\ y = <. u , f >. ) /\ z = R ) -> ( <. A , B >. F y ) = z )
26 nfv 
 |-  F/ y E. w E. v E. u E. f ( ( <. A , B >. = <. w , v >. /\ <. C , D >. = <. u , f >. ) /\ z = R )
27 nfoprab2 
 |-  F/_ y { <. <. x , y >. , z >. | ( ( x e. ( H X. H ) /\ y e. ( H X. H ) ) /\ E. w E. v E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = R ) ) }
28 3 27 nfcxfr 
 |-  F/_ y F
29 17 28 18 nfov 
 |-  F/_ y ( <. A , B >. F <. C , D >. )
30 29 nfeq1 
 |-  F/ y ( <. A , B >. F <. C , D >. ) = z
31 26 30 nfim 
 |-  F/ y ( E. w E. v E. u E. f ( ( <. A , B >. = <. w , v >. /\ <. C , D >. = <. u , f >. ) /\ z = R ) -> ( <. A , B >. F <. C , D >. ) = z )
32 eqeq1 
 |-  ( x = <. A , B >. -> ( x = <. w , v >. <-> <. A , B >. = <. w , v >. ) )
33 32 anbi1d 
 |-  ( x = <. A , B >. -> ( ( x = <. w , v >. /\ y = <. u , f >. ) <-> ( <. A , B >. = <. w , v >. /\ y = <. u , f >. ) ) )
34 33 anbi1d 
 |-  ( x = <. A , B >. -> ( ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = R ) <-> ( ( <. A , B >. = <. w , v >. /\ y = <. u , f >. ) /\ z = R ) ) )
35 34 4exbidv 
 |-  ( x = <. A , B >. -> ( E. w E. v E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = R ) <-> E. w E. v E. u E. f ( ( <. A , B >. = <. w , v >. /\ y = <. u , f >. ) /\ z = R ) ) )
36 oveq1 
 |-  ( x = <. A , B >. -> ( x F y ) = ( <. A , B >. F y ) )
37 36 eqeq1d 
 |-  ( x = <. A , B >. -> ( ( x F y ) = z <-> ( <. A , B >. F y ) = z ) )
38 35 37 imbi12d 
 |-  ( x = <. A , B >. -> ( ( E. w E. v E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = R ) -> ( x F y ) = z ) <-> ( E. w E. v E. u E. f ( ( <. A , B >. = <. w , v >. /\ y = <. u , f >. ) /\ z = R ) -> ( <. A , B >. F y ) = z ) ) )
39 eqeq1 
 |-  ( y = <. C , D >. -> ( y = <. u , f >. <-> <. C , D >. = <. u , f >. ) )
40 39 anbi2d 
 |-  ( y = <. C , D >. -> ( ( <. A , B >. = <. w , v >. /\ y = <. u , f >. ) <-> ( <. A , B >. = <. w , v >. /\ <. C , D >. = <. u , f >. ) ) )
41 40 anbi1d 
 |-  ( y = <. C , D >. -> ( ( ( <. A , B >. = <. w , v >. /\ y = <. u , f >. ) /\ z = R ) <-> ( ( <. A , B >. = <. w , v >. /\ <. C , D >. = <. u , f >. ) /\ z = R ) ) )
42 41 4exbidv 
 |-  ( y = <. C , D >. -> ( E. w E. v E. u E. f ( ( <. A , B >. = <. w , v >. /\ y = <. u , f >. ) /\ z = R ) <-> E. w E. v E. u E. f ( ( <. A , B >. = <. w , v >. /\ <. C , D >. = <. u , f >. ) /\ z = R ) ) )
43 oveq2 
 |-  ( y = <. C , D >. -> ( <. A , B >. F y ) = ( <. A , B >. F <. C , D >. ) )
44 43 eqeq1d 
 |-  ( y = <. C , D >. -> ( ( <. A , B >. F y ) = z <-> ( <. A , B >. F <. C , D >. ) = z ) )
45 42 44 imbi12d 
 |-  ( y = <. C , D >. -> ( ( E. w E. v E. u E. f ( ( <. A , B >. = <. w , v >. /\ y = <. u , f >. ) /\ z = R ) -> ( <. A , B >. F y ) = z ) <-> ( E. w E. v E. u E. f ( ( <. A , B >. = <. w , v >. /\ <. C , D >. = <. u , f >. ) /\ z = R ) -> ( <. A , B >. F <. C , D >. ) = z ) ) )
46 moeq 
 |-  E* z z = R
47 46 mosubop 
 |-  E* z E. u E. f ( y = <. u , f >. /\ z = R )
48 47 mosubop 
 |-  E* z E. w E. v ( x = <. w , v >. /\ E. u E. f ( y = <. u , f >. /\ z = R ) )
49 anass 
 |-  ( ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = R ) <-> ( x = <. w , v >. /\ ( y = <. u , f >. /\ z = R ) ) )
50 49 2exbii 
 |-  ( E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = R ) <-> E. u E. f ( x = <. w , v >. /\ ( y = <. u , f >. /\ z = R ) ) )
51 19.42vv 
 |-  ( E. u E. f ( x = <. w , v >. /\ ( y = <. u , f >. /\ z = R ) ) <-> ( x = <. w , v >. /\ E. u E. f ( y = <. u , f >. /\ z = R ) ) )
52 50 51 bitri 
 |-  ( E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = R ) <-> ( x = <. w , v >. /\ E. u E. f ( y = <. u , f >. /\ z = R ) ) )
53 52 2exbii 
 |-  ( E. w E. v E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = R ) <-> E. w E. v ( x = <. w , v >. /\ E. u E. f ( y = <. u , f >. /\ z = R ) ) )
54 53 mobii 
 |-  ( E* z E. w E. v E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = R ) <-> E* z E. w E. v ( x = <. w , v >. /\ E. u E. f ( y = <. u , f >. /\ z = R ) ) )
55 48 54 mpbir 
 |-  E* z E. w E. v E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = R )
56 55 a1i 
 |-  ( ( x e. ( H X. H ) /\ y e. ( H X. H ) ) -> E* z E. w E. v E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = R ) )
57 56 3 ovidi 
 |-  ( ( x e. ( H X. H ) /\ y e. ( H X. H ) ) -> ( E. w E. v E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = R ) -> ( x F y ) = z ) )
58 16 17 18 25 31 38 45 57 vtocl2gaf 
 |-  ( ( <. A , B >. e. ( H X. H ) /\ <. C , D >. e. ( H X. H ) ) -> ( E. w E. v E. u E. f ( ( <. A , B >. = <. w , v >. /\ <. C , D >. = <. u , f >. ) /\ z = R ) -> ( <. A , B >. F <. C , D >. ) = z ) )
59 14 15 58 syl2an 
 |-  ( ( ( A e. H /\ B e. H ) /\ ( C e. H /\ D e. H ) ) -> ( E. w E. v E. u E. f ( ( <. A , B >. = <. w , v >. /\ <. C , D >. = <. u , f >. ) /\ z = R ) -> ( <. A , B >. F <. C , D >. ) = z ) )
60 13 59 sylbird 
 |-  ( ( ( A e. H /\ B e. H ) /\ ( C e. H /\ D e. H ) ) -> ( z = S -> ( <. A , B >. F <. C , D >. ) = z ) )
61 eqeq2 
 |-  ( z = S -> ( ( <. A , B >. F <. C , D >. ) = z <-> ( <. A , B >. F <. C , D >. ) = S ) )
62 60 61 mpbidi 
 |-  ( ( ( A e. H /\ B e. H ) /\ ( C e. H /\ D e. H ) ) -> ( z = S -> ( <. A , B >. F <. C , D >. ) = S ) )
63 5 11 62 exlimd 
 |-  ( ( ( A e. H /\ B e. H ) /\ ( C e. H /\ D e. H ) ) -> ( E. z z = S -> ( <. A , B >. F <. C , D >. ) = S ) )
64 4 63 mpi 
 |-  ( ( ( A e. H /\ B e. H ) /\ ( C e. H /\ D e. H ) ) -> ( <. A , B >. F <. C , D >. ) = S )