Theorem ov 5562

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

Hypotheses

Ref	Expression
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!zph)
ov.6	|- F = { <. <.x , y >. , z >. | ((x e. R /\ y e. S) /\ ph) }

Assertion

Ref	Expression
ov	|- ((A e. R /\ B e. S) -> ((A FB) = C <-> th))

Distinct variable groups:   x,y,z,A   x,B,y,z   x, C,y,z   x, R,y,z   x, S,y,z   th,x,y,z

Allowed substitution hints:   ph(x,y,z)   ps(x,y,z)   ch(x,y,z)   F(x,y,z)

Proof of Theorem ov

Step	Hyp	Ref	Expression
1		df-ov 5458	. . . . 5 |- (A FB) = ( F ` <.A , B >.)
2		ov.6	. . . . . 6 |- F = { <. <.x , y >. , z >. | ((x e. R /\ y e. S) /\ ph) }
3	2	fveq1i 5122	. . . . 5 |- ( F ` <.A , B >.) = ( { <. <.x , y >. , z >. | ((x e. R /\ y e. S) /\ ph) } ` <.A , B >.)
4	1, 3	eqtri 2057	. . . 4 |- (A FB) = ( { <. <.x , y >. , z >. | ((x e. R /\ y e. S) /\ ph) } ` <.A , B >.)
5	4	eqeq1i 2044	. . 3 |- ((A FB) = C <-> ( { <. <.x , y >. , z >. | ((x e. R /\ y e. S) /\ ph) } ` <.A , B >.) = C)
6		ov.5	. . . . . 6 |- ((x e. R /\ y e. S) -> E!zph)
7	6	fnoprab 5546	. . . . 5 |- { <. <.x , y >. , z >. | ((x e. R /\ y e. S) /\ ph) } Fn { <.x , y >. | (x e. R /\ y e. S) }
8		eleq1 2097	. . . . . . . 8 |- (x = A -> (x e. R <-> A e. R))
9	8	anbi1d 438	. . . . . . 7 |- (x = A -> ((x e. R /\ y e. S) <-> (A e. R /\ y e. S)))
10		eleq1 2097	. . . . . . . 8 |- (y = B -> (y e. S <-> B e. S))
11	10	anbi2d 437	. . . . . . 7 |- (y = B -> ((A e. R /\ y e. S) <-> (A e. R /\ B e. S)))
12	9, 11	opelopabg 3996	. . . . . 6 |- ((A e. R /\ B e. S) -> ( <.A , B >. e. { <.x , y >. | (x e. R /\ y e. S) } <-> (A e. R /\ B e. S)))
13	12	ibir 166	. . . . 5 |- ((A e. R /\ B e. S) -> <.A , B >. e. { <.x , y >. | (x e. R /\ y e. S) })
14		fnopfvb 5158	. . . . 5 |- (( { <. <.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) }))
15	7, 13, 14	sylancr 393	. . . 4 |- ((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) }))
16		ov.1	. . . . 5 |- C e. _V
17		ov.2	. . . . . . 7 |- (x = A -> (ph <-> ps))
18	9, 17	anbi12d 442	. . . . . 6 |- (x = A -> (((x e. R /\ y e. S) /\ ph) <-> ((A e. R /\ y e. S) /\ ps)))
19		ov.3	. . . . . . 7 |- (y = B -> (ps <-> ch))
20	11, 19	anbi12d 442	. . . . . 6 |- (y = B -> (((A e. R /\ y e. S) /\ ps) <-> ((A e. R /\ B e. S) /\ ch)))
21		ov.4	. . . . . . 7 |- (z = C -> (ch <-> th))
22	21	anbi2d 437	. . . . . 6 |- (z = C -> (((A e. R /\ B e. S) /\ ch) <-> ((A e. R /\ B e. S) /\ th)))
23	18, 20, 22	eloprabg 5534	. . . . 5 |- ((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	16, 23	mp3an3 1220	. . . 4 |- ((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	15, 24	bitrd 177	. . 3 |- ((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	5, 25	syl5bb 181	. 2 |- ((A e. R /\ B e. S) -> ((A FB) = C <-> ((A e. R /\ B e. S) /\ th)))
27	26	bianabs 543	1 |- ((A e. R /\ B e. S) -> ((A FB) = C <-> th))

Syntax hints:   -> wi 4   /\ wa 97   <-> wb 98   = wceq 1242   e. wcel 1390  E!weu 1897   _Vcvv 2551   <.cop 3370   {copab 3808   Fn wfn 4840   ` cfv 4845  (class class class)co 5455   {coprab 5456

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bndl 1396  ax-4 1397  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-pow 3918  ax-pr 3935

This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-v 2553  df-sbc 2759  df-un 2916  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-br 3756  df-opab 3810  df-id 4021  df-xp 4294  df-rel 4295  df-cnv 4296  df-co 4297  df-dm 4298  df-iota 4810  df-fun 4847  df-fn 4848  df-fv 4853  df-ov 5458  df-oprab 5459

This theorem is referenced by: (None)