Metamath Proof Explorer


Theorem cofu1st

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

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

Proof

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