Theorem prcofvalg

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

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

Proof

Step	Hyp	Ref	Expression
1		prcofvalg.b	⊢ 𝐵 = ( 𝐷 Func 𝐸 )
2		prcofvalg.n	⊢ 𝑁 = ( 𝐷 Nat 𝐸 )
3		prcofvalg.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑈 )
4		prcofvalg.p	⊢ ( 𝜑 → 𝑃 ∈ 𝑉 )
5		prcofvalg.d	⊢ ( 𝜑 → ( 1st ‘ 𝑃 ) = 𝐷 )
6		prcofvalg.e	⊢ ( 𝜑 → ( 2nd ‘ 𝑃 ) = 𝐸 )
7		df-prcof	⊢ −∘F = ( 𝑝 ∈ V , 𝑓 ∈ V ↦ ⦋ ( 1st ‘ 𝑝 ) / 𝑑 ⦌ ⦋ ( 2nd ‘ 𝑝 ) / 𝑒 ⦌ ⦋ ( 𝑑 Func 𝑒 ) / 𝑏 ⦌ ⟨ ( 𝑘 ∈ 𝑏 ↦ ( 𝑘 ∘func 𝑓 ) ) , ( 𝑘 ∈ 𝑏 , 𝑙 ∈ 𝑏 ↦ ( 𝑎 ∈ ( 𝑘 ( 𝑑 Nat 𝑒 ) 𝑙 ) ↦ ( 𝑎 ∘ ( 1st ‘ 𝑓 ) ) ) ) ⟩ )
8	7	a1i	⊢ ( 𝜑 → −∘F = ( 𝑝 ∈ V , 𝑓 ∈ V ↦ ⦋ ( 1st ‘ 𝑝 ) / 𝑑 ⦌ ⦋ ( 2nd ‘ 𝑝 ) / 𝑒 ⦌ ⦋ ( 𝑑 Func 𝑒 ) / 𝑏 ⦌ ⟨ ( 𝑘 ∈ 𝑏 ↦ ( 𝑘 ∘func 𝑓 ) ) , ( 𝑘 ∈ 𝑏 , 𝑙 ∈ 𝑏 ↦ ( 𝑎 ∈ ( 𝑘 ( 𝑑 Nat 𝑒 ) 𝑙 ) ↦ ( 𝑎 ∘ ( 1st ‘ 𝑓 ) ) ) ) ⟩ ) )
9		fvexd	⊢ ( ( 𝜑 ∧ ( 𝑝 = 𝑃 ∧ 𝑓 = 𝐹 ) ) → ( 1st ‘ 𝑝 ) ∈ V )
10		simprl	⊢ ( ( 𝜑 ∧ ( 𝑝 = 𝑃 ∧ 𝑓 = 𝐹 ) ) → 𝑝 = 𝑃 )
11	10	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑝 = 𝑃 ∧ 𝑓 = 𝐹 ) ) → ( 1st ‘ 𝑝 ) = ( 1st ‘ 𝑃 ) )
12	5	adantr	⊢ ( ( 𝜑 ∧ ( 𝑝 = 𝑃 ∧ 𝑓 = 𝐹 ) ) → ( 1st ‘ 𝑃 ) = 𝐷 )
13	11 12	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑝 = 𝑃 ∧ 𝑓 = 𝐹 ) ) → ( 1st ‘ 𝑝 ) = 𝐷 )
14		fvexd	⊢ ( ( ( 𝜑 ∧ ( 𝑝 = 𝑃 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑑 = 𝐷 ) → ( 2nd ‘ 𝑝 ) ∈ V )
15	10	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑝 = 𝑃 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑑 = 𝐷 ) → 𝑝 = 𝑃 )
16	15	fveq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑝 = 𝑃 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑑 = 𝐷 ) → ( 2nd ‘ 𝑝 ) = ( 2nd ‘ 𝑃 ) )
17	6	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑝 = 𝑃 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑑 = 𝐷 ) → ( 2nd ‘ 𝑃 ) = 𝐸 )
18	16 17	eqtrd	⊢ ( ( ( 𝜑 ∧ ( 𝑝 = 𝑃 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑑 = 𝐷 ) → ( 2nd ‘ 𝑝 ) = 𝐸 )
19		ovexd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 = 𝑃 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑒 = 𝐸 ) → ( 𝑑 Func 𝑒 ) ∈ V )
20		simplr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 = 𝑃 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑒 = 𝐸 ) → 𝑑 = 𝐷 )
21		simpr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 = 𝑃 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑒 = 𝐸 ) → 𝑒 = 𝐸 )
22	20 21	oveq12d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 = 𝑃 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑒 = 𝐸 ) → ( 𝑑 Func 𝑒 ) = ( 𝐷 Func 𝐸 ) )
23	22 1	eqtr4di	⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 = 𝑃 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑒 = 𝐸 ) → ( 𝑑 Func 𝑒 ) = 𝐵 )
24		simpr	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑝 = 𝑃 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) → 𝑏 = 𝐵 )
25		simp-4r	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑝 = 𝑃 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) → ( 𝑝 = 𝑃 ∧ 𝑓 = 𝐹 ) )
26	25	simprd	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑝 = 𝑃 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) → 𝑓 = 𝐹 )
27	26	oveq2d	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑝 = 𝑃 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) → ( 𝑘 ∘func 𝑓 ) = ( 𝑘 ∘func 𝐹 ) )
28	24 27	mpteq12dv	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑝 = 𝑃 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) → ( 𝑘 ∈ 𝑏 ↦ ( 𝑘 ∘func 𝑓 ) ) = ( 𝑘 ∈ 𝐵 ↦ ( 𝑘 ∘func 𝐹 ) ) )
29	20 21	oveq12d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 = 𝑃 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑒 = 𝐸 ) → ( 𝑑 Nat 𝑒 ) = ( 𝐷 Nat 𝐸 ) )
30	29 2	eqtr4di	⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 = 𝑃 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑒 = 𝐸 ) → ( 𝑑 Nat 𝑒 ) = 𝑁 )
31	30	oveqdr	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑝 = 𝑃 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) → ( 𝑘 ( 𝑑 Nat 𝑒 ) 𝑙 ) = ( 𝑘 𝑁 𝑙 ) )
32	26	fveq2d	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑝 = 𝑃 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) → ( 1st ‘ 𝑓 ) = ( 1st ‘ 𝐹 ) )
33	32	coeq2d	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑝 = 𝑃 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) → ( 𝑎 ∘ ( 1st ‘ 𝑓 ) ) = ( 𝑎 ∘ ( 1st ‘ 𝐹 ) ) )
34	31 33	mpteq12dv	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑝 = 𝑃 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) → ( 𝑎 ∈ ( 𝑘 ( 𝑑 Nat 𝑒 ) 𝑙 ) ↦ ( 𝑎 ∘ ( 1st ‘ 𝑓 ) ) ) = ( 𝑎 ∈ ( 𝑘 𝑁 𝑙 ) ↦ ( 𝑎 ∘ ( 1st ‘ 𝐹 ) ) ) )
35	24 24 34	mpoeq123dv	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑝 = 𝑃 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) → ( 𝑘 ∈ 𝑏 , 𝑙 ∈ 𝑏 ↦ ( 𝑎 ∈ ( 𝑘 ( 𝑑 Nat 𝑒 ) 𝑙 ) ↦ ( 𝑎 ∘ ( 1st ‘ 𝑓 ) ) ) ) = ( 𝑘 ∈ 𝐵 , 𝑙 ∈ 𝐵 ↦ ( 𝑎 ∈ ( 𝑘 𝑁 𝑙 ) ↦ ( 𝑎 ∘ ( 1st ‘ 𝐹 ) ) ) ) )
36	28 35	opeq12d	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑝 = 𝑃 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) → ⟨ ( 𝑘 ∈ 𝑏 ↦ ( 𝑘 ∘func 𝑓 ) ) , ( 𝑘 ∈ 𝑏 , 𝑙 ∈ 𝑏 ↦ ( 𝑎 ∈ ( 𝑘 ( 𝑑 Nat 𝑒 ) 𝑙 ) ↦ ( 𝑎 ∘ ( 1st ‘ 𝑓 ) ) ) ) ⟩ = ⟨ ( 𝑘 ∈ 𝐵 ↦ ( 𝑘 ∘func 𝐹 ) ) , ( 𝑘 ∈ 𝐵 , 𝑙 ∈ 𝐵 ↦ ( 𝑎 ∈ ( 𝑘 𝑁 𝑙 ) ↦ ( 𝑎 ∘ ( 1st ‘ 𝐹 ) ) ) ) ⟩ )
37	19 23 36	csbied2	⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 = 𝑃 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑒 = 𝐸 ) → ⦋ ( 𝑑 Func 𝑒 ) / 𝑏 ⦌ ⟨ ( 𝑘 ∈ 𝑏 ↦ ( 𝑘 ∘func 𝑓 ) ) , ( 𝑘 ∈ 𝑏 , 𝑙 ∈ 𝑏 ↦ ( 𝑎 ∈ ( 𝑘 ( 𝑑 Nat 𝑒 ) 𝑙 ) ↦ ( 𝑎 ∘ ( 1st ‘ 𝑓 ) ) ) ) ⟩ = ⟨ ( 𝑘 ∈ 𝐵 ↦ ( 𝑘 ∘func 𝐹 ) ) , ( 𝑘 ∈ 𝐵 , 𝑙 ∈ 𝐵 ↦ ( 𝑎 ∈ ( 𝑘 𝑁 𝑙 ) ↦ ( 𝑎 ∘ ( 1st ‘ 𝐹 ) ) ) ) ⟩ )
38	14 18 37	csbied2	⊢ ( ( ( 𝜑 ∧ ( 𝑝 = 𝑃 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑑 = 𝐷 ) → ⦋ ( 2nd ‘ 𝑝 ) / 𝑒 ⦌ ⦋ ( 𝑑 Func 𝑒 ) / 𝑏 ⦌ ⟨ ( 𝑘 ∈ 𝑏 ↦ ( 𝑘 ∘func 𝑓 ) ) , ( 𝑘 ∈ 𝑏 , 𝑙 ∈ 𝑏 ↦ ( 𝑎 ∈ ( 𝑘 ( 𝑑 Nat 𝑒 ) 𝑙 ) ↦ ( 𝑎 ∘ ( 1st ‘ 𝑓 ) ) ) ) ⟩ = ⟨ ( 𝑘 ∈ 𝐵 ↦ ( 𝑘 ∘func 𝐹 ) ) , ( 𝑘 ∈ 𝐵 , 𝑙 ∈ 𝐵 ↦ ( 𝑎 ∈ ( 𝑘 𝑁 𝑙 ) ↦ ( 𝑎 ∘ ( 1st ‘ 𝐹 ) ) ) ) ⟩ )
39	9 13 38	csbied2	⊢ ( ( 𝜑 ∧ ( 𝑝 = 𝑃 ∧ 𝑓 = 𝐹 ) ) → ⦋ ( 1st ‘ 𝑝 ) / 𝑑 ⦌ ⦋ ( 2nd ‘ 𝑝 ) / 𝑒 ⦌ ⦋ ( 𝑑 Func 𝑒 ) / 𝑏 ⦌ ⟨ ( 𝑘 ∈ 𝑏 ↦ ( 𝑘 ∘func 𝑓 ) ) , ( 𝑘 ∈ 𝑏 , 𝑙 ∈ 𝑏 ↦ ( 𝑎 ∈ ( 𝑘 ( 𝑑 Nat 𝑒 ) 𝑙 ) ↦ ( 𝑎 ∘ ( 1st ‘ 𝑓 ) ) ) ) ⟩ = ⟨ ( 𝑘 ∈ 𝐵 ↦ ( 𝑘 ∘func 𝐹 ) ) , ( 𝑘 ∈ 𝐵 , 𝑙 ∈ 𝐵 ↦ ( 𝑎 ∈ ( 𝑘 𝑁 𝑙 ) ↦ ( 𝑎 ∘ ( 1st ‘ 𝐹 ) ) ) ) ⟩ )
40	4	elexd	⊢ ( 𝜑 → 𝑃 ∈ V )
41	3	elexd	⊢ ( 𝜑 → 𝐹 ∈ V )
42		opex	⊢ ⟨ ( 𝑘 ∈ 𝐵 ↦ ( 𝑘 ∘func 𝐹 ) ) , ( 𝑘 ∈ 𝐵 , 𝑙 ∈ 𝐵 ↦ ( 𝑎 ∈ ( 𝑘 𝑁 𝑙 ) ↦ ( 𝑎 ∘ ( 1st ‘ 𝐹 ) ) ) ) ⟩ ∈ V
43	42	a1i	⊢ ( 𝜑 → ⟨ ( 𝑘 ∈ 𝐵 ↦ ( 𝑘 ∘func 𝐹 ) ) , ( 𝑘 ∈ 𝐵 , 𝑙 ∈ 𝐵 ↦ ( 𝑎 ∈ ( 𝑘 𝑁 𝑙 ) ↦ ( 𝑎 ∘ ( 1st ‘ 𝐹 ) ) ) ) ⟩ ∈ V )
44	8 39 40 41 43	ovmpod	⊢ ( 𝜑 → ( 𝑃 −∘F 𝐹 ) = ⟨ ( 𝑘 ∈ 𝐵 ↦ ( 𝑘 ∘func 𝐹 ) ) , ( 𝑘 ∈ 𝐵 , 𝑙 ∈ 𝐵 ↦ ( 𝑎 ∈ ( 𝑘 𝑁 𝑙 ) ↦ ( 𝑎 ∘ ( 1st ‘ 𝐹 ) ) ) ) ⟩ )