Theorem eqfnfv 3797

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 1487	. . . . 5 |- ((dom F = A /\ dom G = B) -> (dom F = dom G <-> A = B))
2		dmeq 3311	. . . . 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 3587	. . . 4 |- (F Fn A -> dom F = A)
5		fndm 3587	. . . 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 3723	. . . . . 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 1713	. . . 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 600	. 2 |- ((F Fn A /\ G Fn B) -> (F = G -> (A = B /\ A.x e. A (F` x) = (G` x))))
12		visset 1813	. . . . . . . . . . . . . . . . 17 |- y e. V
13	12	fnopfvb 3754	. . . . . . . . . . . . . . . 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 3754	. . . . . . . . . . . . . . . 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 629	. . . . . . . . . . . . . 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 1481	. . . . . . . . . . . . . 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 1541	. . . . . . . . . . . . . 14 |- (F Fn A -> (x e. dom F <-> x e. A))
24		visset 1813	. . . . . . . . . . . . . . 15 |- x e. V
25	24	opeldm 3314	. . . . . . . . . . . . . 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 3587	. . . . . . . . . . . . . . 15 |- (G Fn A -> dom G = A)
29	28	eleq2d 1541	. . . . . . . . . . . . . 14 |- (G Fn A -> (x e. dom G <-> x e. A))
30	24	opeldm 3314	. . . . . . . . . . . . . 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 559	. . . . . . . . . . 11 |- ((F Fn A /\ G Fn A) -> (-. x e. A -> (-. <.x, y>. e. F /\ -. <.x, y>. e. G)))
34		pm5.21 677	. . . . . . . . . . . 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 1288	. . . . . . . 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 1289	. . . . . . 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 1649	. . . . . . 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 3250	. . . . . . 7 |- ((Rel F /\ Rel G) -> (F = G <-> A.xA.y(<.x, y>. e. F <-> <.x, y>. e. G)))
43		fnrel 3586	. . . . . . 7 |- (F Fn A -> Rel F)
44		fnrel 3586	. . . . . . 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 3583	. . . . . 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 516	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 954   = wceq 956   e. wcel 958  A.wral 1645  <.cop 2411  dom cdm 3170  Rel wrel 3175   Fn wfn 3177  ` cfv 3182

This theorem is referenced by:  eqfnfvf 3798  fvreseq 3799  fconst2g 3845  tfr3 3926  eqfnoprval 4016  curry1 4098  df1st2 4126  df2nd2 4127  mapenlem2 4490  seq1res 6327  seq1shftid 6356  seq1seqz 6541  seq1seq0 6545  seqzeq 6555  seqzres 6560  seqzres2 6561  invfval 8261  sspn 8395  nmlno0lem 8453  phoeqi 8518  sinco 8667  cosco 8668  shftefif1olem 8741  dfiop2 9679  hoeqt 9686  ho01 9754  hoeq1t 9756  kbpjt 9880  nmlnop0ALT 9920  lnopco0 9929  lnopcon 9963  lnfncon 9990  hmopidmpj 10080  pjssdif2 10102  pjinvar 10119  cayleylem2 10410

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-11 967  ax-12 968  ax-13 969  ax-14 970  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459  ax-sep 2703  ax-pow 2742  ax-pr 2779

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 981  df-sb 1172  df-eu 1382  df-mo 1383  df-clab 1464  df-cleq 1469  df-clel 1472  df-ne 1587  df-ral 1649  df-rex 1650  df-v 1812  df-dif 2049  df-un 2050  df-in 2051  df-ss 2053  df-nul 2281  df-pw 2402  df-sn 2412  df-pr 2413  df-op 2416  df-uni 2504  df-br 2620  df-opab 2667  df-id 2835  df-xp 3184  df-rel 3185  df-cnv 3186  df-co 3187  df-dm 3188  df-rn 3189  df-res 3190  df-ima 3191  df-fun 3192  df-fn 3193  df-fv 3198

Copyright terms: Public domain