Metamath Proof Explorer

Theorem fuco2

Description: The morphism 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 fuco2 ⊢ φ → P = 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

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 opthg ⊢ 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 ∧ P = 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
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 ∧ P = 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
14 6 13 mpbid ⊢ φ → O = ∘ func ↾ W ∧ P = 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
15 14 simprd ⊢ φ → P = 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