Theorem eqfnfv 3736

Description: Equality of functions is determined by their values. Exercise 4 of [TakeutiZaring] p. 28.

Assertion

Ref	Expression
eqfnfv	|- ((F Fn A /\ G Fn B) -> (F = G <-> (A = B /\ A.x e. A (F` x) = (G` x))))

Distinct variable groups:   x,A   x,F   x,G

Proof of Theorem eqfnfv

Step	Hyp	Ref	Expression
1		eqeq12 1463	. . . . 5 |- ((dom F = A /\ dom G = B) -> (dom F = dom G <-> A = B))
2		dmeq 3268	. . . . 5 |- (F = G -> dom F = dom G)
3	1, 2	syl5bi 208	. . . 4 |- ((dom F = A /\ dom G = B) -> (F = G -> A = B))
4		fndm 3527	. . . 4 |- (F Fn A -> dom F = A)
5		fndm 3527	. . . 4 |- (G Fn B -> dom G = B)
6	3, 4, 5	syl2an 454	. . 3 |- ((F Fn A /\ G Fn B) -> (F = G -> A = B))
7		fveq1 3662	. . . . . 6 |- (F = G -> (F` x) = (G` x))
8	7	a1d 12	. . . . 5 |- (F = G -> (x e. A -> (F` x) = (G` x)))
9	8	r19.21aiv 1689	. . . 4 |- (F = G -> A.x e. A (F` x) = (G` x))
10	9	a1i 8	. . 3 |- ((F Fn A /\ G Fn B) -> (F = G -> A.x e. A (F` x) = (G` x)))
11	6, 10	jcad 598	. 2 |- ((F Fn A /\ G Fn B) -> (F = G -> (A = B /\ A.x e. A (F` x) = (G` x))))
12		visset 1788	. . . . . . . . . . . . . . . . 17 |- y e. V
13	12	fnopfvb 3693	. . . . . . . . . . . . . . . 16 |- ((F Fn A /\ x e. A) -> ((F` x) = y <-> <.x, y>. e. F))
14	13	adantlr 393	. . . . . . . . . . . . . . 15 |- (((F Fn A /\ G Fn A) /\ x e. A) -> ((F` x) = y <-> <.x, y>. e. F))
15	12	fnopfvb 3693	. . . . . . . . . . . . . . . 16 |- ((G Fn A /\ x e. A) -> ((G` x) = y <-> <.x, y>. e. G))
16	15	adantll 392	. . . . . . . . . . . . . . 15 |- (((F Fn A /\ G Fn A) /\ x e. A) -> ((G` x) = y <-> <.x, y>. e. G))
17	14, 16	bibi12d 627	. . . . . . . . . . . . . 14 |- (((F Fn A /\ G Fn A) /\ x e. A) -> (((F` x) = y <-> (G` x) = y) <-> (<.x, y>. e. F <-> <.x, y>. e. G)))
18		eqeq1 1457	. . . . . . . . . . . . . 14 |- ((F` x) = (G` x) -> ((F` x) = y <-> (G` x) = y))
19	17, 18	syl5bi 208	. . . . . . . . . . . . 13 |- (((F Fn A /\ G Fn A) /\ x e. A) -> ((F` x) = (G` x) -> (<.x, y>. e. F <-> <.x, y>. e. G)))
20	19	ex 373	. . . . . . . . . . . 12 |- ((F Fn A /\ G Fn A) -> (x e. A -> ((F` x) = (G` x) -> (<.x, y>. e. F <-> <.x, y>. e. G))))
21	20	a2d 13	. . . . . . . . . . 11 |- ((F Fn A /\ G Fn A) -> ((x e. A -> (F` x) = (G` x)) -> (x e. A -> (<.x, y>. e. F <-> <.x, y>. e. G))))
22	21	com3r 35	. . . . . . . . . 10 |- (x e. A -> ((F Fn A /\ G Fn A) -> ((x e. A -> (F` x) = (G` x)) -> (<.x, y>. e. F <-> <.x, y>. e. G))))
23	4	eleq2d 1517	. . . . . . . . . . . . . 14 |- (F Fn A -> (x e. dom F <-> x e. A))
24		visset 1788	. . . . . . . . . . . . . . 15 |- x e. V
25	24	opeldm 3271	. . . . . . . . . . . . . 14 |- (<.x, y>. e. F -> x e. dom F)
26	23, 25	syl5bi 208	. . . . . . . . . . . . 13 |- (F Fn A -> (<.x, y>. e. F -> x e. A))
27	26	con3d 95	. . . . . . . . . . . 12 |- (F Fn A -> (-. x e. A -> -. <.x, y>. e. F))
28		fndm 3527	. . . . . . . . . . . . . . 15 |- (G Fn A -> dom G = A)
29	28	eleq2d 1517	. . . . . . . . . . . . . 14 |- (G Fn A -> (x e. dom G <-> x e. A))
30	24	opeldm 3271	. . . . . . . . . . . . . 14 |- (<.x, y>. e. G -> x e. dom G)
31	29, 30	syl5bi 208	. . . . . . . . . . . . 13 |- (G Fn A -> (<.x, y>. e. G -> x e. A))
32	31	con3d 95	. . . . . . . . . . . 12 |- (G Fn A -> (-. x e. A -> -. <.x, y>. e. G))
33	27, 32	anim12ii 557	. . . . . . . . . . 11 |- ((F Fn A /\ G Fn A) -> (-. x e. A -> (-. <.x, y>. e. F /\ -. <.x, y>. e. G)))
34		pm5.21 674	. . . . . . . . . . . 12 |- ((-. <.x, y>. e. F /\ -. <.x, y>. e. G) -> (<.x, y>. e. F <-> <.x, y>. e. G))
35	34	a1d 12	. . . . . . . . . . 11 |- ((-. <.x, y>. e. F /\ -. <.x, y>. e. G) -> ((x e. A -> (F` x) = (G` x)) -> (<.x, y>. e. F <-> <.x, y>. e. G)))
36	33, 35	syl6com 53	. . . . . . . . . 10 |- (-. x e. A -> ((F Fn A /\ G Fn A) -> ((x e. A -> (F` x) = (G` x)) -> (<.x, y>. e. F <-> <.x, y>. e. G))))
37	22, 36	pm2.61i 126	. . . . . . . . 9 |- ((F Fn A /\ G Fn A) -> ((x e. A -> (F` x) = (G` x)) -> (<.x, y>. e. F <-> <.x, y>. e. G)))
38	37	19.21adv 1270	. . . . . . . 8 |- ((F Fn A /\ G Fn A) -> ((x e. A -> (F` x) = (G` x)) -> A.y(<.x, y>. e. F <-> <.x, y>. e. G)))
39	38	19.20dv 1271	. . . . . . 7 |- ((F Fn A /\ G Fn A) -> (A.x(x e. A -> (F` x) = (G` x)) -> A.xA.y(<.x, y>. e. F <-> <.x, y>. e. G)))
40		df-ral 1625	. . . . . . 7 |- (A.x e. A (F` x) = (G` x) <-> A.x(x e. A -> (F` x) = (G` x)))
41	39, 40	syl5ib 206	. . . . . 6 |- ((F Fn A /\ G Fn A) -> (A.x e. A (F` x) = (G` x) -> A.xA.y(<.x, y>. e. F <-> <.x, y>. e. G)))
42		eqrel 3212	. . . . . . 7 |- ((Rel F /\ Rel G) -> (F = G <-> A.xA.y(<.x, y>. e. F <-> <.x, y>. e. G)))
43		fnrel 3526	. . . . . . 7 |- (F Fn A -> Rel F)
44		fnrel 3526	. . . . . . 7 |- (G Fn A -> Rel G)
45	42, 43, 44	syl2an 454	. . . . . 6 |- ((F Fn A /\ G Fn A) -> (F = G <-> A.xA.y(<.x, y>. e. F <-> <.x, y>. e. G)))
46	41, 45	sylibrd 204	. . . . 5 |- ((F Fn A /\ G Fn A) -> (A.x e. A (F` x) = (G` x) -> F = G))
47		fneq2 3523	. . . . . 6 |- (A = B -> (G Fn A <-> G Fn B))
48	47	biimparc 419	. . . . 5 |- ((G Fn B /\ A = B) -> G Fn A)
49	46, 48	sylan2 451	. . . 4 |- ((F Fn A /\ (G Fn B /\ A = B)) -> (A.x e. A (F` x) = (G` x) -> F = G))
50	49	exp32 377	. . 3 |- (F Fn A -> (G Fn B -> (A = B -> (A.x e. A (F` x) = (G` x) -> F = G))))
51	50	imp4b 365	. 2 |- ((F Fn A /\ G Fn B) -> ((A = B /\ A.x e. A (F` x) = (G` x)) -> F = G))
52	11, 51	impbid 514	1 |- ((F Fn A /\ G Fn B) -> (F = G <-> (A = B /\ A.x e. A (F` x) = (G` x))))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 146   /\ wa 223  A.wal 950   = wceq 1099   e. wcel 1105  A.wral 1621  <.cop 2382  dom cdm 3133  Rel wrel 3138   Fn wfn 3140  ` cfv 3145

This theorem is referenced by:  eqfnfvf 3737  fvreseq 3738  fconst2g 3784  tfr3 3865  eqfnoprval 3955  curry1 4036  df1st2 4064  df2nd2 4065  mapenlem2 4422  seq1res 6215  seq1shftid 6244  seq1seqz 6424  seq1seq0 6428  seqzeq 6438  seqzres 6443  seqzres2 6444  sspn 8264  nmlno0lem 8320  phoeqi 8384  sinco 8499  cosco 8500  shftefif1olem 8574  shftefif1olemOLD 8575  cayleylem2 8677  dfiop2 9810  hoeqt 9817  ho01 9885  hoeq1t 9887  kbpjt 10010  nmlnop0ALT 10049  lnopco0 10058  lnopcon 10092  lnfncon 10119  hmopidmpj 10205  pjssdif2 10227  pjinvar 10243

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 951  ax-5 952  ax-6 953  ax-7 954  ax-gen 955  ax-8 1101  ax-9 1102  ax-10 1103  ax-12 1104  ax-13 1107  ax-14 1108  ax-11 1180  ax-17 1190  ax-16 1194  ax-11o 1202  ax-ext 1436  ax-sep 2671  ax-nul 2678  ax-pow 2710  ax-pr 2747

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 957  df-sb 1155  df-eu 1359  df-mo 1360  df-clab 1441  df-cleq 1446  df-clel 1449  df-ne 1563  df-ral 1625  df-rex 1626  df-v 1787  df-dif 2020  df-un 2021  df-in 2022  df-ss 2024  df-nul 2252  df-pw 2373  df-sn 2383  df-pr 2384  df-op 2387  df-uni 2472  df-br 2588  df-opab 2635  df-id 2797  df-xp 3147  df-rel 3148  df-cnv 3149  df-co 3150  df-dm 3151  df-rn 3152  df-res 3153  df-ima 3154  df-fun 3155  df-fn 3156  df-fv 3161

Copyright terms: Public domain