Theorem ov3 6242

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

Hypotheses

Ref	Expression
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

Ref	Expression
ov3	|- ( ( ( A e. H /\ B e. H ) /\ ( C e. H /\ D e. H ) ) -> ( <. A , B >. F <. C , D >. ) = S )

Distinct variable groups:   u, f, v, w, x, y, z, A   B, f, u, v, w, x, y, z   x, R, y, z   C, f, u, v, w, y, z   D, f, u, v, w, y, z   f, H, u, v, w, x, y, z   S, f, u, v, w, z

Allowed substitution hints:   C( x)   D( x)   R( w, v, u, f)   S( x, y)   F( x, y, z, w, v, u, f)

Proof of Theorem ov3

Step	Hyp	Ref	Expression
1		ov3.1	. . 3 |- S e. _V
2	1	isseti 2993	. 2 |- E. z z = S
3		nfv 1673	. . 3 |- F/ z ( ( A e. H /\ B e. H ) /\ ( C e. H /\ D e. H ) )
4		nfcv 2589	. . . . 5 |- F/_ z <. A , B >.
5		ov3.3	. . . . . 6 |- 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 ) ) }
6		nfoprab3 6152	. . . . . 6 |- 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 ) ) }
7	5, 6	nfcxfr 2587	. . . . 5 |- F/_ z F
8		nfcv 2589	. . . . 5 |- F/_ z <. C , D >.
9	4, 7, 8	nfov 6129	. . . 4 |- F/_ z ( <. A , B >. F <. C , D >. )
10	9	nfeq1 2603	. . 3 |- F/ z ( <. A , B >. F <. C , D >. ) = S
11		ov3.2	. . . . . . 7 |- ( ( ( w = A /\ v = B ) /\ ( u = C /\ f = D ) ) -> R = S )
12	11	eqeq2d 2454	. . . . . 6 |- ( ( ( w = A /\ v = B ) /\ ( u = C /\ f = D ) ) -> ( z = R <-> z = S ) )
13	12	copsex4g 4595	. . . . 5 |- ( ( ( 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 4886	. . . . . 6 |- ( ( A e. H /\ B e. H ) -> <. A , B >. e. ( H X. H ) )
15		opelxpi 4886	. . . . . 6 |- ( ( C e. H /\ D e. H ) -> <. C , D >. e. ( H X. H ) )
16		nfcv 2589	. . . . . . 7 |- F/_ x <. A , B >.
17		nfcv 2589	. . . . . . 7 |- F/_ y <. A , B >.
18		nfcv 2589	. . . . . . 7 |- F/_ y <. C , D >.
19		nfv 1673	. . . . . . . 8 |- F/ x E. w E. v E. u E. f ( ( <. A , B >. = <. w , v >. /\ y = <. u , f >. ) /\ z = R )
20		nfoprab1 6150	. . . . . . . . . . 11 |- 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	5, 20	nfcxfr 2587	. . . . . . . . . 10 |- F/_ x F
22		nfcv 2589	. . . . . . . . . 10 |- F/_ x y
23	16, 21, 22	nfov 6129	. . . . . . . . 9 |- F/_ x ( <. A , B >. F y )
24	23	nfeq1 2603	. . . . . . . 8 |- F/ x ( <. A , B >. F y ) = z
25	19, 24	nfim 1853	. . . . . . 7 |- 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 1673	. . . . . . . 8 |- F/ y E. w E. v E. u E. f ( ( <. A , B >. = <. w , v >. /\ <. C , D >. = <. u , f >. ) /\ z = R )
27		nfoprab2 6151	. . . . . . . . . . 11 |- 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	5, 27	nfcxfr 2587	. . . . . . . . . 10 |- F/_ y F
29	17, 28, 18	nfov 6129	. . . . . . . . 9 |- F/_ y ( <. A , B >. F <. C , D >. )
30	29	nfeq1 2603	. . . . . . . 8 |- F/ y ( <. A , B >. F <. C , D >. ) = z
31	26, 30	nfim 1853	. . . . . . 7 |- 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 2449	. . . . . . . . . . 11 |- ( x = <. A , B >. -> ( x = <. w , v >. <-> <. A , B >. = <. w , v >. ) )
33	32	anbi1d 704	. . . . . . . . . 10 |- ( x = <. A , B >. -> ( ( x = <. w , v >. /\ y = <. u , f >. ) <-> ( <. A , B >. = <. w , v >. /\ y = <. u , f >. ) ) )
34	33	anbi1d 704	. . . . . . . . 9 |- ( x = <. A , B >. -> ( ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = R ) <-> ( ( <. A , B >. = <. w , v >. /\ y = <. u , f >. ) /\ z = R ) ) )
35	34	4exbidv 1684	. . . . . . . 8 |- ( 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 6113	. . . . . . . . 9 |- ( x = <. A , B >. -> ( x F y ) = ( <. A , B >. F y ) )
37	36	eqeq1d 2451	. . . . . . . 8 |- ( x = <. A , B >. -> ( ( x F y ) = z <-> ( <. A , B >. F y ) = z ) )
38	35, 37	imbi12d 320	. . . . . . 7 |- ( 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 2449	. . . . . . . . . . 11 |- ( y = <. C , D >. -> ( y = <. u , f >. <-> <. C , D >. = <. u , f >. ) )
40	39	anbi2d 703	. . . . . . . . . 10 |- ( y = <. C , D >. -> ( ( <. A , B >. = <. w , v >. /\ y = <. u , f >. ) <-> ( <. A , B >. = <. w , v >. /\ <. C , D >. = <. u , f >. ) ) )
41	40	anbi1d 704	. . . . . . . . 9 |- ( 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 1684	. . . . . . . 8 |- ( 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 6114	. . . . . . . . 9 |- ( y = <. C , D >. -> ( <. A , B >. F y ) = ( <. A , B >. F <. C , D >. ) )
44	43	eqeq1d 2451	. . . . . . . 8 |- ( y = <. C , D >. -> ( ( <. A , B >. F y ) = z <-> ( <. A , B >. F <. C , D >. ) = z ) )
45	42, 44	imbi12d 320	. . . . . . 7 |- ( 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 3150	. . . . . . . . . . . 12 |- E* z z = R
47	46	mosubop 4605	. . . . . . . . . . 11 |- E* z E. u E. f ( y = <. u , f >. /\ z = R )
48	47	mosubop 4605	. . . . . . . . . 10 |- E* z E. w E. v ( x = <. w , v >. /\ E. u E. f ( y = <. u , f >. /\ z = R ) )
49		anass 649	. . . . . . . . . . . . . 14 |- ( ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = R ) <-> ( x = <. w , v >. /\ ( y = <. u , f >. /\ z = R ) ) )
50	49	2exbii 1635	. . . . . . . . . . . . 13 |- ( 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 1926	. . . . . . . . . . . . 13 |- ( 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 249	. . . . . . . . . . . 12 |- ( 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 1635	. . . . . . . . . . 11 |- ( 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 2279	. . . . . . . . . 10 |- ( 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 209	. . . . . . . . 9 |- E* z E. w E. v E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = R )
56	55	a1i 11	. . . . . . . 8 |- ( ( 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, 5	ovidi 6224	. . . . . . 7 |- ( ( 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 3052	. . . . . 6 |- ( ( <. 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 477	. . . . 5 |- ( ( ( 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 235	. . . 4 |- ( ( ( A e. H /\ B e. H ) /\ ( C e. H /\ D e. H ) ) -> ( z = S -> ( <. A , B >. F <. C , D >. ) = z ) )
61		eqeq2 2452	. . . 4 |- ( z = S -> ( ( <. A , B >. F <. C , D >. ) = z <-> ( <. A , B >. F <. C , D >. ) = S ) )
62	60, 61	mpbidi 216	. . 3 |- ( ( ( A e. H /\ B e. H ) /\ ( C e. H /\ D e. H ) ) -> ( z = S -> ( <. A , B >. F <. C , D >. ) = S ) )
63	3, 10, 62	exlimd 1847	. 2 |- ( ( ( A e. H /\ B e. H ) /\ ( C e. H /\ D e. H ) ) -> ( E. z z = S -> ( <. A , B >. F <. C , D >. ) = S ) )
64	2, 63	mpi 17	1 |- ( ( ( A e. H /\ B e. H ) /\ ( C e. H /\ D e. H ) ) -> ( <. A , B >. F <. C , D >. ) = S )

Syntax hints:   -> wi 4   /\ wa 369   = wceq 1369   E.wex 1586   e. wcel 1756   E*wmo 2254   _Vcvv 2987   <.cop 3898   X. cxp 4853  (class class class)co 6106   {coprab 6107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4428  ax-nul 4436  ax-pr 4546

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-ral 2735  df-rex 2736  df-rab 2739  df-v 2989  df-sbc 3202  df-dif 3346  df-un 3348  df-in 3350  df-ss 3357  df-nul 3653  df-if 3807  df-sn 3893  df-pr 3895  df-op 3899  df-uni 4107  df-br 4308  df-opab 4366  df-id 4651  df-xp 4861  df-rel 4862  df-cnv 4863  df-co 4864  df-dm 4865  df-iota 5396  df-fun 5435  df-fv 5441  df-ov 6109  df-oprab 6110

This theorem is referenced by:  ovec  7225  addcnsr  9317  mulcnsr  9318