precofval3

Description: Value of the pre-composition functor as a transposed curry of the functor composition bifunctor. (Contributed by Zhi Wang, 20-Oct-2025)

	Ref	Expression
Hypotheses	precoffunc.r	$⊢ R = D FuncCat E$
	precoffunc.b	$⊢ B = D Func E$
	precoffunc.n	$⊢ N = D Nat E$
	precoffunc.f	$⊢ φ \to F (C Func D) G$
	precoffunc.e	$⊢ φ \to E \in Cat$
	precoffunc.k	$⊢ φ \to K = (g \in B ⟼ g \circ_{func} ⟨F, G⟩)$
	precoffunc.l	$⊢ φ \to L = (g \in B, h \in B ⟼ (a \in (g N h) ⟼ a \circ F))$
	precofval3.q	$⊢ Q = C FuncCat D$
	precofval3.o	No typesetting found for \|- ( ph -> .o. = ( <. Q , R >. curryF ( ( <. C , D >. o.F E ) o.func ( Q swapF R ) ) ) ) with typecode \|-
	precofval3.m	No typesetting found for \|- ( ph -> M = ( ( 1st ` .o. ) ` <. F , G >. ) ) with typecode \|-
Assertion	precofval3	$⊢ φ \to ⟨K, L⟩ = M$

Proof

Step	Hyp	Ref	Expression
1		precoffunc.r	$⊢ R = D FuncCat E$
2		precoffunc.b	$⊢ B = D Func E$
3		precoffunc.n	$⊢ N = D Nat E$
4		precoffunc.f	$⊢ φ \to F (C Func D) G$
5		precoffunc.e	$⊢ φ \to E \in Cat$
6		precoffunc.k	$⊢ φ \to K = (g \in B ⟼ g \circ_{func} ⟨F, G⟩)$
7		precoffunc.l	$⊢ φ \to L = (g \in B, h \in B ⟼ (a \in (g N h) ⟼ a \circ F))$
8		precofval3.q	$⊢ Q = C FuncCat D$
9		precofval3.o	Could not format ( ph -> .o. = ( <. Q , R >. curryF ( ( <. C , D >. o.F E ) o.func ( Q swapF R ) ) ) ) : No typesetting found for \|- ( ph -> .o. = ( <. Q , R >. curryF ( ( <. C , D >. o.F E ) o.func ( Q swapF R ) ) ) ) with typecode \|-
10		precofval3.m	Could not format ( ph -> M = ( ( 1st ` .o. ) ` <. F , G >. ) ) : No typesetting found for \|- ( ph -> M = ( ( 1st ` .o. ) ` <. F , G >. ) ) with typecode \|-
11	2	mpteq1i	$⊢ (g \in B ⟼ g \circ_{func} ⟨F, G⟩) = (g \in (D Func E) ⟼ g \circ_{func} ⟨F, G⟩)$
12	6 11	eqtrdi	$⊢ φ \to K = (g \in (D Func E) ⟼ g \circ_{func} ⟨F, G⟩)$
13	2	a1i	$⊢ φ \to B = D Func E$
14	3	a1i	$⊢ φ \to N = D Nat E$
15	14	oveqd	$⊢ φ \to g N h = g (D Nat E) h$
16		relfunc	$⊢ Rel (C Func D)$
17		brrelex12	$⊢ (Rel (C Func D) \land F (C Func D) G) \to (F \in V \land G \in V)$
18	16 4 17	sylancr	$⊢ φ \to (F \in V \land G \in V)$
19		op1stg	$⊢ (F \in V \land G \in V) \to 1^{st} (⟨F, G⟩) = F$
20	18 19	syl	$⊢ φ \to 1^{st} (⟨F, G⟩) = F$
21	20	eqcomd	$⊢ φ \to F = 1^{st} (⟨F, G⟩)$
22	21	coeq2d	$⊢ φ \to a \circ F = a \circ 1^{st} (⟨F, G⟩)$
23	15 22	mpteq12dv	$⊢ φ \to (a \in (g N h) ⟼ a \circ F) = (a \in (g (D Nat E) h) ⟼ a \circ 1^{st} (⟨F, G⟩))$
24	13 13 23	mpoeq123dv	$⊢ φ \to (g \in B, h \in B ⟼ (a \in (g N h) ⟼ a \circ F)) = (g \in (D Func E), h \in (D Func E) ⟼ (a \in (g (D Nat E) h) ⟼ a \circ 1^{st} (⟨F, G⟩)))$
25	7 24	eqtrd	$⊢ φ \to L = (g \in (D Func E), h \in (D Func E) ⟼ (a \in (g (D Nat E) h) ⟼ a \circ 1^{st} (⟨F, G⟩)))$
26	12 25	opeq12d	$⊢ φ \to ⟨K, L⟩ = ⟨(g \in (D Func E) ⟼ g \circ_{func} ⟨F, G⟩), (g \in (D Func E), h \in (D Func E) ⟼ (a \in (g (D Nat E) h) ⟼ a \circ 1^{st} (⟨F, G⟩)))⟩$
27		df-br	$⊢ F (C Func D) G \leftrightarrow ⟨F, G⟩ \in (C Func D)$
28	4 27	sylib	$⊢ φ \to ⟨F, G⟩ \in (C Func D)$
29	8 1 9 28 5 10	precofval2	$⊢ φ \to M = ⟨(g \in (D Func E) ⟼ g \circ_{func} ⟨F, G⟩), (g \in (D Func E), h \in (D Func E) ⟼ (a \in (g (D Nat E) h) ⟼ a \circ 1^{st} (⟨F, G⟩)))⟩$
30	26 29	eqtr4d	$⊢ φ \to ⟨K, L⟩ = M$

Metamath Proof Explorer

Theorem precofval3

Proof