This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ B = Base C
cofuval.f ⊢ φ → F ∈ C Func D
cofuval.g ⊢ φ → G ∈ D Func E
Assertion cofu1st ⊢ φ → 1 st ⁡ G ∘ func F = 1 st ⁡ G ∘ 1 st ⁡ F

Proof

Step Hyp Ref Expression
1 cofuval.b ⊢ B = Base C
2 cofuval.f ⊢ φ → F ∈ C Func D
3 cofuval.g ⊢ φ → G ∈ D Func E
4 1 2 3 cofuval ⊢ φ → G ∘ func F = 1 st ⁡ G ∘ 1 st ⁡ F x ∈ B , y ∈ B ⟼ 1 st ⁡ F ⁡ x 2 nd ⁡ G 1 st ⁡ F ⁡ y ∘ x 2 nd ⁡ F y
5 4 fveq2d ⊢ φ → 1 st ⁡ G ∘ func F = 1 st ⁡ 1 st ⁡ G ∘ 1 st ⁡ F x ∈ B , y ∈ B ⟼ 1 st ⁡ F ⁡ x 2 nd ⁡ G 1 st ⁡ F ⁡ y ∘ x 2 nd ⁡ F y
6 fvex ⊢ 1 st ⁡ G ∈ V
7 fvex ⊢ 1 st ⁡ F ∈ V
8 6 7 coex ⊢ 1 st ⁡ G ∘ 1 st ⁡ F ∈ V
9 1 fvexi ⊢ B ∈ V
10 9 9 mpoex ⊢ x ∈ B , y ∈ B ⟼ 1 st ⁡ F ⁡ x 2 nd ⁡ G 1 st ⁡ F ⁡ y ∘ x 2 nd ⁡ F y ∈ V
11 8 10 op1st ⊢ 1 st ⁡ 1 st ⁡ G ∘ 1 st ⁡ F x ∈ B , y ∈ B ⟼ 1 st ⁡ F ⁡ x 2 nd ⁡ G 1 st ⁡ F ⁡ y ∘ x 2 nd ⁡ F y = 1 st ⁡ G ∘ 1 st ⁡ F
12 5 11 eqtrdi ⊢ φ → 1 st ⁡ G ∘ func F = 1 st ⁡ G ∘ 1 st ⁡ F