Metamath Proof Explorer

Theorem precoffunc

Description: The pre-composition functor, expressed explicitly, is a functor. (Contributed by Zhi Wang, 11-Oct-2025)

Ref Expression
Hypotheses precoffunc.r ⊢ 𝑅 = ( 𝐷 FuncCat 𝐸 )
precoffunc.s ⊢ 𝑆 = ( 𝐶 FuncCat 𝐸 )
precoffunc.b ⊢ 𝐵 = ( 𝐷 Func 𝐸 )
precoffunc.n ⊢ 𝑁 = ( 𝐷 Nat 𝐸 )
precoffunc.f ⊢ ( 𝜑 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
precoffunc.e ⊢ ( 𝜑 → 𝐸 ∈ Cat )
precoffunc.k ⊢ ( 𝜑 → 𝐾 = ( 𝑔 ∈ 𝐵 ↦ ( 𝑔 ∘func ⟨ 𝐹 , 𝐺 ⟩ ) ) )
precoffunc.l ⊢ ( 𝜑 → 𝐿 = ( 𝑔 ∈ 𝐵 , ℎ ∈ 𝐵 ↦ ( 𝑎 ∈ ( 𝑔 𝑁 ℎ ) ↦ ( 𝑎 ∘ 𝐹 ) ) ) )
Assertion precoffunc ( 𝜑 → 𝐾 ( 𝑅 Func 𝑆 ) 𝐿 )

Proof

Step Hyp Ref Expression
1 precoffunc.r ⊢ 𝑅 = ( 𝐷 FuncCat 𝐸 )
2 precoffunc.s ⊢ 𝑆 = ( 𝐶 FuncCat 𝐸 )
3 precoffunc.b ⊢ 𝐵 = ( 𝐷 Func 𝐸 )
4 precoffunc.n ⊢ 𝑁 = ( 𝐷 Nat 𝐸 )
5 precoffunc.f ⊢ ( 𝜑 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
6 precoffunc.e ⊢ ( 𝜑 → 𝐸 ∈ Cat )
7 precoffunc.k ⊢ ( 𝜑 → 𝐾 = ( 𝑔 ∈ 𝐵 ↦ ( 𝑔 ∘func ⟨ 𝐹 , 𝐺 ⟩ ) ) )
8 precoffunc.l ⊢ ( 𝜑 → 𝐿 = ( 𝑔 ∈ 𝐵 , ℎ ∈ 𝐵 ↦ ( 𝑎 ∈ ( 𝑔 𝑁 ℎ ) ↦ ( 𝑎 ∘ 𝐹 ) ) ) )
9 eqid ⊢ ( 𝐶 FuncCat 𝐷 ) = ( 𝐶 FuncCat 𝐷 )
10 eqidd ⊢ ( 𝜑 → ( ⟨ ( 𝐶 FuncCat 𝐷 ) , 𝑅 ⟩ curryF ( ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) ∘func ( ( 𝐶 FuncCat 𝐷 ) swapF 𝑅 ) ) ) = ( ⟨ ( 𝐶 FuncCat 𝐷 ) , 𝑅 ⟩ curryF ( ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) ∘func ( ( 𝐶 FuncCat 𝐷 ) swapF 𝑅 ) ) ) )
11 df-br ⊢ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ↔ ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐶 Func 𝐷 ) )
12 5 11 sylib ⊢ ( 𝜑 → ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐶 Func 𝐷 ) )
13 3 mpteq1i ⊢ ( 𝑔 ∈ 𝐵 ↦ ( 𝑔 ∘func ⟨ 𝐹 , 𝐺 ⟩ ) ) = ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) ↦ ( 𝑔 ∘func ⟨ 𝐹 , 𝐺 ⟩ ) )
14 7 13 eqtrdi ⊢ ( 𝜑 → 𝐾 = ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) ↦ ( 𝑔 ∘func ⟨ 𝐹 , 𝐺 ⟩ ) ) )
15 3 a1i ⊢ ( 𝜑 → 𝐵 = ( 𝐷 Func 𝐸 ) )
16 4 a1i ⊢ ( 𝜑 → 𝑁 = ( 𝐷 Nat 𝐸 ) )
17 16 oveqd ⊢ ( 𝜑 → ( 𝑔 𝑁 ℎ ) = ( 𝑔 ( 𝐷 Nat 𝐸 ) ℎ ) )
18 relfunc ⊢ Rel ( 𝐶 Func 𝐷 )
19 brrelex12 ⊢ ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ) → ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) )
20 18 5 19 sylancr ⊢ ( 𝜑 → ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) )
21 op1stg ⊢ ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) → ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐹 )
22 20 21 syl ⊢ ( 𝜑 → ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐹 )
23 22 eqcomd ⊢ ( 𝜑 → 𝐹 = ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) )
24 23 coeq2d ⊢ ( 𝜑 → ( 𝑎 ∘ 𝐹 ) = ( 𝑎 ∘ ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ) )
25 17 24 mpteq12dv ⊢ ( 𝜑 → ( 𝑎 ∈ ( 𝑔 𝑁 ℎ ) ↦ ( 𝑎 ∘ 𝐹 ) ) = ( 𝑎 ∈ ( 𝑔 ( 𝐷 Nat 𝐸 ) ℎ ) ↦ ( 𝑎 ∘ ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ) ) )
26 15 15 25 mpoeq123dv ⊢ ( 𝜑 → ( 𝑔 ∈ 𝐵 , ℎ ∈ 𝐵 ↦ ( 𝑎 ∈ ( 𝑔 𝑁 ℎ ) ↦ ( 𝑎 ∘ 𝐹 ) ) ) = ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) , ℎ ∈ ( 𝐷 Func 𝐸 ) ↦ ( 𝑎 ∈ ( 𝑔 ( 𝐷 Nat 𝐸 ) ℎ ) ↦ ( 𝑎 ∘ ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ) ) ) )
27 8 26 eqtrd ⊢ ( 𝜑 → 𝐿 = ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) , ℎ ∈ ( 𝐷 Func 𝐸 ) ↦ ( 𝑎 ∈ ( 𝑔 ( 𝐷 Nat 𝐸 ) ℎ ) ↦ ( 𝑎 ∘ ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ) ) ) )
28 14 27 opeq12d ⊢ ( 𝜑 → ⟨ 𝐾 , 𝐿 ⟩ = ⟨ ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) ↦ ( 𝑔 ∘func ⟨ 𝐹 , 𝐺 ⟩ ) ) , ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) , ℎ ∈ ( 𝐷 Func 𝐸 ) ↦ ( 𝑎 ∈ ( 𝑔 ( 𝐷 Nat 𝐸 ) ℎ ) ↦ ( 𝑎 ∘ ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ) ) ) ⟩ )
29 eqidd ⊢ ( 𝜑 → ( ( 1st ‘ ( ⟨ ( 𝐶 FuncCat 𝐷 ) , 𝑅 ⟩ curryF ( ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) ∘func ( ( 𝐶 FuncCat 𝐷 ) swapF 𝑅 ) ) ) ) ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = ( ( 1st ‘ ( ⟨ ( 𝐶 FuncCat 𝐷 ) , 𝑅 ⟩ curryF ( ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) ∘func ( ( 𝐶 FuncCat 𝐷 ) swapF 𝑅 ) ) ) ) ‘ ⟨ 𝐹 , 𝐺 ⟩ ) )
30 9 1 10 12 6 29 precofval2 ⊢ ( 𝜑 → ( ( 1st ‘ ( ⟨ ( 𝐶 FuncCat 𝐷 ) , 𝑅 ⟩ curryF ( ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) ∘func ( ( 𝐶 FuncCat 𝐷 ) swapF 𝑅 ) ) ) ) ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = ⟨ ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) ↦ ( 𝑔 ∘func ⟨ 𝐹 , 𝐺 ⟩ ) ) , ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) , ℎ ∈ ( 𝐷 Func 𝐸 ) ↦ ( 𝑎 ∈ ( 𝑔 ( 𝐷 Nat 𝐸 ) ℎ ) ↦ ( 𝑎 ∘ ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ) ) ) ⟩ )
31 28 30 eqtr4d ⊢ ( 𝜑 → ⟨ 𝐾 , 𝐿 ⟩ = ( ( 1st ‘ ( ⟨ ( 𝐶 FuncCat 𝐷 ) , 𝑅 ⟩ curryF ( ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) ∘func ( ( 𝐶 FuncCat 𝐷 ) swapF 𝑅 ) ) ) ) ‘ ⟨ 𝐹 , 𝐺 ⟩ ) )
32 9 1 10 12 6 31 2 precofcl ⊢ ( 𝜑 → ⟨ 𝐾 , 𝐿 ⟩ ∈ ( 𝑅 Func 𝑆 ) )
33 df-br ⊢ ( 𝐾 ( 𝑅 Func 𝑆 ) 𝐿 ↔ ⟨ 𝐾 , 𝐿 ⟩ ∈ ( 𝑅 Func 𝑆 ) )
34 32 33 sylibr ⊢ ( 𝜑 → 𝐾 ( 𝑅 Func 𝑆 ) 𝐿 )