Theorem fco 3621

Description: Composition of two mappings.

Assertion

Ref	Expression
fco	|- ((F:B-->C /\ G:A-->B) -> (F o. G):A-->C)

Proof of Theorem fco

Step	Hyp	Ref	Expression
1		funco 3536	. . . . . 6 |- ((Fun F /\ Fun G) -> Fun (F o. G))
2		ffun 3615	. . . . . 6 |- (F:B-->C -> Fun F)
3		ffun 3615	. . . . . 6 |- (G:A-->B -> Fun G)
4	1, 2, 3	syl2an 454	. . . . 5 |- ((F:B-->C /\ G:A-->B) -> Fun (F o. G))
5		fdm 3617	. . . . . . . . . 10 |- (F:B-->C -> dom F = B)
6	5	sseq2d 2079	. . . . . . . . 9 |- (F:B-->C -> (ran G (_ dom F <-> ran G (_ B))
7		frn 3618	. . . . . . . . 9 |- (G:A-->B -> ran G (_ B)
8	6, 7	syl5bir 210	. . . . . . . 8 |- (F:B-->C -> (G:A-->B -> ran G (_ dom F))
9	8	imp 350	. . . . . . 7 |- ((F:B-->C /\ G:A-->B) -> ran G (_ dom F)
10		dmcosseq 3349	. . . . . . 7 |- (ran G (_ dom F -> dom ( F o. G) = dom G)
11	9, 10	syl 10	. . . . . 6 |- ((F:B-->C /\ G:A-->B) -> dom ( F o. G) = dom G)
12		fdm 3617	. . . . . . 7 |- (G:A-->B -> dom G = A)
13	12	adantl 388	. . . . . 6 |- ((F:B-->C /\ G:A-->B) -> dom G = A)
14	11, 13	eqtrd 1499	. . . . 5 |- ((F:B-->C /\ G:A-->B) -> dom ( F o. G) = A)
15	4, 14	jca 288	. . . 4 |- ((F:B-->C /\ G:A-->B) -> (Fun (F o. G) /\ dom ( F o. G) = A))
16		df-fn 3183	. . . 4 |- ((F o. G) Fn A <-> (Fun (F o. G) /\ dom ( F o. G) = A))
17	15, 16	sylibr 200	. . 3 |- ((F:B-->C /\ G:A-->B) -> (F o. G) Fn A)
18		rncoss 3348	. . . . 5 |- ran ( F o. G) (_ ran F
19		sstr2 2061	. . . . . 6 |- (ran ( F o. G) (_ ran F -> (ran F (_ C -> ran ( F o. G) (_ C))
20		frn 3618	. . . . . 6 |- (F:B-->C -> ran F (_ C)
21	19, 20	syl5 21	. . . . 5 |- (ran ( F o. G) (_ ran F -> (F:B-->C -> ran ( F o. G) (_ C))
22	18, 21	ax-mp 7	. . . 4 |- (F:B-->C -> ran ( F o. G) (_ C)
23	22	adantr 389	. . 3 |- ((F:B-->C /\ G:A-->B) -> ran ( F o. G) (_ C)
24	17, 23	jca 288	. 2 |- ((F:B-->C /\ G:A-->B) -> ((F o. G) Fn A /\ ran ( F o. G) (_ C))
25		df-f 3184	. 2 |- ((F o. G):A-->C <-> ((F o. G) Fn A /\ ran ( F o. G) (_ C))
26	24, 25	sylibr 200	1 |- ((F:B-->C /\ G:A-->B) -> (F o. G):A-->C)

Syntax hints:   -> wi 3   /\ wa 223   = wceq 953   (_ wss 2037  dom cdm 3160  ran crn 3161   o. ccom 3164  Fun wfun 3166   Fn wfn 3167  -->wf 3168

This theorem is referenced by:  f1co 3652  foco 3667  mapenlem1 4469  mapenlem2 4470  ac6lem 4726  uzrdgfnuz 6243  ruclem17 7469  cnco 7707  cnpco 7708  cnmetba 7842  cnmet 7843  cncfmet 7844  remetba 7848  imsdf 8258  lnocoi 8352  sincolem 8584  hocof 9609  homco1t 9644  homco2t 9817  hmopcot 9863  pjinvar 10029

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-11 964  ax-12 965  ax-13 966  ax-14 967  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452  ax-sep 2693  ax-pow 2732  ax-pr 2769

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 978  df-sb 1168  df-eu 1375  df-mo 1376  df-clab 1457  df-cleq 1462  df-clel 1465  df-ne 1579  df-v 1803  df-dif 2039  df-un 2040  df-in 2041  df-ss 2043  df-nul 2271  df-pw 2392  df-sn 2402  df-pr 2403  df-op 2406  df-br 2610  df-opab 2657  df-id 2824  df-xp 3174  df-rel 3175  df-cnv 3176  df-co 3177  df-dm 3178  df-rn 3179  df-fun 3182  df-fn 3183  df-f 3184

Copyright terms: Public domain