Metamath Proof Explorer

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 
|- ( ph -> C e. T )
fucofval.d 
|- ( ph -> D e. U )
fucofval.e 
|- ( ph -> E e. V )
fucofval.o 
|- ( ph -> ( <. C , D >. o.F E ) = .o. )
Assertion fucoelvv 
|- ( ph -> .o. e. ( _V X. _V ) )

Proof

Step Hyp Ref Expression
1 fucofval.c 
 |-  ( ph -> C e. T )
2 fucofval.d 
 |-  ( ph -> D e. U )
3 fucofval.e 
 |-  ( ph -> E e. V )
4 fucofval.o 
 |-  ( ph -> ( <. C , D >. o.F E ) = .o. )
5 eqidd 
 |-  ( ph -> ( ( D Func E ) X. ( C Func D ) ) = ( ( D Func E ) X. ( C Func D ) ) )
6 1 2 3 4 5 fucofval 
 |-  ( 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 ) ) ) ) ) ) >. )
7 df-cofu 
 |-  o.func = ( g e. _V , f e. _V |-> <. ( ( 1st ` g ) o. ( 1st ` f ) ) , ( x e. dom dom ( 2nd ` f ) , y e. dom dom ( 2nd ` f ) |-> ( ( ( ( 1st ` f ) ` x ) ( 2nd ` g ) ( ( 1st ` f ) ` y ) ) o. ( x ( 2nd ` f ) y ) ) ) >. )
8 7 mpofun 
 |-  Fun o.func
9 ovex 
 |-  ( D Func E ) e. _V
10 ovex 
 |-  ( C Func D ) e. _V
11 9 10 xpex 
 |-  ( ( D Func E ) X. ( C Func D ) ) e. _V
12 resfunexg 
 |-  ( ( Fun o.func /\ ( ( D Func E ) X. ( C Func D ) ) e. _V ) -> ( o.func |` ( ( D Func E ) X. ( C Func D ) ) ) e. _V )
13 8 11 12 mp2an 
 |-  ( o.func |` ( ( D Func E ) X. ( C Func D ) ) ) e. _V
14 11 11 mpoex 
 |-  ( 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 ) ) ) ) ) ) e. _V
15 13 14 opelvv 
 |-  <. ( 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 ) ) ) ) ) ) >. e. ( _V X. _V )
16 6 15 eqeltrdi 
 |-  ( ph -> .o. e. ( _V X. _V ) )