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

Metamath Proof Explorer

Theorem cofu1a

Description: Value of the object part of the functor composition. (Contributed by Zhi Wang, 16-Nov-2025)

Ref Expression
Hypotheses cofu1a.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
cofu1a.f ⊢ ( 𝜑 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
cofu1a.k ⊢ ( 𝜑 → 𝐾 ( 𝐷 Func 𝐸 ) 𝐿 )
cofu1a.m ⊢ ( 𝜑 → ( ⟨ 𝐾 , 𝐿 ⟩ ∘func ⟨ 𝐹 , 𝐺 ⟩ ) = ⟨ 𝑀 , 𝑁 ⟩ )
cofu1a.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
Assertion cofu1a ( 𝜑 → ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) = ( 𝑀 ‘ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 cofu1a.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
2 cofu1a.f ⊢ ( 𝜑 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
3 cofu1a.k ⊢ ( 𝜑 → 𝐾 ( 𝐷 Func 𝐸 ) 𝐿 )
4 cofu1a.m ⊢ ( 𝜑 → ( ⟨ 𝐾 , 𝐿 ⟩ ∘func ⟨ 𝐹 , 𝐺 ⟩ ) = ⟨ 𝑀 , 𝑁 ⟩ )
5 cofu1a.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6 df-br ⊢ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ↔ ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐶 Func 𝐷 ) )
7 2 6 sylib ⊢ ( 𝜑 → ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐶 Func 𝐷 ) )
8 df-br ⊢ ( 𝐾 ( 𝐷 Func 𝐸 ) 𝐿 ↔ ⟨ 𝐾 , 𝐿 ⟩ ∈ ( 𝐷 Func 𝐸 ) )
9 3 8 sylib ⊢ ( 𝜑 → ⟨ 𝐾 , 𝐿 ⟩ ∈ ( 𝐷 Func 𝐸 ) )
10 1 7 9 5 cofu1 ⊢ ( 𝜑 → ( ( 1st ‘ ( ⟨ 𝐾 , 𝐿 ⟩ ∘func ⟨ 𝐹 , 𝐺 ⟩ ) ) ‘ 𝑋 ) = ( ( 1st ‘ ⟨ 𝐾 , 𝐿 ⟩ ) ‘ ( ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑋 ) ) )
11 4 fveq2d ⊢ ( 𝜑 → ( 1st ‘ ( ⟨ 𝐾 , 𝐿 ⟩ ∘func ⟨ 𝐹 , 𝐺 ⟩ ) ) = ( 1st ‘ ⟨ 𝑀 , 𝑁 ⟩ ) )
12 7 9 cofucl ⊢ ( 𝜑 → ( ⟨ 𝐾 , 𝐿 ⟩ ∘func ⟨ 𝐹 , 𝐺 ⟩ ) ∈ ( 𝐶 Func 𝐸 ) )
13 4 12 eqeltrrd ⊢ ( 𝜑 → ⟨ 𝑀 , 𝑁 ⟩ ∈ ( 𝐶 Func 𝐸 ) )
14 df-br ⊢ ( 𝑀 ( 𝐶 Func 𝐸 ) 𝑁 ↔ ⟨ 𝑀 , 𝑁 ⟩ ∈ ( 𝐶 Func 𝐸 ) )
15 13 14 sylibr ⊢ ( 𝜑 → 𝑀 ( 𝐶 Func 𝐸 ) 𝑁 )
16 15 func1st ⊢ ( 𝜑 → ( 1st ‘ ⟨ 𝑀 , 𝑁 ⟩ ) = 𝑀 )
17 11 16 eqtrd ⊢ ( 𝜑 → ( 1st ‘ ( ⟨ 𝐾 , 𝐿 ⟩ ∘func ⟨ 𝐹 , 𝐺 ⟩ ) ) = 𝑀 )
18 17 fveq1d ⊢ ( 𝜑 → ( ( 1st ‘ ( ⟨ 𝐾 , 𝐿 ⟩ ∘func ⟨ 𝐹 , 𝐺 ⟩ ) ) ‘ 𝑋 ) = ( 𝑀 ‘ 𝑋 ) )
19 3 func1st ⊢ ( 𝜑 → ( 1st ‘ ⟨ 𝐾 , 𝐿 ⟩ ) = 𝐾 )
20 2 func1st ⊢ ( 𝜑 → ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐹 )
21 20 fveq1d ⊢ ( 𝜑 → ( ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑋 ) = ( 𝐹 ‘ 𝑋 ) )
22 19 21 fveq12d ⊢ ( 𝜑 → ( ( 1st ‘ ⟨ 𝐾 , 𝐿 ⟩ ) ‘ ( ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑋 ) ) = ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) )
23 10 18 22 3eqtr3rd ⊢ ( 𝜑 → ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) = ( 𝑀 ‘ 𝑋 ) )