Theorem fco 3711

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 3625	. . . . . 6 |- ((Fun F /\ Fun G) -> Fun (F o. G))
2		ffun 3704	. . . . . 6 |- (F:B-->C -> Fun F)
3		ffun 3704	. . . . . 6 |- (G:A-->B -> Fun G)
4	1, 2, 3	syl2an 456	. . . . 5 |- ((F:B-->C /\ G:A-->B) -> Fun (F o. G))
5		fdm 3706	. . . . . . . . . 10 |- (F:B-->C -> dom F = B)
6	5	sseq2d 2133	. . . . . . . . 9 |- (F:B-->C -> (ran G (_ dom F <-> ran G (_ B))
7		frn 3708	. . . . . . . . 9 |- (G:A-->B -> ran G (_ B)
8	6, 7	syl5bir 208	. . . . . . . 8 |- (F:B-->C -> (G:A-->B -> ran G (_ dom F))
9	8	imp 348	. . . . . . 7 |- ((F:B-->C /\ G:A-->B) -> ran G (_ dom F)
10		dmcosseq 3425	. . . . . . 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 3706	. . . . . . 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 1544	. . . . 5 |- ((F:B-->C /\ G:A-->B) -> dom ( F o. G) = A)
15	4, 14	jca 286	. . . 4 |- ((F:B-->C /\ G:A-->B) -> (Fun (F o. G) /\ dom ( F o. G) = A))
16		df-fn 3248	. . . 4 |- ((F o. G) Fn A <-> (Fun (F o. G) /\ dom ( F o. G) = A))
17	15, 16	sylibr 198	. . 3 |- ((F:B-->C /\ G:A-->B) -> (F o. G) Fn A)
18		rncoss 3424	. . . . 5 |- ran ( F o. G) (_ ran F
19		sstr2 2115	. . . . . 6 |- (ran ( F o. G) (_ ran F -> (ran F (_ C -> ran ( F o. G) (_ C))
20		frn 3708	. . . . . 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 286	. 2 |- ((F:B-->C /\ G:A-->B) -> ((F o. G) Fn A /\ ran ( F o. G) (_ C))
25		df-f 3249	. 2 |- ((F o. G):A-->C <-> ((F o. G) Fn A /\ ran ( F o. G) (_ C))
26	24, 25	sylibr 198	1 |- ((F:B-->C /\ G:A-->B) -> (F o. G):A-->C)

Syntax hints:   -> wi 3   /\ wa 221   = wceq 988   (_ wss 2091  dom cdm 3225  ran crn 3226   o. ccom 3229  Fun wfun 3231   Fn wfn 3232  -->wf 3233

This theorem is referenced by:  f1co 3742  foco 3758  mapenlem1 4578  mapenlem2 4579  ac6lem 4840  uzrdgfnuzi 6599  ruclem17 7651  cnco 7888  cnpco 7889  cnmetba 8023  cnmet 8024  cncfmet 8025  remetba 8029  imsdf 8439  lnocoi 8537  sincolem 8783  hocofi 9812  homco1 9847  homco2 10018  hmopco 10065  pjinvari 10237

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 994  ax-gen 995  ax-8 996  ax-10 998  ax-11 999  ax-12 1000  ax-13 1001  ax-14 1002  ax-17 1003  ax-4 1005  ax-5o 1007  ax-6o 1010  ax-9o 1155  ax-10o 1173  ax-16 1243  ax-11o 1251  ax-ext 1494  ax-sep 2754  ax-pow 2794  ax-pr 2832

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-ex 1013  df-sb 1205  df-eu 1415  df-mo 1416  df-clab 1500  df-cleq 1505  df-clel 1508  df-ne 1624  df-v 1850  df-dif 2093  df-un 2094  df-in 2095  df-ss 2097  df-nul 2325  df-pw 2447  df-sn 2457  df-pr 2458  df-op 2461  df-br 2670  df-opab 2718  df-id 2889  df-xp 3239  df-rel 3240  df-cnv 3241  df-co 3242  df-dm 3243  df-rn 3244  df-fun 3247  df-fn 3248  df-f 3249

Copyright terms: Public domain