Metamath Proof Explorer

Theorem fuco22a

Description: The morphism part of the functor composition bifunctor. See also fuco22 . (Contributed by Zhi Wang, 1-Oct-2025)

Ref Expression
Hypotheses fuco22a.o 
|- ( ph -> ( <. C , D >. o.F E ) = <. O , P >. )
fuco22a.u 
|- ( ph -> U = <. K , F >. )
fuco22a.v 
|- ( ph -> V = <. R , M >. )
fuco22a.a 
|- ( ph -> A e. ( F ( C Nat D ) M ) )
fuco22a.b 
|- ( ph -> B e. ( K ( D Nat E ) R ) )
Assertion fuco22a 
|- ( ph -> ( B ( U P V ) A ) = ( x e. ( Base ` C ) |-> ( ( B ` ( ( 1st ` M ) ` x ) ) ( <. ( ( 1st ` K ) ` ( ( 1st ` F ) ` x ) ) , ( ( 1st ` K ) ` ( ( 1st ` M ) ` x ) ) >. ( comp ` E ) ( ( 1st ` R ) ` ( ( 1st ` M ) ` x ) ) ) ( ( ( ( 1st ` F ) ` x ) ( 2nd ` K ) ( ( 1st ` M ) ` x ) ) ` ( A ` x ) ) ) ) )

Proof

Step Hyp Ref Expression
1 fuco22a.o 
 |-  ( ph -> ( <. C , D >. o.F E ) = <. O , P >. )
2 fuco22a.u 
 |-  ( ph -> U = <. K , F >. )
3 fuco22a.v 
 |-  ( ph -> V = <. R , M >. )
4 fuco22a.a 
 |-  ( ph -> A e. ( F ( C Nat D ) M ) )
5 fuco22a.b 
 |-  ( ph -> B e. ( K ( D Nat E ) R ) )
6 relfunc 
 |-  Rel ( D Func E )
7 df-rel 
 |-  ( Rel ( D Func E ) <-> ( D Func E ) C_ ( _V X. _V ) )
8 6 7 mpbi 
 |-  ( D Func E ) C_ ( _V X. _V )
9 eqid 
 |-  ( D Nat E ) = ( D Nat E )
10 9 natrcl 
 |-  ( B e. ( K ( D Nat E ) R ) -> ( K e. ( D Func E ) /\ R e. ( D Func E ) ) )
11 5 10 syl 
 |-  ( ph -> ( K e. ( D Func E ) /\ R e. ( D Func E ) ) )
12 11 simpld 
 |-  ( ph -> K e. ( D Func E ) )
13 8 12 sselid 
 |-  ( ph -> K e. ( _V X. _V ) )
14 1st2ndb 
 |-  ( K e. ( _V X. _V ) <-> K = <. ( 1st ` K ) , ( 2nd ` K ) >. )
15 13 14 sylib 
 |-  ( ph -> K = <. ( 1st ` K ) , ( 2nd ` K ) >. )
16 relfunc 
 |-  Rel ( C Func D )
17 df-rel 
 |-  ( Rel ( C Func D ) <-> ( C Func D ) C_ ( _V X. _V ) )
18 16 17 mpbi 
 |-  ( C Func D ) C_ ( _V X. _V )
19 eqid 
 |-  ( C Nat D ) = ( C Nat D )
20 19 natrcl 
 |-  ( A e. ( F ( C Nat D ) M ) -> ( F e. ( C Func D ) /\ M e. ( C Func D ) ) )
21 4 20 syl 
 |-  ( ph -> ( F e. ( C Func D ) /\ M e. ( C Func D ) ) )
22 21 simpld 
 |-  ( ph -> F e. ( C Func D ) )
23 18 22 sselid 
 |-  ( ph -> F e. ( _V X. _V ) )
24 1st2ndb 
 |-  ( F e. ( _V X. _V ) <-> F = <. ( 1st ` F ) , ( 2nd ` F ) >. )
25 23 24 sylib 
 |-  ( ph -> F = <. ( 1st ` F ) , ( 2nd ` F ) >. )
26 15 25 opeq12d 
 |-  ( ph -> <. K , F >. = <. <. ( 1st ` K ) , ( 2nd ` K ) >. , <. ( 1st ` F ) , ( 2nd ` F ) >. >. )
27 2 26 eqtrd 
 |-  ( ph -> U = <. <. ( 1st ` K ) , ( 2nd ` K ) >. , <. ( 1st ` F ) , ( 2nd ` F ) >. >. )
28 11 simprd 
 |-  ( ph -> R e. ( D Func E ) )
29 8 28 sselid 
 |-  ( ph -> R e. ( _V X. _V ) )
30 1st2ndb 
 |-  ( R e. ( _V X. _V ) <-> R = <. ( 1st ` R ) , ( 2nd ` R ) >. )
31 29 30 sylib 
 |-  ( ph -> R = <. ( 1st ` R ) , ( 2nd ` R ) >. )
32 21 simprd 
 |-  ( ph -> M e. ( C Func D ) )
33 18 32 sselid 
 |-  ( ph -> M e. ( _V X. _V ) )
34 1st2ndb 
 |-  ( M e. ( _V X. _V ) <-> M = <. ( 1st ` M ) , ( 2nd ` M ) >. )
35 33 34 sylib 
 |-  ( ph -> M = <. ( 1st ` M ) , ( 2nd ` M ) >. )
36 31 35 opeq12d 
 |-  ( ph -> <. R , M >. = <. <. ( 1st ` R ) , ( 2nd ` R ) >. , <. ( 1st ` M ) , ( 2nd ` M ) >. >. )
37 3 36 eqtrd 
 |-  ( ph -> V = <. <. ( 1st ` R ) , ( 2nd ` R ) >. , <. ( 1st ` M ) , ( 2nd ` M ) >. >. )
38 19 4 nat1st2nd 
 |-  ( ph -> A e. ( <. ( 1st ` F ) , ( 2nd ` F ) >. ( C Nat D ) <. ( 1st ` M ) , ( 2nd ` M ) >. ) )
39 9 5 nat1st2nd 
 |-  ( ph -> B e. ( <. ( 1st ` K ) , ( 2nd ` K ) >. ( D Nat E ) <. ( 1st ` R ) , ( 2nd ` R ) >. ) )
40 1 27 37 38 39 fuco22 
 |-  ( ph -> ( B ( U P V ) A ) = ( x e. ( Base ` C ) |-> ( ( B ` ( ( 1st ` M ) ` x ) ) ( <. ( ( 1st ` K ) ` ( ( 1st ` F ) ` x ) ) , ( ( 1st ` K ) ` ( ( 1st ` M ) ` x ) ) >. ( comp ` E ) ( ( 1st ` R ) ` ( ( 1st ` M ) ` x ) ) ) ( ( ( ( 1st ` F ) ` x ) ( 2nd ` K ) ( ( 1st ` M ) ` x ) ) ` ( A ` x ) ) ) ) )