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 17965

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 17964	. . 3 ⊢ (𝜑 → (1^st ‘(𝐺 ∘_func 𝐹)) = ((1^st ‘𝐺) ∘ (1^st ‘𝐹)))
5	4	fveq1d 6887	. 2 ⊢ (𝜑 → ((1^st ‘(𝐺 ∘_func 𝐹))‘𝑋) = (((1^st ‘𝐺) ∘ (1^st ‘𝐹))‘𝑋))
6		eqid 2765	. . . 4 ⊢ (Base‘𝐷) = (Base‘𝐷)
7		relfunc 17943	. . . . 5 ⊢ Rel (𝐶 Func 𝐷)
8		1st2ndbr 8045	. . . . 5 ⊢ ((Rel (𝐶 Func 𝐷) ∧ 𝐹 ∈ (𝐶 Func 𝐷)) → (1^st ‘𝐹)(𝐶 Func 𝐷)(2^nd ‘𝐹))
9	7, 2, 8	sylancr 599	. . . 4 ⊢ (𝜑 → (1^st ‘𝐹)(𝐶 Func 𝐷)(2^nd ‘𝐹))
10	1, 6, 9	funcf1 17947	. . 3 ⊢ (𝜑 → (1^st ‘𝐹):𝐵⟶(Base‘𝐷))
11		cofu2nd.x	. . 3 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
12		fvco3 6985	. . 3 ⊢ (((1^st ‘𝐹):𝐵⟶(Base‘𝐷) ∧ 𝑋 ∈ 𝐵) → (((1^st ‘𝐺) ∘ (1^st ‘𝐹))‘𝑋) = ((1^st ‘𝐺)‘((1^st ‘𝐹)‘𝑋)))
13	10, 11, 12	syl2anc 596	. 2 ⊢ (𝜑 → (((1^st ‘𝐺) ∘ (1^st ‘𝐹))‘𝑋) = ((1^st ‘𝐺)‘((1^st ‘𝐹)‘𝑋)))
14	5, 13	eqtrd 2800	1 ⊢ (𝜑 → ((1^st ‘(𝐺 ∘_func 𝐹))‘𝑋) = ((1^st ‘𝐺)‘((1^st ‘𝐹)‘𝑋)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 = wceq 1570 ∈ wcel 2146 class class class wbr 5111 ∘ ccom 5667 Rel wrel 5668 ⟶wf 6536 ‘cfv 6540 (class class class)co 7419 1^st c1st 7990 2^nd c2nd 7991 Basecbs 17293 Func cfunc 17935 ∘_func ccofu 17937

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2737 ax-rep 5240 ax-sep 5259 ax-nul 5271 ax-pow 5338 ax-pr 5406 ax-un 7742

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-ral 3082 df-rex 3092 df-reu 3372 df-rab 3419 df-v 3459 df-sbc 3747 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-nul 4287 df-if 4490 df-pw 4566 df-sn 4592 df-pr 4594 df-op 4598 df-uni 4875 df-iun 4960 df-br 5112 df-opab 5176 df-mpt 5195 df-id 5558 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-iota 6496 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-ov 7422 df-oprab 7423 df-mpo 7424 df-1st 7992 df-2nd 7993 df-map 8832 df-ixp 8902 df-func 17939 df-cofu 17941

This theorem is used by: cofucl 17969 cofuass 17970 cofull 18017 cofth 18018 catciso 18192 1st2ndprf 18286 uncf1 18316 uncf2 18317 yonedalem21 18353 yonedalem22 18358 cofu1a 49931 cofid1a 49949 uptrar 50053 cofuswapf1 50131 prcofdiag1 50230 prcofdiag 50231 oppfdiag1 50251 oppfdiag 50253

W3C validator