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

Metamath Proof Explorer

Theorem cofid1

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

Ref Expression
Hypotheses cofid1a.i ⊢ 𝐼 = ( idfunc ‘ 𝐷 )
cofid1a.b ⊢ 𝐵 = ( Base ‘ 𝐷 )
cofid1a.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
cofid1.f ⊢ ( 𝜑 → 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 )
cofid1.k ⊢ ( 𝜑 → 𝐾 ( 𝐸 Func 𝐷 ) 𝐿 )
cofid1.o ⊢ ( 𝜑 → ( ⟨ 𝐾 , 𝐿 ⟩ ∘func ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐼 )
Assertion cofid1 ( 𝜑 → ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) = 𝑋 )

Proof

Step Hyp Ref Expression
1 cofid1a.i ⊢ 𝐼 = ( idfunc ‘ 𝐷 )
2 cofid1a.b ⊢ 𝐵 = ( Base ‘ 𝐷 )
3 cofid1a.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
4 cofid1.f ⊢ ( 𝜑 → 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 )
5 cofid1.k ⊢ ( 𝜑 → 𝐾 ( 𝐸 Func 𝐷 ) 𝐿 )
6 cofid1.o ⊢ ( 𝜑 → ( ⟨ 𝐾 , 𝐿 ⟩ ∘func ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐼 )
7 5 func1st ⊢ ( 𝜑 → ( 1st ‘ ⟨ 𝐾 , 𝐿 ⟩ ) = 𝐾 )
8 4 func1st ⊢ ( 𝜑 → ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐹 )
9 8 fveq1d ⊢ ( 𝜑 → ( ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑋 ) = ( 𝐹 ‘ 𝑋 ) )
10 7 9 fveq12d ⊢ ( 𝜑 → ( ( 1st ‘ ⟨ 𝐾 , 𝐿 ⟩ ) ‘ ( ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑋 ) ) = ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) )
11 df-br ⊢ ( 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 ↔ ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐷 Func 𝐸 ) )
12 4 11 sylib ⊢ ( 𝜑 → ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐷 Func 𝐸 ) )
13 df-br ⊢ ( 𝐾 ( 𝐸 Func 𝐷 ) 𝐿 ↔ ⟨ 𝐾 , 𝐿 ⟩ ∈ ( 𝐸 Func 𝐷 ) )
14 5 13 sylib ⊢ ( 𝜑 → ⟨ 𝐾 , 𝐿 ⟩ ∈ ( 𝐸 Func 𝐷 ) )
15 1 2 3 12 14 6 cofid1a ⊢ ( 𝜑 → ( ( 1st ‘ ⟨ 𝐾 , 𝐿 ⟩ ) ‘ ( ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑋 ) ) = 𝑋 )
16 10 15 eqtr3d ⊢ ( 𝜑 → ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) = 𝑋 )