Theorem eqfnfv 4766

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 1896	. . . . 5 |- ((dom F = A /\ dom G = B) -> (dom F = dom G <-> A = B))
2		dmeq 4157	. . . . 5 |- (F = G -> dom F = dom G)
3	1, 2	syl5bi 225	. . . 4 |- ((dom F = A /\ dom G = B) -> (F = G -> A = B))
4		fndm 4512	. . . 4 |- (F Fn A -> dom F = A)
5		fndm 4512	. . . 4 |- (G Fn B -> dom G = B)
6	3, 4, 5	syl2an 503	. . 3 |- ((F Fn A /\ G Fn B) -> (F = G -> A = B))
7		fveq1 4680	. . . . . 6 |- (F = G -> (F` x) = (G` x))
8	7	a1d 15	. . . . 5 |- (F = G -> (x e. A -> (F` x) = (G` x)))
9	8	r19.21aiv 2175	. . . 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 661	. 2 |- ((F Fn A /\ G Fn B) -> (F = G -> (A = B /\ A.x e. A (F` x) = (G` x))))
12		visset 2295	. . . . . . . . . . . . . . . . 17 |- y e. _V
13	12	fnopfvb 4713	. . . . . . . . . . . . . . . 16 |- ((F Fn A /\ x e. A) -> ((F` x) = y <-> <.x, y>. e. F))
14	13	adantlr 429	. . . . . . . . . . . . . . 15 |- (((F Fn A /\ G Fn A) /\ x e. A) -> ((F` x) = y <-> <.x, y>. e. F))
15	12	fnopfvb 4713	. . . . . . . . . . . . . . . 16 |- ((G Fn A /\ x e. A) -> ((G` x) = y <-> <.x, y>. e. G))
16	15	adantll 428	. . . . . . . . . . . . . . 15 |- (((F Fn A /\ G Fn A) /\ x e. A) -> ((G` x) = y <-> <.x, y>. e. G))
17	14, 16	bibi12d 691	. . . . . . . . . . . . . 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 1890	. . . . . . . . . . . . . 14 |- ((F` x) = (G` x) -> ((F` x) = y <-> (G` x) = y))
19	17, 18	syl5bi 225	. . . . . . . . . . . . 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 402	. . . . . . . . . . . 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 16	. . . . . . . . . . 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 39	. . . . . . . . . 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 1964	. . . . . . . . . . . . . 14 |- (F Fn A -> (x e. dom F <-> x e. A))
24		visset 2295	. . . . . . . . . . . . . . 15 |- x e. _V
25	24	opeldm 4160	. . . . . . . . . . . . . 14 |- (<.x, y>. e. F -> x e. dom F)
26	23, 25	syl5bi 225	. . . . . . . . . . . . 13 |- (F Fn A -> (<.x, y>. e. F -> x e. A))
27	26	con3d 111	. . . . . . . . . . . 12 |- (F Fn A -> (-. x e. A -> -. <.x, y>. e. F))
28		fndm 4512	. . . . . . . . . . . . . . 15 |- (G Fn A -> dom G = A)
29	28	eleq2d 1964	. . . . . . . . . . . . . 14 |- (G Fn A -> (x e. dom G <-> x e. A))
30	24	opeldm 4160	. . . . . . . . . . . . . 14 |- (<.x, y>. e. G -> x e. dom G)
31	29, 30	syl5bi 225	. . . . . . . . . . . . 13 |- (G Fn A -> (<.x, y>. e. G -> x e. A))
32	31	con3d 111	. . . . . . . . . . . 12 |- (G Fn A -> (-. x e. A -> -. <.x, y>. e. G))
33	27, 32	anim12ii 618	. . . . . . . . . . 11 |- ((F Fn A /\ G Fn A) -> (-. x e. A -> (-. <.x, y>. e. F /\ -. <.x, y>. e. G)))
34		pm5.21 741	. . . . . . . . . . . 12 |- ((-. <.x, y>. e. F /\ -. <.x, y>. e. G) -> (<.x, y>. e. F <-> <.x, y>. e. G))
35	34	a1d 15	. . . . . . . . . . 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 64	. . . . . . . . . 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 140	. . . . . . . . 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 1666	. . . . . . . 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	alimdv 1668	. . . . . . 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 2109	. . . . . . 7 |- (A.x e. A (F` x) = (G` x) <-> A.x(x e. A -> (F` x) = (G` x)))
41	39, 40	syl5ib 223	. . . . . 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 4077	. . . . . . 7 |- ((Rel F /\ Rel G) -> (F = G <-> A.xA.y(<.x, y>. e. F <-> <.x, y>. e. G)))
43		fnrel 4511	. . . . . . 7 |- (F Fn A -> Rel F)
44		fnrel 4511	. . . . . . 7 |- (G Fn A -> Rel G)
45	42, 43, 44	syl2an 503	. . . . . 6 |- ((F Fn A /\ G Fn A) -> (F = G <-> A.xA.y(<.x, y>. e. F <-> <.x, y>. e. G)))
46	41, 45	sylibrd 221	. . . . 5 |- ((F Fn A /\ G Fn A) -> (A.x e. A (F` x) = (G` x) -> F = G))
47		fneq2 4504	. . . . . 6 |- (A = B -> (G Fn A <-> G Fn B))
48	47	biimparc 463	. . . . 5 |- ((G Fn B /\ A = B) -> G Fn A)
49	46, 48	sylan2 500	. . . 4 |- ((F Fn A /\ (G Fn B /\ A = B)) -> (A.x e. A (F` x) = (G` x) -> F = G))
50	49	exp32 408	. . 3 |- (F Fn A -> (G Fn B -> (A = B -> (A.x e. A (F` x) = (G` x) -> F = G))))
51	50	imp4b 392	. 2 |- ((F Fn A /\ G Fn B) -> ((A = B /\ A.x e. A (F` x) = (G` x)) -> F = G))
52	11, 51	impbid 574	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 163   /\ wa 240  A.wal 1296   = wceq 1298   e. wcel 1300  A.wral 2105  <.cop 3046  dom cdm 3986  Rel wrel 3991   Fn wfn 3993  ` cfv 3998

This theorem is referenced by:  eqfnfv2 4767  eqfnfv2OLD 4768  eqfnfv3 4769  eqfnoprv 4945  tfr3 5134  oprabco 10159  upxp 10225  uptx 10226  txcnopab 10228  eqfunfv 13839  soseq 13955  wfr3g 13956  frr3g 13980  axdenselem4 14022  njtlc 14389  eqfnung2 14459  cbicplem 14508  fnopabco 15711  eqfnfv3OLD 15721  upixp 15729  sdclem1 15809  rrnmet 16016  phtpycolem3 16053  phtpycolem4 16054  pcocn 16076  pcohtpylem3 16082

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-br 3339  df-opab 3396  df-id 3586  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-fv 4014

Copyright terms: Public domain