Theorem prcofvala

Description: Value of the pre-composition functor. (Contributed by Zhi Wang, 2-Nov-2025)

	Ref	Expression
Hypotheses	prcofvalg.b	⊢ 𝐵 = ( 𝐷 Func 𝐸 )
	prcofvalg.n	⊢ 𝑁 = ( 𝐷 Nat 𝐸 )
	prcofvala.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
	prcofvala.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑊 )
	prcofvala.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑈 )
Assertion	prcofvala	⊢ ( 𝜑 → ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) = ⟨ ( 𝑘 ∈ 𝐵 ↦ ( 𝑘 ∘func 𝐹 ) ) , ( 𝑘 ∈ 𝐵 , 𝑙 ∈ 𝐵 ↦ ( 𝑎 ∈ ( 𝑘 𝑁 𝑙 ) ↦ ( 𝑎 ∘ ( 1st ‘ 𝐹 ) ) ) ) ⟩ )

Proof

Step	Hyp	Ref	Expression
1		prcofvalg.b	⊢ 𝐵 = ( 𝐷 Func 𝐸 )
2		prcofvalg.n	⊢ 𝑁 = ( 𝐷 Nat 𝐸 )
3		prcofvala.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
4		prcofvala.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑊 )
5		prcofvala.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑈 )
6		opex	⊢ ⟨ 𝐷 , 𝐸 ⟩ ∈ V
7	6	a1i	⊢ ( 𝜑 → ⟨ 𝐷 , 𝐸 ⟩ ∈ V )
8		op1stg	⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( 1st ‘ ⟨ 𝐷 , 𝐸 ⟩ ) = 𝐷 )
9	3 4 8	syl2anc	⊢ ( 𝜑 → ( 1st ‘ ⟨ 𝐷 , 𝐸 ⟩ ) = 𝐷 )
10		op2ndg	⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( 2nd ‘ ⟨ 𝐷 , 𝐸 ⟩ ) = 𝐸 )
11	3 4 10	syl2anc	⊢ ( 𝜑 → ( 2nd ‘ ⟨ 𝐷 , 𝐸 ⟩ ) = 𝐸 )
12	1 2 5 7 9 11	prcofvalg	⊢ ( 𝜑 → ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) = ⟨ ( 𝑘 ∈ 𝐵 ↦ ( 𝑘 ∘func 𝐹 ) ) , ( 𝑘 ∈ 𝐵 , 𝑙 ∈ 𝐵 ↦ ( 𝑎 ∈ ( 𝑘 𝑁 𝑙 ) ↦ ( 𝑎 ∘ ( 1st ‘ 𝐹 ) ) ) ) ⟩ )