Theorem fnopabfv 2858

Description: Representation of a function in terms of its values.

Assertion

Ref	Expression
fnopabfv	|- (F Fn A <-> F = {<.x, y>. | (x e. A /\ y = (F` x))})

Distinct variable group(s):   x,y,A   x,F,y

Proof of Theorem fnopabfv

Step	Hyp	Ref	Expression
1		visset 1350	. . . . . . . . 9 |- z e. V
2		visset 1350	. . . . . . . . 9 |- w e. V
3	1, 2	fnop 2727	. . . . . . . 8 |- ((F Fn A /\ <.z, w>. e. F) -> z e. A)
4	3	exp 291	. . . . . . 7 |- (F Fn A -> (<.z, w>. e. F -> z e. A))
5		pm4.71r 482	. . . . . . 7 |- ((<.z, w>. e. F -> z e. A) <-> (<.z, w>. e. F <-> (z e. A /\ <.z, w>. e. F)))
6	4, 5	sylib 173	. . . . . 6 |- (F Fn A -> (<.z, w>. e. F <-> (z e. A /\ <.z, w>. e. F)))
7	2	fnfvop 2856	. . . . . . . . 9 |- ((F Fn A /\ z e. A) -> ((F` z) = w <-> <.z, w>. e. F))
8		cleqcom 1103	. . . . . . . . 9 |- (w = (F` z) <-> (F` z) = w)
9	7, 8	syl5bb 410	. . . . . . . 8 |- ((F Fn A /\ z e. A) -> (w = (F` z) <-> <.z, w>. e. F))
10	9	exp 291	. . . . . . 7 |- (F Fn A -> (z e. A -> (w = (F` z) <-> <.z, w>. e. F)))
11	10	pm5.32d 491	. . . . . 6 |- (F Fn A -> ((z e. A /\ w = (F` z)) <-> (z e. A /\ <.z, w>. e. F)))
12	6, 11	bitr4d 409	. . . . 5 |- (F Fn A -> (<.z, w>. e. F <-> (z e. A /\ w = (F` z))))
13		eleq1 1149	. . . . . . 7 |- (x = z -> (x e. A <-> z e. A))
14		fveq2 2832	. . . . . . . 8 |- (x = z -> (F` x) = (F` z))
15	14	cleq2d 1112	. . . . . . 7 |- (x = z -> (y = (F` x) <-> y = (F` z)))
16	13, 15	anbi12d 476	. . . . . 6 |- (x = z -> ((x e. A /\ y = (F` x)) <-> (z e. A /\ y = (F` z))))
17		cleq1 1107	. . . . . . 7 |- (y = w -> (y = (F` z) <-> w = (F` z)))
18	17	anbi2d 468	. . . . . 6 |- (y = w -> ((z e. A /\ y = (F` z)) <-> (z e. A /\ w = (F` z))))
19	1, 2, 16, 18	opelopab 2117	. . . . 5 |- (<.z, w>. e. {<.x, y>. | (x e. A /\ y = (F` x))} <-> (z e. A /\ w = (F` z)))
20	12, 19	syl6bbr 416	. . . 4 |- (F Fn A -> (<.z, w>. e. F <-> <.z, w>. e. {<.x, y>. | (x e. A /\ y = (F` x))}))
21	20	19.21aivv 944	. . 3 |- (F Fn A -> A.zA.w(<.z, w>. e. F <-> <.z, w>. e. {<.x, y>. | (x e. A /\ y = (F` x))}))
22		fnrel 2722	. . . . 5 |- (F Fn A -> Rel F)
23		relopab 2494	. . . . 5 |- Rel {<.x, y>. | (x e. A /\ y = (F` x))}
24	22, 23	jctir 241	. . . 4 |- (F Fn A -> (Rel F /\ Rel {<.x, y>. | (x e. A /\ y = (F` x))}))
25		cleqrel 2483	. . . 4 |- ((Rel F /\ Rel {<.x, y>. | (x e. A /\ y = (F` x))}) -> (F = {<.x, y>. | (x e. A /\ y = (F` x))} <-> A.zA.w(<.z, w>. e. F <-> <.z, w>. e. {<.x, y>. | (x e. A /\ y = (F` x))})))
26	24, 25	syl 12	. . 3 |- (F Fn A -> (F = {<.x, y>. | (x e. A /\ y = (F` x))} <-> A.zA.w(<.z, w>. e. F <-> <.z, w>. e. {<.x, y>. | (x e. A /\ y = (F` x))})))
27	21, 26	mpbird 171	. 2 |- (F Fn A -> F = {<.x, y>. | (x e. A /\ y = (F` x))})
28		fvex 2838	. . . 4 |- (F` x) e. V
29		cleqid 1102	. . . 4 |- {<.x, y>. | (x e. A /\ y = (F` x))} = {<.x, y>. | (x e. A /\ y = (F` x))}
30	28, 29	fnopab2 2747	. . 3 |- {<.x, y>. | (x e. A /\ y = (F` x))} Fn A
31		fneq1 2718	. . 3 |- (F = {<.x, y>. | (x e. A /\ y = (F` x))} -> (F Fn A <-> {<.x, y>. | (x e. A /\ y = (F` x))} Fn A))
32	30, 31	mpbiri 169	. 2 |- (F = {<.x, y>. | (x e. A /\ y = (F` x))} -> F Fn A)
33	27, 32	impbi 139	1 |- (F Fn A <-> F = {<.x, y>. | (x e. A /\ y = (F` x))})

Syntax hints:   -> wi 2   <-> wb 127   /\ wa 196  A.wal 672   = weq 797   = wceq 1091   e. wcel 1092  <.cop 1810  {copab 2055  Rel wrel 2415   Fn wfn 2417  ` cfv 2422

This theorem is referenced by:  fopabfv 2894  fnoprval 3042  xpmapenlem3 3393  pjrn 5587

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-un 1076  ax-pow 1077

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679  df-sb 853  df-eu 1009  df-mo 1010  df-clab 1093  df-cleq 1097  df-clel 1099  df-ral 1205  df-rex 1206  df-v 1349  df-dif 1489  df-un 1490  df-in 1491  df-ss 1492  df-nul 1708  df-pw 1799  df-sn 1811  df-pr 1812  df-op 1815  df-uni 1920  df-br 2063  df-opab 2098  df-id 2125  df-xp 2424  df-rel 2425  df-cnv 2426  df-co 2427  df-dm 2428  df-rn 2429  df-res 2430  df-ima 2431  df-fun 2432  df-fn 2433  df-fv 2438

metamath.org