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

Metamath Proof Explorer

Theorem cofid1a

Description: Express the object part of ( G o.func F ) = I explicitly. (Contributed by Zhi Wang, 15-Nov-2025)

Ref Expression
Hypotheses cofid1a.i ⊢ I = id func ⁡ D
cofid1a.b ⊢ B = Base D
cofid1a.x ⊢ φ → X ∈ B
cofid1a.f ⊢ φ → F ∈ D Func E
cofid1a.g ⊢ φ → G ∈ E Func D
cofid1a.o ⊢ φ → G ∘ func F = I
Assertion cofid1a ⊢ φ → 1 st ⁡ G ⁡ 1 st ⁡ F ⁡ X = X

Proof

Step Hyp Ref Expression
1 cofid1a.i ⊢ I = id func ⁡ D
2 cofid1a.b ⊢ B = Base D
3 cofid1a.x ⊢ φ → X ∈ B
4 cofid1a.f ⊢ φ → F ∈ D Func E
5 cofid1a.g ⊢ φ → G ∈ E Func D
6 cofid1a.o ⊢ φ → G ∘ func F = I
7 6 fveq2d ⊢ φ → 1 st ⁡ G ∘ func F = 1 st ⁡ I
8 7 fveq1d ⊢ φ → 1 st ⁡ G ∘ func F ⁡ X = 1 st ⁡ I ⁡ X
9 2 4 5 3 cofu1 ⊢ φ → 1 st ⁡ G ∘ func F ⁡ X = 1 st ⁡ G ⁡ 1 st ⁡ F ⁡ X
10 4 func1st2nd ⊢ φ → 1 st ⁡ F D Func E 2 nd ⁡ F
11 10 funcrcl2 ⊢ φ → D ∈ Cat
12 1 2 11 3 idfu1 ⊢ φ → 1 st ⁡ I ⁡ X = X
13 8 9 12 3eqtr3d ⊢ φ → 1 st ⁡ G ⁡ 1 st ⁡ F ⁡ X = X