Theorem eqfnung2 14459

Description: If a family of sets A indexed by I covers the common domain B of two functions F and G, the restrictions of F and G to (A i^i B) are equal iff F = G. Compare eqfnun 15705.

Assertion

Ref	Expression
eqfnung2	|- ((B C_ U_i e. I A /\ F Fn B /\ G Fn B) -> (A.i e. I (F |` A) = (G |` A) <-> F = G))

Distinct variable groups:   i,F   i,G

Proof of Theorem eqfnung2

Step	Hyp	Ref	Expression
1		eqidd 1885	. . . . 5 |- (((B C_ U_i e. I A /\ F Fn B /\ G Fn B) /\ A.i e. I (F |` A) = (G |` A)) -> B = B)
2		ssel 2615	. . . . . . . . . . . 12 |- (B C_ U_i e. I A -> (x e. B -> x e. U_i e. I A))
3		eliun 3259	. . . . . . . . . . . . 13 |- (x e. U_i e. I A <-> E.i e. I x e. A)
4		r19.29 2227	. . . . . . . . . . . . . . . . . 18 |- ((A.i e. I (F |` A) = (G |` A) /\ E.i e. I x e. A) -> E.i e. I ((F |` A) = (G |` A) /\ x e. A))
5		fveq1 4680	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((F |` A) = (G |` A) -> ((F |` A)` x) = ((G |` A)` x))
6		fvres 4691	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (x e. A -> ((F |` A)` x) = (F` x))
7		fvres 4691	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (x e. A -> ((G |` A)` x) = (G` x))
8		eqeq12 1896	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((((F |` A)` x) = (F` x) /\ ((G |` A)` x) = (G` x)) -> (((F |` A)` x) = ((G |` A)` x) <-> (F` x) = (G` x)))
9	8	biimpd 170	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((((F |` A)` x) = (F` x) /\ ((G |` A)` x) = (G` x)) -> (((F |` A)` x) = ((G |` A)` x) -> (F` x) = (G` x)))
10	6, 7, 9	syl11anc 524	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (x e. A -> (((F |` A)` x) = ((G |` A)` x) -> (F` x) = (G` x)))
11	5, 10	mpan9 521	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((F |` A) = (G |` A) /\ x e. A) -> (F` x) = (G` x))
12	11	r19.23aivr 14294	. . . . . . . . . . . . . . . . . . . . . 22 |- (E.i e. I ((F |` A) = (G |` A) /\ x e. A) -> (F` x) = (G` x))
13	12	a1d 15	. . . . . . . . . . . . . . . . . . . . 21 |- (E.i e. I ((F |` A) = (G |` A) /\ x e. A) -> (B C_ U_i e. I A -> (F` x) = (G` x)))
14	13	a1i 8	. . . . . . . . . . . . . . . . . . . 20 |- (x e. B -> (E.i e. I ((F |` A) = (G |` A) /\ x e. A) -> (B C_ U_i e. I A -> (F` x) = (G` x))))
15	14	a1i12 9	. . . . . . . . . . . . . . . . . . 19 |- (F Fn B -> (G Fn B -> (x e. B -> (E.i e. I ((F |` A) = (G |` A) /\ x e. A) -> (B C_ U_i e. I A -> (F` x) = (G` x))))))
16	15	com4r 45	. . . . . . . . . . . . . . . . . 18 |- (E.i e. I ((F |` A) = (G |` A) /\ x e. A) -> (F Fn B -> (G Fn B -> (x e. B -> (B C_ U_i e. I A -> (F` x) = (G` x))))))
17	4, 16	syl 12	. . . . . . . . . . . . . . . . 17 |- ((A.i e. I (F |` A) = (G |` A) /\ E.i e. I x e. A) -> (F Fn B -> (G Fn B -> (x e. B -> (B C_ U_i e. I A -> (F` x) = (G` x))))))
18	17	ex 402	. . . . . . . . . . . . . . . 16 |- (A.i e. I (F |` A) = (G |` A) -> (E.i e. I x e. A -> (F Fn B -> (G Fn B -> (x e. B -> (B C_ U_i e. I A -> (F` x) = (G` x)))))))
19	18	com4t 44	. . . . . . . . . . . . . . 15 |- (F Fn B -> (G Fn B -> (A.i e. I (F |` A) = (G |` A) -> (E.i e. I x e. A -> (x e. B -> (B C_ U_i e. I A -> (F` x) = (G` x)))))))
20	19	3imp 1061	. . . . . . . . . . . . . 14 |- ((F Fn B /\ G Fn B /\ A.i e. I (F |` A) = (G |` A)) -> (E.i e. I x e. A -> (x e. B -> (B C_ U_i e. I A -> (F` x) = (G` x)))))
21	20	com3l 38	. . . . . . . . . . . . 13 |- (E.i e. I x e. A -> (x e. B -> ((F Fn B /\ G Fn B /\ A.i e. I (F |` A) = (G |` A)) -> (B C_ U_i e. I A -> (F` x) = (G` x)))))
22	3, 21	sylbi 216	. . . . . . . . . . . 12 |- (x e. U_i e. I A -> (x e. B -> ((F Fn B /\ G Fn B /\ A.i e. I (F |` A) = (G |` A)) -> (B C_ U_i e. I A -> (F` x) = (G` x)))))
23	2, 22	syl6com 64	. . . . . . . . . . 11 |- (x e. B -> (B C_ U_i e. I A -> (x e. B -> ((F Fn B /\ G Fn B /\ A.i e. I (F |` A) = (G |` A)) -> (B C_ U_i e. I A -> (F` x) = (G` x))))))
24	23	pm2.43a 80	. . . . . . . . . 10 |- (x e. B -> (B C_ U_i e. I A -> ((F Fn B /\ G Fn B /\ A.i e. I (F |` A) = (G |` A)) -> (B C_ U_i e. I A -> (F` x) = (G` x)))))
25	24	com14 42	. . . . . . . . 9 |- (B C_ U_i e. I A -> (B C_ U_i e. I A -> ((F Fn B /\ G Fn B /\ A.i e. I (F |` A) = (G |` A)) -> (x e. B -> (F` x) = (G` x)))))
26	25	pm2.43i 78	. . . . . . . 8 |- (B C_ U_i e. I A -> ((F Fn B /\ G Fn B /\ A.i e. I (F |` A) = (G |` A)) -> (x e. B -> (F` x) = (G` x))))
27	26	3expd 1085	. . . . . . 7 |- (B C_ U_i e. I A -> (F Fn B -> (G Fn B -> (A.i e. I (F |` A) = (G |` A) -> (x e. B -> (F` x) = (G` x))))))
28	27	3imp1 1081	. . . . . 6 |- (((B C_ U_i e. I A /\ F Fn B /\ G Fn B) /\ A.i e. I (F |` A) = (G |` A)) -> (x e. B -> (F` x) = (G` x)))
29	28	r19.21aiv 2175	. . . . 5 |- (((B C_ U_i e. I A /\ F Fn B /\ G Fn B) /\ A.i e. I (F |` A) = (G |` A)) -> A.x e. B (F` x) = (G` x))
30	1, 29	jca 310	. . . 4 |- (((B C_ U_i e. I A /\ F Fn B /\ G Fn B) /\ A.i e. I (F |` A) = (G |` A)) -> (B = B /\ A.x e. B (F` x) = (G` x)))
31		3simpc 874	. . . . . 6 |- ((B C_ U_i e. I A /\ F Fn B /\ G Fn B) -> (F Fn B /\ G Fn B))
32	31	adantr 425	. . . . 5 |- (((B C_ U_i e. I A /\ F Fn B /\ G Fn B) /\ A.i e. I (F |` A) = (G |` A)) -> (F Fn B /\ G Fn B))
33		eqfnfv 4766	. . . . 5 |- ((F Fn B /\ G Fn B) -> (F = G <-> (B = B /\ A.x e. B (F` x) = (G` x))))
34	32, 33	syl 12	. . . 4 |- (((B C_ U_i e. I A /\ F Fn B /\ G Fn B) /\ A.i e. I (F |` A) = (G |` A)) -> (F = G <-> (B = B /\ A.x e. B (F` x) = (G` x))))
35	30, 34	mpbird 213	. . 3 |- (((B C_ U_i e. I A /\ F Fn B /\ G Fn B) /\ A.i e. I (F |` A) = (G |` A)) -> F = G)
36	35	ex 402	. 2 |- ((B C_ U_i e. I A /\ F Fn B /\ G Fn B) -> (A.i e. I (F |` A) = (G |` A) -> F = G))
37		reseq1 4218	. . . 4 |- (F = G -> (F |` A) = (G |` A))
38	37	adantr 425	. . 3 |- ((F = G /\ i e. I) -> (F |` A) = (G |` A))
39	38	r19.21aiva 2176	. 2 |- (F = G -> A.i e. I (F |` A) = (G |` A))
40	36, 39	impbid1 575	1 |- ((B C_ U_i e. I A /\ F Fn B /\ G Fn B) -> (A.i e. I (F |` A) = (G |` A) <-> F = G))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  A.wral 2105  E.wrex 2106   C_ wss 2593  U_ciun 3255   |` cres 3988   Fn wfn 3993  ` cfv 3998

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-3an 860  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-iun 3257  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