Theorem fnoprval 4094

Description: Representation of an operation class abstraction in terms of its values.

Assertion

Ref	Expression
fnoprval	|- (F Fn (A X. B) <-> F = {<.<.x, y>., z>. | ((x e. A /\ y e. B) /\ z = (xFy))})

Distinct variable groups:   x,y,z,A   x,B,y,z   x,F,y,z

Proof of Theorem fnoprval

Step	Hyp	Ref	Expression
1		dffn5 3834	. 2 |- (F Fn (A X. B) <-> F = {<.w, z>. | (w e. (A X. B) /\ z = (F` w))})
2		elxp 3257	. . . . . . 7 |- (w e. (A X. B) <-> E.xE.y(w = <.x, y>. /\ (x e. A /\ y e. B)))
3	2	anbi1i 483	. . . . . 6 |- ((w e. (A X. B) /\ z = (F` w)) <-> (E.xE.y(w = <.x, y>. /\ (x e. A /\ y e. B)) /\ z = (F` w)))
4		19.41vv 1339	. . . . . 6 |- (E.xE.y((w = <.x, y>. /\ (x e. A /\ y e. B)) /\ z = (F` w)) <-> (E.xE.y(w = <.x, y>. /\ (x e. A /\ y e. B)) /\ z = (F` w)))
5		anass 441	. . . . . . . 8 |- (((w = <.x, y>. /\ (x e. A /\ y e. B)) /\ z = (F` w)) <-> (w = <.x, y>. /\ ((x e. A /\ y e. B) /\ z = (F` w))))
6		fveq2 3800	. . . . . . . . . . . 12 |- (w = <.x, y>. -> (F` w) = (F` <.x, y>.))
7		df-opr 4041	. . . . . . . . . . . 12 |- (xFy) = (F` <.x, y>.)
8	6, 7	syl6eqr 1562	. . . . . . . . . . 11 |- (w = <.x, y>. -> (F` w) = (xFy))
9	8	eqeq2d 1523	. . . . . . . . . 10 |- (w = <.x, y>. -> (z = (F` w) <-> z = (xFy)))
10	9	anbi2d 618	. . . . . . . . 9 |- (w = <.x, y>. -> (((x e. A /\ y e. B) /\ z = (F` w)) <-> ((x e. A /\ y e. B) /\ z = (xFy))))
11	10	pm5.32i 647	. . . . . . . 8 |- ((w = <.x, y>. /\ ((x e. A /\ y e. B) /\ z = (F` w))) <-> (w = <.x, y>. /\ ((x e. A /\ y e. B) /\ z = (xFy))))
12	5, 11	bitri 171	. . . . . . 7 |- (((w = <.x, y>. /\ (x e. A /\ y e. B)) /\ z = (F` w)) <-> (w = <.x, y>. /\ ((x e. A /\ y e. B) /\ z = (xFy))))
13	12	2exbii 1084	. . . . . 6 |- (E.xE.y((w = <.x, y>. /\ (x e. A /\ y e. B)) /\ z = (F` w)) <-> E.xE.y(w = <.x, y>. /\ ((x e. A /\ y e. B) /\ z = (xFy))))
14	3, 4, 13	3bitr2i 177	. . . . 5 |- ((w e. (A X. B) /\ z = (F` w)) <-> E.xE.y(w = <.x, y>. /\ ((x e. A /\ y e. B) /\ z = (xFy))))
15	14	opabbii 2722	. . . 4 |- {<.w, z>. | (w e. (A X. B) /\ z = (F` w))} = {<.w, z>. | E.xE.y(w = <.x, y>. /\ ((x e. A /\ y e. B) /\ z = (xFy)))}
16		dfoprab2 4067	. . . 4 |- {<.<.x, y>., z>. | ((x e. A /\ y e. B) /\ z = (xFy))} = {<.w, z>. | E.xE.y(w = <.x, y>. /\ ((x e. A /\ y e. B) /\ z = (xFy)))}
17	15, 16	eqtr4i 1535	. . 3 |- {<.w, z>. | (w e. (A X. B) /\ z = (F` w))} = {<.<.x, y>., z>. | ((x e. A /\ y e. B) /\ z = (xFy))}
18	17	eqeq2i 1522	. 2 |- (F = {<.w, z>. | (w e. (A X. B) /\ z = (F` w))} <-> F = {<.<.x, y>., z>. | ((x e. A /\ y e. B) /\ z = (xFy))})
19	1, 18	bitri 171	1 |- (F Fn (A X. B) <-> F = {<.<.x, y>., z>. | ((x e. A /\ y e. B) /\ z = (xFy))})

Syntax hints:   <-> wb 144   /\ wa 221   = wceq 988   e. wcel 990  E.wex 1012  <.cop 2456  {copab 2717   X. cxp 3223   Fn wfn 3232  ` cfv 3237  (class class class)co 4039  {copab2 4040

This theorem is referenced by:  foprval 4095  mapxpen 4584  dfioo2 6463  cnnvm 8432

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 994  ax-gen 995  ax-8 996  ax-9 997  ax-10 998  ax-11 999  ax-12 1000  ax-13 1001  ax-14 1002  ax-17 1003  ax-4 1005  ax-5o 1007  ax-6o 1010  ax-9o 1155  ax-10o 1173  ax-16 1243  ax-11o 1251  ax-ext 1494  ax-sep 2754  ax-pow 2794  ax-pr 2832  ax-un 2920

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-ex 1013  df-sb 1205  df-eu 1415  df-mo 1416  df-clab 1500  df-cleq 1505  df-clel 1508  df-ne 1624  df-ral 1687  df-rex 1688  df-v 1850  df-dif 2093  df-un 2094  df-in 2095  df-ss 2097  df-nul 2325  df-pw 2447  df-sn 2457  df-pr 2458  df-op 2461  df-uni 2552  df-br 2670  df-opab 2718  df-id 2889  df-xp 3239  df-rel 3240  df-cnv 3241  df-co 3242  df-dm 3243  df-rn 3244  df-res 3245  df-ima 3246  df-fun 3247  df-fn 3248  df-fv 3253  df-opr 4041  df-oprab 4042

Copyright terms: Public domain