fvco2 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > fvco2		Structured version Visualization version GIF version

Theorem fvco2 6998

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.)

**Assertion**
Ref	Expression
fvco2	⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → ((𝐹 ∘ 𝐺)‘𝑋) = (𝐹‘(𝐺‘𝑋)))

Proof of Theorem fvco2 Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		imaco 6258	. . . . 5 ⊢ ((𝐹 ∘ 𝐺) “ {𝑋}) = (𝐹 “ (𝐺 “ {𝑋}))
2		fnsnfv 6980	. . . . . 6 ⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → {(𝐺‘𝑋)} = (𝐺 “ {𝑋}))
3	2	imaeq2d 6066	. . . . 5 ⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝐹 “ {(𝐺‘𝑋)}) = (𝐹 “ (𝐺 “ {𝑋})))
4	1, 3	eqtr4id 2786	. . . 4 ⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → ((𝐹 ∘ 𝐺) “ {𝑋}) = (𝐹 “ {(𝐺‘𝑋)}))
5	4	eleq2d 2814	. . 3 ⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝑥 ∈ ((𝐹 ∘ 𝐺) “ {𝑋}) ↔ 𝑥 ∈ (𝐹 “ {(𝐺‘𝑋)})))
6	5	iotabidv 6535	. 2 ⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → (℩𝑥𝑥 ∈ ((𝐹 ∘ 𝐺) “ {𝑋})) = (℩𝑥𝑥 ∈ (𝐹 “ {(𝐺‘𝑋)})))
7		dffv3 6896	. 2 ⊢ ((𝐹 ∘ 𝐺)‘𝑋) = (℩𝑥𝑥 ∈ ((𝐹 ∘ 𝐺) “ {𝑋}))
8		dffv3 6896	. 2 ⊢ (𝐹‘(𝐺‘𝑋)) = (℩𝑥𝑥 ∈ (𝐹 “ {(𝐺‘𝑋)}))
9	6, 7, 8	3eqtr4g 2792	1 ⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → ((𝐹 ∘ 𝐺)‘𝑋) = (𝐹‘(𝐺‘𝑋)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 394 = wceq 1533 ∈ wcel 2098 {csn 4630 “ cima 5683 ∘ ccom 5684 ℩cio 6501 Fn wfn 6546 ‘cfv 6551

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2166 ax-ext 2698 ax-sep 5301 ax-nul 5308 ax-pr 5431

This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2529 df-eu 2558 df-clab 2705 df-cleq 2719 df-clel 2805 df-ne 2937 df-ral 3058 df-rex 3067 df-rab 3429 df-v 3473 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4325 df-if 4531 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4911 df-br 5151 df-opab 5213 df-id 5578 df-xp 5686 df-rel 5687 df-cnv 5688 df-co 5689 df-dm 5690 df-rn 5691 df-res 5692 df-ima 5693 df-iota 6503 df-fun 6553 df-fn 6554 df-fv 6559

This theorem is referenced by: fvco 6999 fvco3 7000 fvco4i 7002 fvcofneq 7106 ofco 7712 curry1 8113 curry2 8116 fsplitfpar 8127 enfixsn 9110 updjudhcoinlf 9961 updjudhcoinrg 9962 updjud 9963 smobeth 10615 fpwwe 10675 addpqnq 10967 mulpqnq 10970 revco 14823 ccatco 14824 cshco 14825 swrdco 14826 isoval 17753 prdsidlem 18731 gsumwmhm 18802 prdsinvlem 19010 ghmquskerco 19240 gsmsymgrfixlem1 19387 f1omvdconj 19406 pmtrfinv 19421 symggen 19430 symgtrinv 19432 pmtr3ncomlem1 19433 prdsmgp 20096 ringidval 20128 lmhmco 20933 chrrhm 21466 cofipsgn 21530 dsmmbas2 21676 dsmm0cl 21679 frlmbas 21694 frlmup3 21739 frlmup4 21740 f1lindf 21761 lindfmm 21766 evlslem1 22033 evlsvar 22041 m1detdiag 22517 1stccnp 23384 prdstopn 23550 xpstopnlem2 23733 uniioombllem6 25535 precsexlem1 28123 precsexlem2 28124 precsexlem3 28125 precsexlem4 28126 precsexlem5 28127 ex-fpar 30290 0vfval 30434 cnre2csqlem 33516 mblfinlem2 37136 rabren3dioph 42238 hausgraph 42636 stoweidlem59 45449 afvco2 46558 gricushgr 47234 ackvalsucsucval 47812

W3C validator

	
		OSZAR »