Theorem fucoelvv

Description: A functor composition bifunctor is an ordered pair. Enables 1st2ndb . (Contributed by Zhi Wang, 29-Sep-2025)

	Ref	Expression
Hypotheses	fucofval.c	$$⊢\phi \to C\in T$$
	fucofval.d	$$⊢\phi \to D\in U$$
	fucofval.e	$$⊢\phi \to E\in V$$
	fucofval.o	No typesetting found for |- ( ph -> ( <. C , D >. o.F E ) = .o. ) with typecode |-
Assertion	fucoelvv	Could not format assertion : No typesetting found for |- ( ph -> .o. e. ( _V X. _V ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		fucofval.c	$$⊢\phi \to C\in T$$
2		fucofval.d	$$⊢\phi \to D\in U$$
3		fucofval.e	$$⊢\phi \to E\in V$$
4		fucofval.o	Could not format ( ph -> ( <. C , D >. o.F E ) = .o. ) : No typesetting found for |- ( ph -> ( <. C , D >. o.F E ) = .o. ) with typecode |-
5		eqidd	$$⊢\phi \to \left(D\mathrm{Func}E\right)\times \left(C\mathrm{Func}D\right)=\left(D\mathrm{Func}E\right)\times \left(C\mathrm{Func}D\right)$$
6	1 2 3 4 5	fucofval	Could not format ( ph -> .o. = <. ( o.func |` ( ( D Func E ) X. ( C Func D ) ) ) , ( u e. ( ( D Func E ) X. ( C Func D ) ) , v e. ( ( D Func E ) X. ( C Func D ) ) |-> [_ ( 1st ` ( 2nd ` u ) ) / f ]_ [_ ( 1st ` ( 1st ` u ) ) / k ]_ [_ ( 2nd ` ( 1st ` u ) ) / l ]_ [_ ( 1st ` ( 2nd ` v ) ) / m ]_ [_ ( 1st ` ( 1st ` v ) ) / r ]_ ( b e. ( ( 1st ` u ) ( D Nat E ) ( 1st ` v ) ) , a e. ( ( 2nd ` u ) ( C Nat D ) ( 2nd ` v ) ) |-> ( x e. ( Base ` C ) |-> ( ( b ` ( m ` x ) ) ( <. ( k ` ( f ` x ) ) , ( k ` ( m ` x ) ) >. ( comp ` E ) ( r ` ( m ` x ) ) ) ( ( ( f ` x ) l ( m ` x ) ) ` ( a ` x ) ) ) ) ) ) >. ) : No typesetting found for |- ( ph -> .o. = <. ( o.func |` ( ( D Func E ) X. ( C Func D ) ) ) , ( u e. ( ( D Func E ) X. ( C Func D ) ) , v e. ( ( D Func E ) X. ( C Func D ) ) |-> [_ ( 1st ` ( 2nd ` u ) ) / f ]_ [_ ( 1st ` ( 1st ` u ) ) / k ]_ [_ ( 2nd ` ( 1st ` u ) ) / l ]_ [_ ( 1st ` ( 2nd ` v ) ) / m ]_ [_ ( 1st ` ( 1st ` v ) ) / r ]_ ( b e. ( ( 1st ` u ) ( D Nat E ) ( 1st ` v ) ) , a e. ( ( 2nd ` u ) ( C Nat D ) ( 2nd ` v ) ) |-> ( x e. ( Base ` C ) |-> ( ( b ` ( m ` x ) ) ( <. ( k ` ( f ` x ) ) , ( k ` ( m ` x ) ) >. ( comp ` E ) ( r ` ( m ` x ) ) ) ( ( ( f ` x ) l ( m ` x ) ) ` ( a ` x ) ) ) ) ) ) >. ) with typecode |-
7		df-cofu	$$⊢{\circ }_{\mathrm{func}}=\left(g\in \mathrm{V},f\in \mathrm{V}⟼⟨1^{st}\left(g\right)\circ 1^{st}\left(f\right),\left(x\in \mathrm{dom}\mathrm{dom}{2}^{nd}\left(f\right),y\in \mathrm{dom}\mathrm{dom}{2}^{nd}\left(f\right)⟼\left(1^{st}\left(f\right)\left(x\right)2^{nd}\left(g\right)1^{st}\left(f\right)\left(y\right)\right)\circ \left(x{2}^{nd}\left(f\right)y\right)\right)⟩\right)$$
8	7	mpofun	$$⊢\mathrm{Fun}{\circ }_{\mathrm{func}}$$
9		ovex	$$⊢D\mathrm{Func}E\in \mathrm{V}$$
10		ovex	$$⊢C\mathrm{Func}D\in \mathrm{V}$$
11	9 10	xpex	$$⊢\left(D\mathrm{Func}E\right)\times \left(C\mathrm{Func}D\right)\in \mathrm{V}$$
12		resfunexg	$$⊢\left(\mathrm{Fun}{\circ }_{\mathrm{func}}\wedge \left(D\mathrm{Func}E\right)\times \left(C\mathrm{Func}D\right)\in \mathrm{V}\right)\to {{\circ }_{\mathrm{func}}\upharpoonright }_{\left(\left(D\mathrm{Func}E\right)\times \left(C\mathrm{Func}D\right)\right)}\in \mathrm{V}$$
13	8 11 12	mp2an	$$⊢{{\circ }_{\mathrm{func}}\upharpoonright }_{\left(\left(D\mathrm{Func}E\right)\times \left(C\mathrm{Func}D\right)\right)}\in \mathrm{V}$$
14	11 11	mpoex	$$⊢\left(u\in \left(\left(D\mathrm{Func}E\right)\times \left(C\mathrm{Func}D\right)\right),v\in \left(\left(D\mathrm{Func}E\right)\times \left(C\mathrm{Func}D\right)\right)⟼⦋1^{st}\left(2^{nd}\left(u\right)\right)/f⦌⦋1^{st}\left(1^{st}\left(u\right)\right)/k⦌⦋2^{nd}\left(1^{st}\left(u\right)\right)/l⦌⦋1^{st}\left(2^{nd}\left(v\right)\right)/m⦌⦋1^{st}\left(1^{st}\left(v\right)\right)/r⦌\left(b\in \left(1^{st}\left(u\right)\left(D\mathrm{Nat}E\right)1^{st}\left(v\right)\right),a\in \left(2^{nd}\left(u\right)\left(C\mathrm{Nat}D\right)2^{nd}\left(v\right)\right)⟼\left(x\in {\mathrm{Base}}_C⟼b\left(m\left(x\right)\right)\left(⟨k\left(f\left(x\right)\right),k\left(m\left(x\right)\right)⟩\mathrm{comp}\left(E\right)r\left(m\left(x\right)\right)\right)\left(f\left(x\right)lm\left(x\right)\right)\left(a\left(x\right)\right)\right)\right)\right)\in \mathrm{V}$$
15	13 14	opelvv	$$⊢⟨{{\circ }_{\mathrm{func}}\upharpoonright }_{\left(\left(D\mathrm{Func}E\right)\times \left(C\mathrm{Func}D\right)\right)},\left(u\in \left(\left(D\mathrm{Func}E\right)\times \left(C\mathrm{Func}D\right)\right),v\in \left(\left(D\mathrm{Func}E\right)\times \left(C\mathrm{Func}D\right)\right)⟼⦋1^{st}\left(2^{nd}\left(u\right)\right)/f⦌⦋1^{st}\left(1^{st}\left(u\right)\right)/k⦌⦋2^{nd}\left(1^{st}\left(u\right)\right)/l⦌⦋1^{st}\left(2^{nd}\left(v\right)\right)/m⦌⦋1^{st}\left(1^{st}\left(v\right)\right)/r⦌\left(b\in \left(1^{st}\left(u\right)\left(D\mathrm{Nat}E\right)1^{st}\left(v\right)\right),a\in \left(2^{nd}\left(u\right)\left(C\mathrm{Nat}D\right)2^{nd}\left(v\right)\right)⟼\left(x\in {\mathrm{Base}}_C⟼b\left(m\left(x\right)\right)\left(⟨k\left(f\left(x\right)\right),k\left(m\left(x\right)\right)⟩\mathrm{comp}\left(E\right)r\left(m\left(x\right)\right)\right)\left(f\left(x\right)lm\left(x\right)\right)\left(a\left(x\right)\right)\right)\right)\right)⟩\in \left(\mathrm{V}\times \mathrm{V}\right)$$
16	6 15	eqeltrdi	Could not format ( ph -> .o. e. ( _V X. _V ) ) : No typesetting found for |- ( ph -> .o. e. ( _V X. _V ) ) with typecode |-