cofu1 - Metamath Proof Explorer

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

Theorem cofu1 17808

Description: Value of the object part of the functor composition. (Contributed by Mario Carneiro, 28-Jan-2017.)

**Hypotheses**
Ref	Expression
cofuval.b	⊢ 𝐵 = (Base‘𝐶)
cofuval.f	⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))
cofuval.g	⊢ (𝜑 → 𝐺 ∈ (𝐷 Func 𝐸))
cofu2nd.x	⊢ (𝜑 → 𝑋 ∈ 𝐵)

**Assertion**
Ref	Expression
cofu1	⊢ (𝜑 → ((1^st ‘(𝐺 ∘_func 𝐹))‘𝑋) = ((1^st ‘𝐺)‘((1^st ‘𝐹)‘𝑋)))

**Proof of Theorem cofu1**
Step	Hyp	Ref	Expression
1		cofuval.b	. . . 4 ⊢ 𝐵 = (Base‘𝐶)
2		cofuval.f	. . . 4 ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))
3		cofuval.g	. . . 4 ⊢ (𝜑 → 𝐺 ∈ (𝐷 Func 𝐸))
4	1, 2, 3	cofu1st 17807	. . 3 ⊢ (𝜑 → (1^st ‘(𝐺 ∘_func 𝐹)) = ((1^st ‘𝐺) ∘ (1^st ‘𝐹)))
5	4	fveq1d 6836	. 2 ⊢ (𝜑 → ((1^st ‘(𝐺 ∘_func 𝐹))‘𝑋) = (((1^st ‘𝐺) ∘ (1^st ‘𝐹))‘𝑋))
6		eqid 2736	. . . 4 ⊢ (Base‘𝐷) = (Base‘𝐷)
7		relfunc 17786	. . . . 5 ⊢ Rel (𝐶 Func 𝐷)
8		1st2ndbr 7986	. . . . 5 ⊢ ((Rel (𝐶 Func 𝐷) ∧ 𝐹 ∈ (𝐶 Func 𝐷)) → (1^st ‘𝐹)(𝐶 Func 𝐷)(2^nd ‘𝐹))
9	7, 2, 8	sylancr 587	. . . 4 ⊢ (𝜑 → (1^st ‘𝐹)(𝐶 Func 𝐷)(2^nd ‘𝐹))
10	1, 6, 9	funcf1 17790	. . 3 ⊢ (𝜑 → (1^st ‘𝐹):𝐵⟶(Base‘𝐷))
11		cofu2nd.x	. . 3 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
12		fvco3 6933	. . 3 ⊢ (((1^st ‘𝐹):𝐵⟶(Base‘𝐷) ∧ 𝑋 ∈ 𝐵) → (((1^st ‘𝐺) ∘ (1^st ‘𝐹))‘𝑋) = ((1^st ‘𝐺)‘((1^st ‘𝐹)‘𝑋)))
13	10, 11, 12	syl2anc 584	. 2 ⊢ (𝜑 → (((1^st ‘𝐺) ∘ (1^st ‘𝐹))‘𝑋) = ((1^st ‘𝐺)‘((1^st ‘𝐹)‘𝑋)))
14	5, 13	eqtrd 2771	1 ⊢ (𝜑 → ((1^st ‘(𝐺 ∘_func 𝐹))‘𝑋) = ((1^st ‘𝐺)‘((1^st ‘𝐹)‘𝑋)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 = wceq 1541 ∈ wcel 2113 class class class wbr 5098 ∘ ccom 5628 Rel wrel 5629 ⟶wf 6488 ‘cfv 6492 (class class class)co 7358 1^st c1st 7931 2^nd c2nd 7932 Basecbs 17136 Func cfunc 17778 ∘_func ccofu 17780

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 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2184 ax-ext 2708 ax-rep 5224 ax-sep 5241 ax-nul 5251 ax-pow 5310 ax-pr 5377 ax-un 7680

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-ral 3052 df-rex 3061 df-reu 3351 df-rab 3400 df-v 3442 df-sbc 3741 df-csb 3850 df-dif 3904 df-un 3906 df-in 3908 df-ss 3918 df-nul 4286 df-if 4480 df-pw 4556 df-sn 4581 df-pr 4583 df-op 4587 df-uni 4864 df-iun 4948 df-br 5099 df-opab 5161 df-mpt 5180 df-id 5519 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-rn 5635 df-res 5636 df-ima 5637 df-iota 6448 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-ov 7361 df-oprab 7362 df-mpo 7363 df-1st 7933 df-2nd 7934 df-map 8765 df-ixp 8836 df-func 17782 df-cofu 17784

This theorem is referenced by: cofucl 17812 cofuass 17813 cofull 17860 cofth 17861 catciso 18035 1st2ndprf 18129 uncf1 18159 uncf2 18160 yonedalem21 18196 yonedalem22 18201 cofu1a 49349 cofid1a 49367 uptrar 49471 cofuswapf1 49549 prcofdiag1 49648 prcofdiag 49649 oppfdiag1 49669 oppfdiag 49671

W3C validator