Theorem prcofval

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	⊢ ( 𝜑 → 𝐸 ∈ 𝑊 )
	prcofval.r	⊢ Rel 𝑅
	prcofval.f	⊢ ( 𝜑 → 𝐹 𝑅 𝐺 )
Assertion	prcofval	⊢ ( 𝜑 → ( ⟨ 𝐷 , 𝐸 ⟩ −∘F ⟨ 𝐹 , 𝐺 ⟩ ) = ⟨ ( 𝑘 ∈ 𝐵 ↦ ( 𝑘 ∘func ⟨ 𝐹 , 𝐺 ⟩ ) ) , ( 𝑘 ∈ 𝐵 , 𝑙 ∈ 𝐵 ↦ ( 𝑎 ∈ ( 𝑘 𝑁 𝑙 ) ↦ ( 𝑎 ∘ 𝐹 ) ) ) ⟩ )

Proof

Step	Hyp	Ref	Expression
1		prcofvalg.b	⊢ 𝐵 = ( 𝐷 Func 𝐸 )
2		prcofvalg.n	⊢ 𝑁 = ( 𝐷 Nat 𝐸 )
3		prcofvala.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
4		prcofvala.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑊 )
5		prcofval.r	⊢ Rel 𝑅
6		prcofval.f	⊢ ( 𝜑 → 𝐹 𝑅 𝐺 )
7		opex	⊢ ⟨ 𝐹 , 𝐺 ⟩ ∈ V
8	7	a1i	⊢ ( 𝜑 → ⟨ 𝐹 , 𝐺 ⟩ ∈ V )
9	1 2 3 4 8	prcofvala	⊢ ( 𝜑 → ( ⟨ 𝐷 , 𝐸 ⟩ −∘F ⟨ 𝐹 , 𝐺 ⟩ ) = ⟨ ( 𝑘 ∈ 𝐵 ↦ ( 𝑘 ∘func ⟨ 𝐹 , 𝐺 ⟩ ) ) , ( 𝑘 ∈ 𝐵 , 𝑙 ∈ 𝐵 ↦ ( 𝑎 ∈ ( 𝑘 𝑁 𝑙 ) ↦ ( 𝑎 ∘ ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ) ) ) ⟩ )
10	5	brrelex12i	⊢ ( 𝐹 𝑅 𝐺 → ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) )
11		op1stg	⊢ ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) → ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐹 )
12	6 10 11	3syl	⊢ ( 𝜑 → ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐹 )
13	12	coeq2d	⊢ ( 𝜑 → ( 𝑎 ∘ ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ) = ( 𝑎 ∘ 𝐹 ) )
14	13	mpteq2dv	⊢ ( 𝜑 → ( 𝑎 ∈ ( 𝑘 𝑁 𝑙 ) ↦ ( 𝑎 ∘ ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ) ) = ( 𝑎 ∈ ( 𝑘 𝑁 𝑙 ) ↦ ( 𝑎 ∘ 𝐹 ) ) )
15	14	mpoeq3dv	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐵 , 𝑙 ∈ 𝐵 ↦ ( 𝑎 ∈ ( 𝑘 𝑁 𝑙 ) ↦ ( 𝑎 ∘ ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ) ) ) = ( 𝑘 ∈ 𝐵 , 𝑙 ∈ 𝐵 ↦ ( 𝑎 ∈ ( 𝑘 𝑁 𝑙 ) ↦ ( 𝑎 ∘ 𝐹 ) ) ) )
16	15	opeq2d	⊢ ( 𝜑 → ⟨ ( 𝑘 ∈ 𝐵 ↦ ( 𝑘 ∘func ⟨ 𝐹 , 𝐺 ⟩ ) ) , ( 𝑘 ∈ 𝐵 , 𝑙 ∈ 𝐵 ↦ ( 𝑎 ∈ ( 𝑘 𝑁 𝑙 ) ↦ ( 𝑎 ∘ ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ) ) ) ⟩ = ⟨ ( 𝑘 ∈ 𝐵 ↦ ( 𝑘 ∘func ⟨ 𝐹 , 𝐺 ⟩ ) ) , ( 𝑘 ∈ 𝐵 , 𝑙 ∈ 𝐵 ↦ ( 𝑎 ∈ ( 𝑘 𝑁 𝑙 ) ↦ ( 𝑎 ∘ 𝐹 ) ) ) ⟩ )
17	9 16	eqtrd	⊢ ( 𝜑 → ( ⟨ 𝐷 , 𝐸 ⟩ −∘F ⟨ 𝐹 , 𝐺 ⟩ ) = ⟨ ( 𝑘 ∈ 𝐵 ↦ ( 𝑘 ∘func ⟨ 𝐹 , 𝐺 ⟩ ) ) , ( 𝑘 ∈ 𝐵 , 𝑙 ∈ 𝐵 ↦ ( 𝑎 ∈ ( 𝑘 𝑁 𝑙 ) ↦ ( 𝑎 ∘ 𝐹 ) ) ) ⟩ )