Metamath Proof Explorer

Theorem fuco1

Description: The object part of the functor composition bifunctor. (Contributed by Zhi Wang, 29-Sep-2025)

Ref Expression
Hypotheses fucofval.c ⊢ φ → C ∈ T
fucofval.d ⊢ φ → D ∈ U
fucofval.e ⊢ φ → E ∈ V
fuco1.o No typesetting found for |- ( ph -> ( <. C , D >. o.F E ) = <. O , P >. ) with typecode |-
fuco1.w ⊢ φ → W = D Func E × C Func D
Assertion fuco1 ⊢ φ → O = ∘ func ↾ W

Proof

Step Hyp Ref Expression
1 fucofval.c ⊢ φ → C ∈ T
2 fucofval.d ⊢ φ → D ∈ U
3 fucofval.e ⊢ φ → E ∈ V
4 fuco1.o Could not format ( ph -> ( <. C , D >. o.F E ) = <. O , P >. ) : No typesetting found for |- ( ph -> ( <. C , D >. o.F E ) = <. O , P >. ) with typecode |-
5 fuco1.w ⊢ φ → W = D Func E × C Func D
6 1 2 3 4 5 fucofval ⊢ φ → O P = ∘ func ↾ W u ∈ W , v ∈ W ⟼ ⦋ 1 st ⁡ 2 nd ⁡ u / f⦌ ⦋ 1 st ⁡ 1 st ⁡ u / k⦌ ⦋ 2 nd ⁡ 1 st ⁡ u / l⦌ ⦋ 1 st ⁡ 2 nd ⁡ v / m⦌ ⦋ 1 st ⁡ 1 st ⁡ v / r⦌ b ∈ 1 st ⁡ u D Nat E 1 st ⁡ v , a ∈ 2 nd ⁡ u C Nat D 2 nd ⁡ v ⟼ x ∈ Base C ⟼ b ⁡ m ⁡ x k ⁡ f ⁡ x k ⁡ m ⁡ x comp ⁡ E r ⁡ m ⁡ x f ⁡ x l m ⁡ x ⁡ a ⁡ x
7 1 2 3 4 fucoelvv ⊢ φ → O P ∈ V × V
8 opelxp1 ⊢ O P ∈ V × V → O ∈ V
9 7 8 syl ⊢ φ → O ∈ V
10 opelxp2 ⊢ O P ∈ V × V → P ∈ V
11 7 10 syl ⊢ φ → P ∈ V
12 opth1g ⊢ O ∈ V ∧ P ∈ V → O P = ∘ func ↾ W u ∈ W , v ∈ W ⟼ ⦋ 1 st ⁡ 2 nd ⁡ u / f⦌ ⦋ 1 st ⁡ 1 st ⁡ u / k⦌ ⦋ 2 nd ⁡ 1 st ⁡ u / l⦌ ⦋ 1 st ⁡ 2 nd ⁡ v / m⦌ ⦋ 1 st ⁡ 1 st ⁡ v / r⦌ b ∈ 1 st ⁡ u D Nat E 1 st ⁡ v , a ∈ 2 nd ⁡ u C Nat D 2 nd ⁡ v ⟼ x ∈ Base C ⟼ b ⁡ m ⁡ x k ⁡ f ⁡ x k ⁡ m ⁡ x comp ⁡ E r ⁡ m ⁡ x f ⁡ x l m ⁡ x ⁡ a ⁡ x → O = ∘ func ↾ W
13 9 11 12 syl2anc ⊢ φ → O P = ∘ func ↾ W u ∈ W , v ∈ W ⟼ ⦋ 1 st ⁡ 2 nd ⁡ u / f⦌ ⦋ 1 st ⁡ 1 st ⁡ u / k⦌ ⦋ 2 nd ⁡ 1 st ⁡ u / l⦌ ⦋ 1 st ⁡ 2 nd ⁡ v / m⦌ ⦋ 1 st ⁡ 1 st ⁡ v / r⦌ b ∈ 1 st ⁡ u D Nat E 1 st ⁡ v , a ∈ 2 nd ⁡ u C Nat D 2 nd ⁡ v ⟼ x ∈ Base C ⟼ b ⁡ m ⁡ x k ⁡ f ⁡ x k ⁡ m ⁡ x comp ⁡ E r ⁡ m ⁡ x f ⁡ x l m ⁡ x ⁡ a ⁡ x → O = ∘ func ↾ W
14 6 13 mpd ⊢ φ → O = ∘ func ↾ W