Theorem prcof22a

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

	Ref	Expression
Hypotheses	prcof21a.n	⊢ 𝑁 = ( 𝐷 Nat 𝐸 )
	prcof21a.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐾 𝑁 𝐿 ) )
	prcof21a.p	⊢ ( 𝜑 → ( 2nd ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) = 𝑃 )
	prcof22a.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	prcof22a.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	prcof22a.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
Assertion	prcof22a	⊢ ( 𝜑 → ( ( ( 𝐾 𝑃 𝐿 ) ‘ 𝐴 ) ‘ 𝑋 ) = ( 𝐴 ‘ ( ( 1st ‘ 𝐹 ) ‘ 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		prcof21a.n	⊢ 𝑁 = ( 𝐷 Nat 𝐸 )
2		prcof21a.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐾 𝑁 𝐿 ) )
3		prcof21a.p	⊢ ( 𝜑 → ( 2nd ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) = 𝑃 )
4		prcof22a.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
5		prcof22a.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6		prcof22a.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
7	1 2 3 6	prcof21a	⊢ ( 𝜑 → ( ( 𝐾 𝑃 𝐿 ) ‘ 𝐴 ) = ( 𝐴 ∘ ( 1st ‘ 𝐹 ) ) )
8	7	fveq1d	⊢ ( 𝜑 → ( ( ( 𝐾 𝑃 𝐿 ) ‘ 𝐴 ) ‘ 𝑋 ) = ( ( 𝐴 ∘ ( 1st ‘ 𝐹 ) ) ‘ 𝑋 ) )
9		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
10	6	func1st2nd	⊢ ( 𝜑 → ( 1st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2nd ‘ 𝐹 ) )
11	4 9 10	funcf1	⊢ ( 𝜑 → ( 1st ‘ 𝐹 ) : 𝐵 ⟶ ( Base ‘ 𝐷 ) )
12	11 5	fvco3d	⊢ ( 𝜑 → ( ( 𝐴 ∘ ( 1st ‘ 𝐹 ) ) ‘ 𝑋 ) = ( 𝐴 ‘ ( ( 1st ‘ 𝐹 ) ‘ 𝑋 ) ) )
13	8 12	eqtrd	⊢ ( 𝜑 → ( ( ( 𝐾 𝑃 𝐿 ) ‘ 𝐴 ) ‘ 𝑋 ) = ( 𝐴 ‘ ( ( 1st ‘ 𝐹 ) ‘ 𝑋 ) ) )