![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > fco | Structured version Visualization version GIF version |
Description: Composition of two mappings. (Contributed by NM, 29-Aug-1999.) (Proof shortened by Andrew Salmon, 17-Sep-2011.) |
Ref | Expression |
---|---|
fco | ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → (𝐹 ∘ 𝐺):𝐴⟶𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-f 6127 | . . 3 ⊢ (𝐹:𝐵⟶𝐶 ↔ (𝐹 Fn 𝐵 ∧ ran 𝐹 ⊆ 𝐶)) | |
2 | df-f 6127 | . . 3 ⊢ (𝐺:𝐴⟶𝐵 ↔ (𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵)) | |
3 | fnco 6232 | . . . . . . 7 ⊢ ((𝐹 Fn 𝐵 ∧ 𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵) → (𝐹 ∘ 𝐺) Fn 𝐴) | |
4 | 3 | 3expib 1156 | . . . . . 6 ⊢ (𝐹 Fn 𝐵 → ((𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵) → (𝐹 ∘ 𝐺) Fn 𝐴)) |
5 | 4 | adantr 474 | . . . . 5 ⊢ ((𝐹 Fn 𝐵 ∧ ran 𝐹 ⊆ 𝐶) → ((𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵) → (𝐹 ∘ 𝐺) Fn 𝐴)) |
6 | rncoss 5619 | . . . . . . 7 ⊢ ran (𝐹 ∘ 𝐺) ⊆ ran 𝐹 | |
7 | sstr 3835 | . . . . . . 7 ⊢ ((ran (𝐹 ∘ 𝐺) ⊆ ran 𝐹 ∧ ran 𝐹 ⊆ 𝐶) → ran (𝐹 ∘ 𝐺) ⊆ 𝐶) | |
8 | 6, 7 | mpan 681 | . . . . . 6 ⊢ (ran 𝐹 ⊆ 𝐶 → ran (𝐹 ∘ 𝐺) ⊆ 𝐶) |
9 | 8 | adantl 475 | . . . . 5 ⊢ ((𝐹 Fn 𝐵 ∧ ran 𝐹 ⊆ 𝐶) → ran (𝐹 ∘ 𝐺) ⊆ 𝐶) |
10 | 5, 9 | jctird 522 | . . . 4 ⊢ ((𝐹 Fn 𝐵 ∧ ran 𝐹 ⊆ 𝐶) → ((𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵) → ((𝐹 ∘ 𝐺) Fn 𝐴 ∧ ran (𝐹 ∘ 𝐺) ⊆ 𝐶))) |
11 | 10 | imp 397 | . . 3 ⊢ (((𝐹 Fn 𝐵 ∧ ran 𝐹 ⊆ 𝐶) ∧ (𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵)) → ((𝐹 ∘ 𝐺) Fn 𝐴 ∧ ran (𝐹 ∘ 𝐺) ⊆ 𝐶)) |
12 | 1, 2, 11 | syl2anb 591 | . 2 ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → ((𝐹 ∘ 𝐺) Fn 𝐴 ∧ ran (𝐹 ∘ 𝐺) ⊆ 𝐶)) |
13 | df-f 6127 | . 2 ⊢ ((𝐹 ∘ 𝐺):𝐴⟶𝐶 ↔ ((𝐹 ∘ 𝐺) Fn 𝐴 ∧ ran (𝐹 ∘ 𝐺) ⊆ 𝐶)) | |
14 | 12, 13 | sylibr 226 | 1 ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → (𝐹 ∘ 𝐺):𝐴⟶𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 ⊆ wss 3798 ran crn 5343 ∘ ccom 5346 Fn wfn 6118 ⟶wf 6119 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1894 ax-4 1908 ax-5 2009 ax-6 2075 ax-7 2112 ax-9 2173 ax-10 2192 ax-11 2207 ax-12 2220 ax-13 2389 ax-ext 2803 ax-sep 5005 ax-nul 5013 ax-pr 5127 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 879 df-3an 1113 df-tru 1660 df-ex 1879 df-nf 1883 df-sb 2068 df-mo 2605 df-eu 2640 df-clab 2812 df-cleq 2818 df-clel 2821 df-nfc 2958 df-ral 3122 df-rex 3123 df-rab 3126 df-v 3416 df-dif 3801 df-un 3803 df-in 3805 df-ss 3812 df-nul 4145 df-if 4307 df-sn 4398 df-pr 4400 df-op 4404 df-br 4874 df-opab 4936 df-id 5250 df-xp 5348 df-rel 5349 df-cnv 5350 df-co 5351 df-dm 5352 df-rn 5353 df-fun 6125 df-fn 6126 df-f 6127 |
This theorem is referenced by: fco2 6296 f1co 6348 foco 6365 mapen 8393 fsuppco2 8577 mapfienlem1 8579 mapfienlem3 8581 mapfien 8582 unxpwdom2 8762 wemapwe 8871 cofsmo 9406 cfcoflem 9409 isf34lem7 9516 isf34lem6 9517 canthp1lem2 9790 inar1 9912 addnqf 10085 mulnqf 10086 axdc4uzlem 13077 seqf1olem2 13135 wrdco 13952 lenco 13953 lo1o1 14640 o1co 14694 caucvgrlem2 14782 fsumcl2lem 14839 fsumadd 14847 fsummulc2 14890 fsumrelem 14913 supcvg 14962 fprodcl2lem 15053 fprodmul 15063 fproddiv 15064 fprodn0 15082 algcvg 15662 cofucl 16900 setccatid 17086 estrccatid 17124 funcestrcsetclem9 17141 funcsetcestrclem9 17156 yonedalem3b 17272 mhmco 17715 pwsco1mhm 17723 pwsco2mhm 17724 gsumwmhm 17736 f1omvdconj 18216 pmtrfinv 18231 symgtrinv 18242 psgnunilem1 18263 gsumval3lem1 18659 gsumval3lem2 18660 gsumval3 18661 gsumzcl2 18664 gsumzf1o 18666 gsumzaddlem 18674 gsumzmhm 18690 gsumzoppg 18697 gsumzinv 18698 gsumsub 18701 dprdf1o 18785 ablfaclem2 18839 psrass1lem 19738 psrnegcl 19757 coe1f2 19939 cnfldds 20116 dsmmbas2 20444 f1lindf 20528 lindfmm 20533 cpmadumatpolylem1 21056 cnco 21441 cnpco 21442 lmcnp 21479 cnmpt11 21837 cnmpt21 21845 qtopcn 21888 fmco 22135 flfcnp 22178 tsmsf1o 22318 tsmsmhm 22319 tsmssub 22322 imasdsf1olem 22548 comet 22688 nrmmetd 22749 isngp2 22771 isngp3 22772 tngngp2 22826 cnmet 22945 cnfldms 22949 cncfco 23080 cnfldcusp 23525 ovolfioo 23633 ovolficc 23634 ovolfsf 23637 ovollb 23645 ovolctb 23656 ovolicc2lem4 23686 ovolicc2 23688 volsup 23722 uniioovol 23745 uniioombllem3a 23750 uniioombllem3 23751 uniioombllem4 23752 uniioombllem5 23753 uniioombl 23755 mbfdm 23792 ismbfcn 23795 mbfres 23810 mbfimaopnlem 23821 cncombf 23824 limccnp 24054 dvcobr 24108 dvcof 24110 dvcjbr 24111 dvcj 24112 dvmptco 24134 dvlip2 24157 itgsubstlem 24210 coecj 24433 pserulm 24575 jensenlem2 25127 jensen 25128 amgmlem 25129 gamf 25182 dchrinv 25399 motcgrg 25856 vsfval 28032 imsdf 28088 lnocoi 28156 hocofi 29169 homco1 29204 homco2 29380 hmopco 29426 kbass2 29520 kbass5 29523 opsqrlem1 29543 opsqrlem6 29548 pjinvari 29594 fmptco1f1o 29972 fcobij 30037 fcobijfs 30038 mbfmco 30860 dstfrvclim1 31074 reprpmtf1o 31242 subfacp1lem5 31701 mrsubco 31953 mclsppslem 32015 circum 32101 mblfinlem2 33984 mbfresfi 33992 ftc1anclem5 34025 ghomco 34225 rngohomco 34308 tendococl 36840 mapco2g 38114 diophrw 38159 hausgraph 38626 sblpnf 39342 fcoss 40201 fcod 40221 limccog 40640 mbfres2cn 40961 volioof 40991 volioofmpt 40998 voliooicof 41000 stoweidlem31 41035 stoweidlem59 41063 subsaliuncllem 41359 sge0resrnlem 41404 hoicvr 41549 ovolval2lem 41644 ovolval2 41645 ovolval3 41648 ovolval4lem1 41650 ovolval5lem3 41655 isomushgr 42537 mgmhmco 42641 amgmwlem 43437 |
Copyright terms: Public domain | W3C validator |