Metamath Proof Explorer

Theorem prcof2

Description: The morphism part of the pre-composition functor. (Contributed by Zhi Wang, 3-Nov-2025)

Ref Expression
Hypotheses prcof2a.n ⊢ 𝑁 = ( 𝐷 Nat 𝐸 )
prcof2a.k ⊢ ( 𝜑 → 𝐾 ∈ ( 𝐷 Func 𝐸 ) )
prcof2a.l ⊢ ( 𝜑 → 𝐿 ∈ ( 𝐷 Func 𝐸 ) )
prcof2.p ⊢ ( 𝜑 → ( 2nd ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F ⟨ 𝐹 , 𝐺 ⟩ ) ) = 𝑃 )
prcof2.r ⊢ Rel 𝑅
prcof2.f ⊢ ( 𝜑 → 𝐹 𝑅 𝐺 )
Assertion prcof2 ( 𝜑 → ( 𝐾 𝑃 𝐿 ) = ( 𝑎 ∈ ( 𝐾 𝑁 𝐿 ) ↦ ( 𝑎 ∘ 𝐹 ) ) )

Proof

Step Hyp Ref Expression
1 prcof2a.n ⊢ 𝑁 = ( 𝐷 Nat 𝐸 )
2 prcof2a.k ⊢ ( 𝜑 → 𝐾 ∈ ( 𝐷 Func 𝐸 ) )
3 prcof2a.l ⊢ ( 𝜑 → 𝐿 ∈ ( 𝐷 Func 𝐸 ) )
4 prcof2.p ⊢ ( 𝜑 → ( 2nd ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F ⟨ 𝐹 , 𝐺 ⟩ ) ) = 𝑃 )
5 prcof2.r ⊢ Rel 𝑅
6 prcof2.f ⊢ ( 𝜑 → 𝐹 𝑅 𝐺 )
7 eqid ⊢ ( 𝐷 Func 𝐸 ) = ( 𝐷 Func 𝐸 )
8 2 func1st2nd ⊢ ( 𝜑 → ( 1st ‘ 𝐾 ) ( 𝐷 Func 𝐸 ) ( 2nd ‘ 𝐾 ) )
9 8 funcrcl2 ⊢ ( 𝜑 → 𝐷 ∈ Cat )
10 8 funcrcl3 ⊢ ( 𝜑 → 𝐸 ∈ Cat )
11 7 1 9 10 5 6 prcofval ⊢ ( 𝜑 → ( ⟨ 𝐷 , 𝐸 ⟩ −∘F ⟨ 𝐹 , 𝐺 ⟩ ) = ⟨ ( 𝑘 ∈ ( 𝐷 Func 𝐸 ) ↦ ( 𝑘 ∘func ⟨ 𝐹 , 𝐺 ⟩ ) ) , ( 𝑘 ∈ ( 𝐷 Func 𝐸 ) , 𝑙 ∈ ( 𝐷 Func 𝐸 ) ↦ ( 𝑎 ∈ ( 𝑘 𝑁 𝑙 ) ↦ ( 𝑎 ∘ 𝐹 ) ) ) ⟩ )
12 11 fveq2d ⊢ ( 𝜑 → ( 2nd ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F ⟨ 𝐹 , 𝐺 ⟩ ) ) = ( 2nd ‘ ⟨ ( 𝑘 ∈ ( 𝐷 Func 𝐸 ) ↦ ( 𝑘 ∘func ⟨ 𝐹 , 𝐺 ⟩ ) ) , ( 𝑘 ∈ ( 𝐷 Func 𝐸 ) , 𝑙 ∈ ( 𝐷 Func 𝐸 ) ↦ ( 𝑎 ∈ ( 𝑘 𝑁 𝑙 ) ↦ ( 𝑎 ∘ 𝐹 ) ) ) ⟩ ) )
13 ovex ⊢ ( 𝐷 Func 𝐸 ) ∈ V
14 13 mptex ⊢ ( 𝑘 ∈ ( 𝐷 Func 𝐸 ) ↦ ( 𝑘 ∘func ⟨ 𝐹 , 𝐺 ⟩ ) ) ∈ V
15 13 13 mpoex ⊢ ( 𝑘 ∈ ( 𝐷 Func 𝐸 ) , 𝑙 ∈ ( 𝐷 Func 𝐸 ) ↦ ( 𝑎 ∈ ( 𝑘 𝑁 𝑙 ) ↦ ( 𝑎 ∘ 𝐹 ) ) ) ∈ V
16 14 15 op2nd ⊢ ( 2nd ‘ ⟨ ( 𝑘 ∈ ( 𝐷 Func 𝐸 ) ↦ ( 𝑘 ∘func ⟨ 𝐹 , 𝐺 ⟩ ) ) , ( 𝑘 ∈ ( 𝐷 Func 𝐸 ) , 𝑙 ∈ ( 𝐷 Func 𝐸 ) ↦ ( 𝑎 ∈ ( 𝑘 𝑁 𝑙 ) ↦ ( 𝑎 ∘ 𝐹 ) ) ) ⟩ ) = ( 𝑘 ∈ ( 𝐷 Func 𝐸 ) , 𝑙 ∈ ( 𝐷 Func 𝐸 ) ↦ ( 𝑎 ∈ ( 𝑘 𝑁 𝑙 ) ↦ ( 𝑎 ∘ 𝐹 ) ) )
17 12 16 eqtrdi ⊢ ( 𝜑 → ( 2nd ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F ⟨ 𝐹 , 𝐺 ⟩ ) ) = ( 𝑘 ∈ ( 𝐷 Func 𝐸 ) , 𝑙 ∈ ( 𝐷 Func 𝐸 ) ↦ ( 𝑎 ∈ ( 𝑘 𝑁 𝑙 ) ↦ ( 𝑎 ∘ 𝐹 ) ) ) )
18 4 17 eqtr3d ⊢ ( 𝜑 → 𝑃 = ( 𝑘 ∈ ( 𝐷 Func 𝐸 ) , 𝑙 ∈ ( 𝐷 Func 𝐸 ) ↦ ( 𝑎 ∈ ( 𝑘 𝑁 𝑙 ) ↦ ( 𝑎 ∘ 𝐹 ) ) ) )
19 simprl ⊢ ( ( 𝜑 ∧ ( 𝑘 = 𝐾 ∧ 𝑙 = 𝐿 ) ) → 𝑘 = 𝐾 )
20 simprr ⊢ ( ( 𝜑 ∧ ( 𝑘 = 𝐾 ∧ 𝑙 = 𝐿 ) ) → 𝑙 = 𝐿 )
21 19 20 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑘 = 𝐾 ∧ 𝑙 = 𝐿 ) ) → ( 𝑘 𝑁 𝑙 ) = ( 𝐾 𝑁 𝐿 ) )
22 21 mpteq1d ⊢ ( ( 𝜑 ∧ ( 𝑘 = 𝐾 ∧ 𝑙 = 𝐿 ) ) → ( 𝑎 ∈ ( 𝑘 𝑁 𝑙 ) ↦ ( 𝑎 ∘ 𝐹 ) ) = ( 𝑎 ∈ ( 𝐾 𝑁 𝐿 ) ↦ ( 𝑎 ∘ 𝐹 ) ) )
23 ovex ⊢ ( 𝐾 𝑁 𝐿 ) ∈ V
24 23 mptex ⊢ ( 𝑎 ∈ ( 𝐾 𝑁 𝐿 ) ↦ ( 𝑎 ∘ 𝐹 ) ) ∈ V
25 24 a1i ⊢ ( 𝜑 → ( 𝑎 ∈ ( 𝐾 𝑁 𝐿 ) ↦ ( 𝑎 ∘ 𝐹 ) ) ∈ V )
26 18 22 2 3 25 ovmpod ⊢ ( 𝜑 → ( 𝐾 𝑃 𝐿 ) = ( 𝑎 ∈ ( 𝐾 𝑁 𝐿 ) ↦ ( 𝑎 ∘ 𝐹 ) ) )