Theorem cofu1

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

	Ref	Expression
Hypotheses	cofuval.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	cofuval.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
	cofuval.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐷 Func 𝐸 ) )
	cofu2nd.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
Assertion	cofu1	⊢ ( 𝜑 → ( ( 1st ‘ ( 𝐺 ∘func 𝐹 ) ) ‘ 𝑋 ) = ( ( 1st ‘ 𝐺 ) ‘ ( ( 1st ‘ 𝐹 ) ‘ 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		cofuval.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
2		cofuval.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
3		cofuval.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐷 Func 𝐸 ) )
4		cofu2nd.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5	1 2 3	cofu1st	⊢ ( 𝜑 → ( 1st ‘ ( 𝐺 ∘func 𝐹 ) ) = ( ( 1st ‘ 𝐺 ) ∘ ( 1st ‘ 𝐹 ) ) )
6	5	fveq1d	⊢ ( 𝜑 → ( ( 1st ‘ ( 𝐺 ∘func 𝐹 ) ) ‘ 𝑋 ) = ( ( ( 1st ‘ 𝐺 ) ∘ ( 1st ‘ 𝐹 ) ) ‘ 𝑋 ) )
7		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
8		relfunc	⊢ Rel ( 𝐶 Func 𝐷 )
9		1st2ndbr	⊢ ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝐹 ∈ ( 𝐶 Func 𝐷 ) ) → ( 1st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2nd ‘ 𝐹 ) )
10	8 2 9	sylancr	⊢ ( 𝜑 → ( 1st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2nd ‘ 𝐹 ) )
11	1 7 10	funcf1	⊢ ( 𝜑 → ( 1st ‘ 𝐹 ) : 𝐵 ⟶ ( Base ‘ 𝐷 ) )
12		fvco3	⊢ ( ( ( 1st ‘ 𝐹 ) : 𝐵 ⟶ ( Base ‘ 𝐷 ) ∧ 𝑋 ∈ 𝐵 ) → ( ( ( 1st ‘ 𝐺 ) ∘ ( 1st ‘ 𝐹 ) ) ‘ 𝑋 ) = ( ( 1st ‘ 𝐺 ) ‘ ( ( 1st ‘ 𝐹 ) ‘ 𝑋 ) ) )
13	11 4 12	syl2anc	⊢ ( 𝜑 → ( ( ( 1st ‘ 𝐺 ) ∘ ( 1st ‘ 𝐹 ) ) ‘ 𝑋 ) = ( ( 1st ‘ 𝐺 ) ‘ ( ( 1st ‘ 𝐹 ) ‘ 𝑋 ) ) )
14	6 13	eqtrd	⊢ ( 𝜑 → ( ( 1st ‘ ( 𝐺 ∘func 𝐹 ) ) ‘ 𝑋 ) = ( ( 1st ‘ 𝐺 ) ‘ ( ( 1st ‘ 𝐹 ) ‘ 𝑋 ) ) )