Metamath Proof Explorer

Theorem fucofn2

Description: The morphism part of the functor composition bifunctor is a function on the Cartesian square of the base set. (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 fucofn2 ⊢ φ → P Fn W × 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 eqid ⊢ 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 = 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 ovex ⊢ 1 st ⁡ u D Nat E 1 st ⁡ v ∈ V
8 ovex ⊢ 2 nd ⁡ u C Nat D 2 nd ⁡ v ∈ V
9 7 8 mpoex ⊢ 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 ∈ V
10 9 csbex ⊢ ⦋ 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 ∈ V
11 10 csbex ⊢ ⦋ 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 ∈ V
12 11 csbex ⊢ ⦋ 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 ∈ V
13 12 csbex ⊢ ⦋ 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 ∈ V
14 13 csbex ⊢ ⦋ 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 ∈ V
15 6 14 fnmpoi ⊢ 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 Fn W × W
16 1 2 3 4 5 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
17 16 fneq1d ⊢ φ → P Fn W × 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 Fn W × W
18 15 17 mpbiri ⊢ φ → P Fn W × W