cofu1st

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

Step	Hyp	Ref	Expression
1		cofuval.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
2		cofuval.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
3		cofuval.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐷 Func 𝐸 ) )
4	1 2 3	cofuval	⊢ ( 𝜑 → ( 𝐺 ∘_func 𝐹 ) = ⟨ ( ( 1^st ‘ 𝐺 ) ∘ ( 1^st ‘ 𝐹 ) ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ) ) ⟩ )
5	4	fveq2d	⊢ ( 𝜑 → ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) = ( 1^st ‘ ⟨ ( ( 1^st ‘ 𝐺 ) ∘ ( 1^st ‘ 𝐹 ) ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ) ) ⟩ ) )
6		fvex	⊢ ( 1^st ‘ 𝐺 ) ∈ V
7		fvex	⊢ ( 1^st ‘ 𝐹 ) ∈ V
8	6 7	coex	⊢ ( ( 1^st ‘ 𝐺 ) ∘ ( 1^st ‘ 𝐹 ) ) ∈ V
9	1	fvexi	⊢ 𝐵 ∈ V
10	9 9	mpoex	⊢ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ) ) ∈ V
11	8 10	op1st	⊢ ( 1^st ‘ ⟨ ( ( 1^st ‘ 𝐺 ) ∘ ( 1^st ‘ 𝐹 ) ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ) ) ⟩ ) = ( ( 1^st ‘ 𝐺 ) ∘ ( 1^st ‘ 𝐹 ) )
12	5 11	eqtrdi	⊢ ( 𝜑 → ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) = ( ( 1^st ‘ 𝐺 ) ∘ ( 1^st ‘ 𝐹 ) ) )

Metamath Proof Explorer