Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > fvco2 | Structured version Visualization version GIF version |
Description: Value of a function composition. Similar to second part of Theorem 3H of [Enderton] p. 47. (Contributed by NM, 9-Oct-2004.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) (Revised by Stefan O'Rear, 16-Oct-2014.) |
Ref | Expression |
---|---|
fvco2 | ⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → ((𝐹 ∘ 𝐺)‘𝑋) = (𝐹‘(𝐺‘𝑋))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fnsnfv 6736 | . . . . . 6 ⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → {(𝐺‘𝑋)} = (𝐺 “ {𝑋})) | |
2 | 1 | imaeq2d 5922 | . . . . 5 ⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝐹 “ {(𝐺‘𝑋)}) = (𝐹 “ (𝐺 “ {𝑋}))) |
3 | imaco 6097 | . . . . 5 ⊢ ((𝐹 ∘ 𝐺) “ {𝑋}) = (𝐹 “ (𝐺 “ {𝑋})) | |
4 | 2, 3 | syl6reqr 2873 | . . . 4 ⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → ((𝐹 ∘ 𝐺) “ {𝑋}) = (𝐹 “ {(𝐺‘𝑋)})) |
5 | 4 | eleq2d 2896 | . . 3 ⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝑥 ∈ ((𝐹 ∘ 𝐺) “ {𝑋}) ↔ 𝑥 ∈ (𝐹 “ {(𝐺‘𝑋)}))) |
6 | 5 | iotabidv 6332 | . 2 ⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → (℩𝑥𝑥 ∈ ((𝐹 ∘ 𝐺) “ {𝑋})) = (℩𝑥𝑥 ∈ (𝐹 “ {(𝐺‘𝑋)}))) |
7 | dffv3 6659 | . 2 ⊢ ((𝐹 ∘ 𝐺)‘𝑋) = (℩𝑥𝑥 ∈ ((𝐹 ∘ 𝐺) “ {𝑋})) | |
8 | dffv3 6659 | . 2 ⊢ (𝐹‘(𝐺‘𝑋)) = (℩𝑥𝑥 ∈ (𝐹 “ {(𝐺‘𝑋)})) | |
9 | 6, 7, 8 | 3eqtr4g 2879 | 1 ⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → ((𝐹 ∘ 𝐺)‘𝑋) = (𝐹‘(𝐺‘𝑋))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 = wceq 1531 ∈ wcel 2108 {csn 4559 “ cima 5551 ∘ ccom 5552 ℩cio 6305 Fn wfn 6343 ‘cfv 6348 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1905 ax-6 1964 ax-7 2009 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2154 ax-12 2170 ax-ext 2791 ax-sep 5194 ax-nul 5201 ax-pow 5257 ax-pr 5320 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1084 df-tru 1534 df-ex 1775 df-nf 1779 df-sb 2064 df-mo 2616 df-eu 2648 df-clab 2798 df-cleq 2812 df-clel 2891 df-nfc 2961 df-ne 3015 df-ral 3141 df-rex 3142 df-rab 3145 df-v 3495 df-sbc 3771 df-dif 3937 df-un 3939 df-in 3941 df-ss 3950 df-nul 4290 df-if 4466 df-sn 4560 df-pr 4562 df-op 4566 df-uni 4831 df-br 5058 df-opab 5120 df-id 5453 df-xp 5554 df-rel 5555 df-cnv 5556 df-co 5557 df-dm 5558 df-rn 5559 df-res 5560 df-ima 5561 df-iota 6307 df-fun 6350 df-fn 6351 df-fv 6356 |
This theorem is referenced by: fvco 6752 fvco3 6753 fvco4i 6755 fvcofneq 6852 ofco 7421 curry1 7791 curry2 7794 fsplitfpar 7806 enfixsn 8618 updjudhcoinlf 9353 updjudhcoinrg 9354 updjud 9355 smobeth 10000 fpwwe 10060 addpqnq 10352 mulpqnq 10355 revco 14188 ccatco 14189 cshco 14190 swrdco 14191 isoval 17027 prdsidlem 17935 gsumwmhm 18002 prdsinvlem 18200 gsmsymgrfixlem1 18547 f1omvdconj 18566 pmtrfinv 18581 symggen 18590 symgtrinv 18592 pmtr3ncomlem1 18593 ringidval 19245 prdsmgp 19352 lmhmco 19807 evlslem1 20287 evlsvar 20295 chrrhm 20670 cofipsgn 20729 dsmmbas2 20873 dsmm0cl 20876 frlmbas 20891 frlmup3 20936 frlmup4 20937 f1lindf 20958 lindfmm 20963 m1detdiag 21198 1stccnp 22062 prdstopn 22228 xpstopnlem2 22411 uniioombllem6 24181 ex-fpar 28233 0vfval 28375 cnre2csqlem 31146 mblfinlem2 34922 rabren3dioph 39403 hausgraph 39803 stoweidlem59 42335 afvco2 43366 isomushgr 43982 isomgrtrlem 43994 |
Copyright terms: Public domain | W3C validator |