Theorem cocanfo 15689

Description: Cancellation of a surjective function from the right side of a composition.

Assertion

Ref	Expression
cocanfo	|- (((F:A-onto->B /\ G Fn B /\ H Fn B) /\ (G o. F) = (H o. F)) -> G = H)

Proof of Theorem cocanfo

Step	Hyp	Ref	Expression
1		dffo3 4792	. . . 4 |- (F:A-onto->B <-> (F:A-->B /\ A.x e. B E.y e. A x = (F` y)))
2		fveq2 4681	. . . . . . . . . . . . . 14 |- (x = (F` y) -> (G` x) = (G` (F` y)))
3		fveq2 4681	. . . . . . . . . . . . . 14 |- (x = (F` y) -> (H` x) = (H` (F` y)))
4	2, 3	eqeq12d 1899	. . . . . . . . . . . . 13 |- (x = (F` y) -> ((G` x) = (H` x) <-> (G` (F` y)) = (H` (F` y))))
5		fvco 4736	. . . . . . . . . . . . . . . . . . . . . 22 |- ((Fun G /\ Fun F /\ y e. dom F) -> ((G o. F)` y) = (G` (F` y)))
6	5	3expb 1068	. . . . . . . . . . . . . . . . . . . . 21 |- ((Fun G /\ (Fun F /\ y e. dom F)) -> ((G o. F)` y) = (G` (F` y)))
7		fnfun 4510	. . . . . . . . . . . . . . . . . . . . 21 |- (G Fn B -> Fun G)
8		ffun 4565	. . . . . . . . . . . . . . . . . . . . . . 23 |- (F:A-->B -> Fun F)
9	8	adantr 425	. . . . . . . . . . . . . . . . . . . . . 22 |- ((F:A-->B /\ y e. A) -> Fun F)
10		fdm 4567	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (F:A-->B -> dom F = A)
11	10	eleq2d 1964	. . . . . . . . . . . . . . . . . . . . . . 23 |- (F:A-->B -> (y e. dom F <-> y e. A))
12	11	biimpar 461	. . . . . . . . . . . . . . . . . . . . . 22 |- ((F:A-->B /\ y e. A) -> y e. dom F)
13	9, 12	jca 310	. . . . . . . . . . . . . . . . . . . . 21 |- ((F:A-->B /\ y e. A) -> (Fun F /\ y e. dom F))
14	6, 7, 13	syl2an 503	. . . . . . . . . . . . . . . . . . . 20 |- ((G Fn B /\ (F:A-->B /\ y e. A)) -> ((G o. F)` y) = (G` (F` y)))
15	14	anassrs 489	. . . . . . . . . . . . . . . . . . 19 |- (((G Fn B /\ F:A-->B) /\ y e. A) -> ((G o. F)` y) = (G` (F` y)))
16	15	ancom1s 548	. . . . . . . . . . . . . . . . . 18 |- (((F:A-->B /\ G Fn B) /\ y e. A) -> ((G o. F)` y) = (G` (F` y)))
17	16	3adantl3 1034	. . . . . . . . . . . . . . . . 17 |- (((F:A-->B /\ G Fn B /\ H Fn B) /\ y e. A) -> ((G o. F)` y) = (G` (F` y)))
18		fvco 4736	. . . . . . . . . . . . . . . . . . . . . 22 |- ((Fun H /\ Fun F /\ y e. dom F) -> ((H o. F)` y) = (H` (F` y)))
19	18	3expb 1068	. . . . . . . . . . . . . . . . . . . . 21 |- ((Fun H /\ (Fun F /\ y e. dom F)) -> ((H o. F)` y) = (H` (F` y)))
20		fnfun 4510	. . . . . . . . . . . . . . . . . . . . 21 |- (H Fn B -> Fun H)
21	19, 20, 13	syl2an 503	. . . . . . . . . . . . . . . . . . . 20 |- ((H Fn B /\ (F:A-->B /\ y e. A)) -> ((H o. F)` y) = (H` (F` y)))
22	21	anassrs 489	. . . . . . . . . . . . . . . . . . 19 |- (((H Fn B /\ F:A-->B) /\ y e. A) -> ((H o. F)` y) = (H` (F` y)))
23	22	ancom1s 548	. . . . . . . . . . . . . . . . . 18 |- (((F:A-->B /\ H Fn B) /\ y e. A) -> ((H o. F)` y) = (H` (F` y)))
24	23	3adantl2 1033	. . . . . . . . . . . . . . . . 17 |- (((F:A-->B /\ G Fn B /\ H Fn B) /\ y e. A) -> ((H o. F)` y) = (H` (F` y)))
25	17, 24	eqeq12d 1899	. . . . . . . . . . . . . . . 16 |- (((F:A-->B /\ G Fn B /\ H Fn B) /\ y e. A) -> (((G o. F)` y) = ((H o. F)` y) <-> (G` (F` y)) = (H` (F` y))))
26	25	biimpa 460	. . . . . . . . . . . . . . 15 |- ((((F:A-->B /\ G Fn B /\ H Fn B) /\ y e. A) /\ ((G o. F)` y) = ((H o. F)` y)) -> (G` (F` y)) = (H` (F` y)))
27		fveq1 4680	. . . . . . . . . . . . . . 15 |- ((G o. F) = (H o. F) -> ((G o. F)` y) = ((H o. F)` y))
28	26, 27	sylan2 500	. . . . . . . . . . . . . 14 |- ((((F:A-->B /\ G Fn B /\ H Fn B) /\ y e. A) /\ (G o. F) = (H o. F)) -> (G` (F` y)) = (H` (F` y)))
29	28	an1rs 547	. . . . . . . . . . . . 13 |- ((((F:A-->B /\ G Fn B /\ H Fn B) /\ (G o. F) = (H o. F)) /\ y e. A) -> (G` (F` y)) = (H` (F` y)))
30	4, 29	syl5cbir 228	. . . . . . . . . . . 12 |- ((((F:A-->B /\ G Fn B /\ H Fn B) /\ (G o. F) = (H o. F)) /\ y e. A) -> (x = (F` y) -> (G` x) = (H` x)))
31	30	r19.23adva 2216	. . . . . . . . . . 11 |- (((F:A-->B /\ G Fn B /\ H Fn B) /\ (G o. F) = (H o. F)) -> (E.y e. A x = (F` y) -> (G` x) = (H` x)))
32	31	3exp1 1084	. . . . . . . . . 10 |- (F:A-->B -> (G Fn B -> (H Fn B -> ((G o. F) = (H o. F) -> (E.y e. A x = (F` y) -> (G` x) = (H` x))))))
33	32	3imp2 1083	. . . . . . . . 9 |- ((F:A-->B /\ (G Fn B /\ H Fn B /\ (G o. F) = (H o. F))) -> (E.y e. A x = (F` y) -> (G` x) = (H` x)))
34	33	ralimdv 2172	. . . . . . . 8 |- ((F:A-->B /\ (G Fn B /\ H Fn B /\ (G o. F) = (H o. F))) -> (A.x e. B E.y e. A x = (F` y) -> A.x e. B (G` x) = (H` x)))
35	34	ex 402	. . . . . . 7 |- (F:A-->B -> ((G Fn B /\ H Fn B /\ (G o. F) = (H o. F)) -> (A.x e. B E.y e. A x = (F` y) -> A.x e. B (G` x) = (H` x))))
36	35	com23 36	. . . . . 6 |- (F:A-->B -> (A.x e. B E.y e. A x = (F` y) -> ((G Fn B /\ H Fn B /\ (G o. F) = (H o. F)) -> A.x e. B (G` x) = (H` x))))
37	36	imp 377	. . . . 5 |- ((F:A-->B /\ A.x e. B E.y e. A x = (F` y)) -> ((G Fn B /\ H Fn B /\ (G o. F) = (H o. F)) -> A.x e. B (G` x) = (H` x)))
38	37	3expd 1085	. . . 4 |- ((F:A-->B /\ A.x e. B E.y e. A x = (F` y)) -> (G Fn B -> (H Fn B -> ((G o. F) = (H o. F) -> A.x e. B (G` x) = (H` x)))))
39	1, 38	sylbi 216	. . 3 |- (F:A-onto->B -> (G Fn B -> (H Fn B -> ((G o. F) = (H o. F) -> A.x e. B (G` x) = (H` x)))))
40	39	3imp1 1081	. 2 |- (((F:A-onto->B /\ G Fn B /\ H Fn B) /\ (G o. F) = (H o. F)) -> A.x e. B (G` x) = (H` x))
41		eqfnfv2 4767	. . . 4 |- ((G Fn B /\ H Fn B) -> (G = H <-> A.x e. B (G` x) = (H` x)))
42	41	3adant1 894	. . 3 |- ((F:A-onto->B /\ G Fn B /\ H Fn B) -> (G = H <-> A.x e. B (G` x) = (H` x)))
43	42	adantr 425	. 2 |- (((F:A-onto->B /\ G Fn B /\ H Fn B) /\ (G o. F) = (H o. F)) -> (G = H <-> A.x e. B (G` x) = (H` x)))
44	40, 43	mpbird 213	1 |- (((F:A-onto->B /\ G Fn B /\ H Fn B) /\ (G o. F) = (H o. F)) -> G = H)

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  A.wral 2105  E.wrex 2106  dom cdm 3986   o. ccom 3990  Fun wfun 3992   Fn wfn 3993  -->wf 3994  -onto->wfo 3996  ` 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-13 1311  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  ax-un 3790

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-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-f 4010  df-fo 4012  df-fv 4014

Copyright terms: Public domain