![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > fco | Structured version Visualization version GIF version |
Description: Composition of two functions with domain and codomain as a function with domain and codomain. (Contributed by NM, 29-Aug-1999.) (Proof shortened by Andrew Salmon, 17-Sep-2011.) (Proof shortened by AV, 20-Sep-2024.) |
Ref | Expression |
---|---|
fco | ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → (𝐹 ∘ 𝐺):𝐴⟶𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ffun 6720 | . . 3 ⊢ (𝐺:𝐴⟶𝐵 → Fun 𝐺) | |
2 | fcof 6740 | . . 3 ⊢ ((𝐹:𝐵⟶𝐶 ∧ Fun 𝐺) → (𝐹 ∘ 𝐺):(◡𝐺 “ 𝐵)⟶𝐶) | |
3 | 1, 2 | sylan2 592 | . 2 ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → (𝐹 ∘ 𝐺):(◡𝐺 “ 𝐵)⟶𝐶) |
4 | fimacnv 6739 | . . . . 5 ⊢ (𝐺:𝐴⟶𝐵 → (◡𝐺 “ 𝐵) = 𝐴) | |
5 | 4 | eqcomd 2737 | . . . 4 ⊢ (𝐺:𝐴⟶𝐵 → 𝐴 = (◡𝐺 “ 𝐵)) |
6 | 5 | adantl 481 | . . 3 ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → 𝐴 = (◡𝐺 “ 𝐵)) |
7 | 6 | feq2d 6703 | . 2 ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → ((𝐹 ∘ 𝐺):𝐴⟶𝐶 ↔ (𝐹 ∘ 𝐺):(◡𝐺 “ 𝐵)⟶𝐶)) |
8 | 3, 7 | mpbird 257 | 1 ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → (𝐹 ∘ 𝐺):𝐴⟶𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 = wceq 1540 ◡ccnv 5675 “ cima 5679 ∘ ccom 5680 Fun wfun 6537 ⟶wf 6539 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2153 ax-12 2170 ax-ext 2702 ax-sep 5299 ax-nul 5306 ax-pr 5427 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2533 df-eu 2562 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-ral 3061 df-rex 3070 df-rab 3432 df-v 3475 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-nul 4323 df-if 4529 df-sn 4629 df-pr 4631 df-op 4635 df-br 5149 df-opab 5211 df-id 5574 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 df-fun 6545 df-fn 6546 df-f 6547 |
This theorem is referenced by: fcod 6743 fco2 6744 f1coOLD 6800 mapen 9147 fsuppco2 9404 mapfienlem1 9406 unxpwdom2 9589 wemapwe 9698 cfcoflem 10273 isf34lem7 10380 isf34lem6 10381 inar1 10776 addnqf 10949 mulnqf 10950 axdc4uzlem 13955 seqf1olem2 14015 wrdco 14789 lenco 14790 lo1o1 15483 o1co 15537 caucvgrlem2 15628 fsumcl2lem 15684 fsumadd 15693 fsummulc2 15737 fsumrelem 15760 supcvg 15809 fprodcl2lem 15901 fprodmul 15911 fproddiv 15912 fprodn0 15930 algcvg 16520 cofucl 17845 setccatid 18044 estrccatid 18093 funcestrcsetclem9 18110 funcsetcestrclem9 18125 yonedalem3b 18242 mgmhmco 18645 mhmco 18746 pwsco1mhm 18755 pwsco2mhm 18756 gsumwmhm 18768 efmndcl 18805 f1omvdconj 19362 pmtrfinv 19377 symgtrinv 19388 psgnunilem1 19409 gsumval3lem1 19821 gsumval3 19823 gsumzcl2 19826 gsumzf1o 19828 gsumzaddlem 19837 gsumzmhm 19853 gsumzoppg 19860 gsumzinv 19861 gsumsub 19864 dprdf1o 19950 ablfaclem2 20004 cnfldds 21242 dsmmbas2 21601 f1lindf 21686 lindfmm 21691 psrass1lemOLD 21802 psrnegcl 21825 coe1f2 22051 cpmadumatpolylem1 22702 cnco 23089 cnpco 23090 lmcnp 23127 cnmpt11 23486 cnmpt21 23494 qtopcn 23537 fmco 23784 flfcnp 23827 tsmsf1o 23968 tsmsmhm 23969 tsmssub 23972 imasdsf1olem 24198 nrmmetd 24402 isngp2 24425 isngp3 24426 tngngp2 24488 cnmet 24607 cnfldms 24611 cncfco 24746 cnfldcusp 25204 ovolfioo 25315 ovolficc 25316 ovolfsf 25319 ovollb 25327 ovolctb 25338 ovolicc2lem4 25368 ovolicc2 25370 volsup 25404 uniioovol 25427 uniioombllem3a 25432 uniioombllem3 25433 uniioombllem4 25434 uniioombllem5 25435 uniioombl 25437 mbfdm 25474 ismbfcn 25477 mbfres 25492 mbfimaopnlem 25503 cncombf 25506 limccnp 25739 dvcobrOLD 25797 dvcof 25799 dvcjbr 25800 dvcj 25801 dvmptco 25823 dvlip2 25847 itgsubstlem 25902 coecj 26130 pserulm 26272 jensenlem2 26832 jensen 26833 amgmlem 26834 gamf 26887 dchrinv 27106 motcgrg 28227 vsfval 30318 imsdf 30374 lnocoi 30442 hocofi 31451 homco1 31486 homco2 31662 hmopco 31708 kbass2 31802 kbass5 31805 opsqrlem1 31825 opsqrlem6 31830 pjinvari 31876 fmptco1f1o 32289 fcobij 32379 fcobijfs 32380 mbfmco 33726 dstfrvclim1 33939 reprpmtf1o 34101 mrsubco 34975 mclsppslem 35037 circum 35122 gg-cnfldds 35641 mblfinlem2 36989 mbfresfi 36997 ftc1anclem5 37028 ghomco 37222 rngohomco 37305 tendococl 40106 mapco2g 41914 diophrw 41959 hausgraph 42416 sblpnf 43531 fcoss 44367 limccog 44794 mbfres2cn 45132 volioof 45161 volioofmpt 45168 voliooicof 45170 stoweidlem31 45205 stoweidlem59 45233 subsaliuncllem 45531 sge0resrnlem 45577 hoicvr 45722 ovolval2lem 45817 ovolval2 45818 ovolval3 45821 ovolval4lem1 45823 isomushgr 46952 amgmwlem 48010 |
Copyright terms: Public domain | W3C validator |