Metamath Proof Explorer

Theorem fucofvalne

Description: Value of the function giving the functor composition bifunctor, if C or D are not sets. (Contributed by Zhi Wang, 7-Oct-2025)

Ref Expression
Hypotheses fucofvalne.c 
|- ( ph -> -. ( C e. _V /\ D e. _V ) )
fucofvalne.e 
|- ( ph -> E e. Cat )
fucofvalne.o 
|- ( ph -> ( <. C , D >. o.F E ) = .o. )
fucofvalne.w 
|- ( ph -> W = ( ( D Func E ) X. ( C Func D ) ) )
Assertion fucofvalne 
|- ( ph -> .o. =/= <. ( o.func |` W ) , ( u e. W , v e. W |-> [_ ( 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 ) ) ) ) ) ) >. )

Proof

Step Hyp Ref Expression
1 fucofvalne.c 
 |-  ( ph -> -. ( C e. _V /\ D e. _V ) )
2 fucofvalne.e 
 |-  ( ph -> E e. Cat )
3 fucofvalne.o 
 |-  ( ph -> ( <. C , D >. o.F E ) = .o. )
4 fucofvalne.w 
 |-  ( ph -> W = ( ( D Func E ) X. ( C Func D ) ) )
5 0ex 
 |-  (/) e. _V
6 5 a1i 
 |-  ( ph -> (/) e. _V )
7 1st0 
 |-  ( 1st ` (/) ) = (/)
8 7 a1i 
 |-  ( ph -> ( 1st ` (/) ) = (/) )
9 2nd0 
 |-  ( 2nd ` (/) ) = (/)
10 9 a1i 
 |-  ( ph -> ( 2nd ` (/) ) = (/) )
11 opprc 
 |-  ( -. ( C e. _V /\ D e. _V ) -> <. C , D >. = (/) )
12 1 11 syl 
 |-  ( ph -> <. C , D >. = (/) )
13 12 oveq1d 
 |-  ( ph -> ( <. C , D >. o.F E ) = ( (/) o.F E ) )
14 13 3 eqtr3d 
 |-  ( ph -> ( (/) o.F E ) = .o. )
15 eqidd 
 |-  ( ph -> ( ( (/) Func E ) X. ( (/) Func (/) ) ) = ( ( (/) Func E ) X. ( (/) Func (/) ) ) )
16 6 8 10 2 14 15 fucofvalg 
 |-  ( ph -> .o. = <. ( o.func |` ( ( (/) Func E ) X. ( (/) Func (/) ) ) ) , ( u e. ( ( (/) Func E ) X. ( (/) Func (/) ) ) , v e. ( ( (/) Func E ) X. ( (/) Func (/) ) ) |-> [_ ( 1st ` ( 2nd ` u ) ) / f ]_ [_ ( 1st ` ( 1st ` u ) ) / k ]_ [_ ( 2nd ` ( 1st ` u ) ) / l ]_ [_ ( 1st ` ( 2nd ` v ) ) / m ]_ [_ ( 1st ` ( 1st ` v ) ) / r ]_ ( b e. ( ( 1st ` u ) ( (/) Nat E ) ( 1st ` v ) ) , a e. ( ( 2nd ` u ) ( (/) Nat (/) ) ( 2nd ` v ) ) |-> ( x e. ( Base ` (/) ) |-> ( ( b ` ( m ` x ) ) ( <. ( k ` ( f ` x ) ) , ( k ` ( m ` x ) ) >. ( comp ` E ) ( r ` ( m ` x ) ) ) ( ( ( f ` x ) l ( m ` x ) ) ` ( a ` x ) ) ) ) ) ) >. )
17 opex 
 |-  <. (/) , (/) >. e. _V
18 17 snnz 
 |-  { <. (/) , (/) >. } =/= (/)
19 18 neii 
 |-  -. { <. (/) , (/) >. } = (/)
20 ioran 
 |-  ( -. ( { <. (/) , (/) >. } = (/) \/ { <. (/) , (/) >. } = (/) ) <-> ( -. { <. (/) , (/) >. } = (/) /\ -. { <. (/) , (/) >. } = (/) ) )
21 xpeq0 
 |-  ( ( { <. (/) , (/) >. } X. { <. (/) , (/) >. } ) = (/) <-> ( { <. (/) , (/) >. } = (/) \/ { <. (/) , (/) >. } = (/) ) )
22 21 biimpi 
 |-  ( ( { <. (/) , (/) >. } X. { <. (/) , (/) >. } ) = (/) -> ( { <. (/) , (/) >. } = (/) \/ { <. (/) , (/) >. } = (/) ) )
23 22 con3i 
 |-  ( -. ( { <. (/) , (/) >. } = (/) \/ { <. (/) , (/) >. } = (/) ) -> -. ( { <. (/) , (/) >. } X. { <. (/) , (/) >. } ) = (/) )
24 20 23 sylbir 
 |-  ( ( -. { <. (/) , (/) >. } = (/) /\ -. { <. (/) , (/) >. } = (/) ) -> -. ( { <. (/) , (/) >. } X. { <. (/) , (/) >. } ) = (/) )
25 19 19 24 mp2an 
 |-  -. ( { <. (/) , (/) >. } X. { <. (/) , (/) >. } ) = (/)
26 2 0func 
 |-  ( ph -> ( (/) Func E ) = { <. (/) , (/) >. } )
27 0cat 
 |-  (/) e. Cat
28 27 a1i 
 |-  ( ph -> (/) e. Cat )
29 28 0func 
 |-  ( ph -> ( (/) Func (/) ) = { <. (/) , (/) >. } )
30 26 29 xpeq12d 
 |-  ( ph -> ( ( (/) Func E ) X. ( (/) Func (/) ) ) = ( { <. (/) , (/) >. } X. { <. (/) , (/) >. } ) )
31 df-func 
 |-  Func = ( t e. Cat , u e. Cat |-> { <. f , g >. | [. ( Base ` t ) / b ]. ( f : b --> ( Base ` u ) /\ g e. X_ z e. ( b X. b ) ( ( ( f ` ( 1st ` z ) ) ( Hom ` u ) ( f ` ( 2nd ` z ) ) ) ^m ( ( Hom ` t ) ` z ) ) /\ A. x e. b ( ( ( x g x ) ` ( ( Id ` t ) ` x ) ) = ( ( Id ` u ) ` ( f ` x ) ) /\ A. y e. b A. z e. b A. m e. ( x ( Hom ` t ) y ) A. n e. ( y ( Hom ` t ) z ) ( ( x g z ) ` ( n ( <. x , y >. ( comp ` t ) z ) m ) ) = ( ( ( y g z ) ` n ) ( <. ( f ` x ) , ( f ` y ) >. ( comp ` u ) ( f ` z ) ) ( ( x g y ) ` m ) ) ) ) } )
32 31 reldmmpo 
 |-  Rel dom Func
33 0nelrel0 
 |-  ( Rel dom Func -> -. (/) e. dom Func )
34 32 33 ax-mp 
 |-  -. (/) e. dom Func
35 12 eleq1d 
 |-  ( ph -> ( <. C , D >. e. dom Func <-> (/) e. dom Func ) )
36 34 35 mtbiri 
 |-  ( ph -> -. <. C , D >. e. dom Func )
37 df-ov 
 |-  ( C Func D ) = ( Func ` <. C , D >. )
38 ndmfv 
 |-  ( -. <. C , D >. e. dom Func -> ( Func ` <. C , D >. ) = (/) )
39 37 38 eqtrid 
 |-  ( -. <. C , D >. e. dom Func -> ( C Func D ) = (/) )
40 39 xpeq2d 
 |-  ( -. <. C , D >. e. dom Func -> ( ( D Func E ) X. ( C Func D ) ) = ( ( D Func E ) X. (/) ) )
41 xp0 
 |-  ( ( D Func E ) X. (/) ) = (/)
42 40 41 eqtrdi 
 |-  ( -. <. C , D >. e. dom Func -> ( ( D Func E ) X. ( C Func D ) ) = (/) )
43 36 42 syl 
 |-  ( ph -> ( ( D Func E ) X. ( C Func D ) ) = (/) )
44 30 43 eqeq12d 
 |-  ( ph -> ( ( ( (/) Func E ) X. ( (/) Func (/) ) ) = ( ( D Func E ) X. ( C Func D ) ) <-> ( { <. (/) , (/) >. } X. { <. (/) , (/) >. } ) = (/) ) )
45 25 44 mtbiri 
 |-  ( ph -> -. ( ( (/) Func E ) X. ( (/) Func (/) ) ) = ( ( D Func E ) X. ( C Func D ) ) )
46 rescofuf 
 |-  ( o.func |` ( ( (/) Func E ) X. ( (/) Func (/) ) ) ) : ( ( (/) Func E ) X. ( (/) Func (/) ) ) --> ( (/) Func E )
47 46 fdmi 
 |-  dom ( o.func |` ( ( (/) Func E ) X. ( (/) Func (/) ) ) ) = ( ( (/) Func E ) X. ( (/) Func (/) ) )
48 rescofuf 
 |-  ( o.func |` ( ( D Func E ) X. ( C Func D ) ) ) : ( ( D Func E ) X. ( C Func D ) ) --> ( C Func E )
49 48 fdmi 
 |-  dom ( o.func |` ( ( D Func E ) X. ( C Func D ) ) ) = ( ( D Func E ) X. ( C Func D ) )
50 47 49 eqeq12i 
 |-  ( dom ( o.func |` ( ( (/) Func E ) X. ( (/) Func (/) ) ) ) = dom ( o.func |` ( ( D Func E ) X. ( C Func D ) ) ) <-> ( ( (/) Func E ) X. ( (/) Func (/) ) ) = ( ( D Func E ) X. ( C Func D ) ) )
51 50 biimpi 
 |-  ( dom ( o.func |` ( ( (/) Func E ) X. ( (/) Func (/) ) ) ) = dom ( o.func |` ( ( D Func E ) X. ( C Func D ) ) ) -> ( ( (/) Func E ) X. ( (/) Func (/) ) ) = ( ( D Func E ) X. ( C Func D ) ) )
52 51 con3i 
 |-  ( -. ( ( (/) Func E ) X. ( (/) Func (/) ) ) = ( ( D Func E ) X. ( C Func D ) ) -> -. dom ( o.func |` ( ( (/) Func E ) X. ( (/) Func (/) ) ) ) = dom ( o.func |` ( ( D Func E ) X. ( C Func D ) ) ) )
53 dmeq 
 |-  ( ( o.func |` ( ( (/) Func E ) X. ( (/) Func (/) ) ) ) = ( o.func |` ( ( D Func E ) X. ( C Func D ) ) ) -> dom ( o.func |` ( ( (/) Func E ) X. ( (/) Func (/) ) ) ) = dom ( o.func |` ( ( D Func E ) X. ( C Func D ) ) ) )
54 53 con3i 
 |-  ( -. dom ( o.func |` ( ( (/) Func E ) X. ( (/) Func (/) ) ) ) = dom ( o.func |` ( ( D Func E ) X. ( C Func D ) ) ) -> -. ( o.func |` ( ( (/) Func E ) X. ( (/) Func (/) ) ) ) = ( o.func |` ( ( D Func E ) X. ( C Func D ) ) ) )
55 45 52 54 3syl 
 |-  ( ph -> -. ( o.func |` ( ( (/) Func E ) X. ( (/) Func (/) ) ) ) = ( o.func |` ( ( D Func E ) X. ( C Func D ) ) ) )
56 55 neqned 
 |-  ( ph -> ( o.func |` ( ( (/) Func E ) X. ( (/) Func (/) ) ) ) =/= ( o.func |` ( ( D Func E ) X. ( C Func D ) ) ) )
57 4 reseq2d 
 |-  ( ph -> ( o.func |` W ) = ( o.func |` ( ( D Func E ) X. ( C Func D ) ) ) )
58 56 57 neeqtrrd 
 |-  ( ph -> ( o.func |` ( ( (/) Func E ) X. ( (/) Func (/) ) ) ) =/= ( o.func |` W ) )
59 ovex 
 |-  ( (/) Func E ) e. _V
60 ovex 
 |-  ( (/) Func (/) ) e. _V
61 59 60 xpex 
 |-  ( ( (/) Func E ) X. ( (/) Func (/) ) ) e. _V
62 fex 
 |-  ( ( ( o.func |` ( ( (/) Func E ) X. ( (/) Func (/) ) ) ) : ( ( (/) Func E ) X. ( (/) Func (/) ) ) --> ( (/) Func E ) /\ ( ( (/) Func E ) X. ( (/) Func (/) ) ) e. _V ) -> ( o.func |` ( ( (/) Func E ) X. ( (/) Func (/) ) ) ) e. _V )
63 46 61 62 mp2an 
 |-  ( o.func |` ( ( (/) Func E ) X. ( (/) Func (/) ) ) ) e. _V
64 61 61 mpoex 
 |-  ( u e. ( ( (/) Func E ) X. ( (/) Func (/) ) ) , v e. ( ( (/) Func E ) X. ( (/) Func (/) ) ) |-> [_ ( 1st ` ( 2nd ` u ) ) / f ]_ [_ ( 1st ` ( 1st ` u ) ) / k ]_ [_ ( 2nd ` ( 1st ` u ) ) / l ]_ [_ ( 1st ` ( 2nd ` v ) ) / m ]_ [_ ( 1st ` ( 1st ` v ) ) / r ]_ ( b e. ( ( 1st ` u ) ( (/) Nat E ) ( 1st ` v ) ) , a e. ( ( 2nd ` u ) ( (/) Nat (/) ) ( 2nd ` v ) ) |-> ( x e. ( Base ` (/) ) |-> ( ( b ` ( m ` x ) ) ( <. ( k ` ( f ` x ) ) , ( k ` ( m ` x ) ) >. ( comp ` E ) ( r ` ( m ` x ) ) ) ( ( ( f ` x ) l ( m ` x ) ) ` ( a ` x ) ) ) ) ) ) e. _V
65 opth1neg 
 |-  ( ( ( o.func |` ( ( (/) Func E ) X. ( (/) Func (/) ) ) ) e. _V /\ ( u e. ( ( (/) Func E ) X. ( (/) Func (/) ) ) , v e. ( ( (/) Func E ) X. ( (/) Func (/) ) ) |-> [_ ( 1st ` ( 2nd ` u ) ) / f ]_ [_ ( 1st ` ( 1st ` u ) ) / k ]_ [_ ( 2nd ` ( 1st ` u ) ) / l ]_ [_ ( 1st ` ( 2nd ` v ) ) / m ]_ [_ ( 1st ` ( 1st ` v ) ) / r ]_ ( b e. ( ( 1st ` u ) ( (/) Nat E ) ( 1st ` v ) ) , a e. ( ( 2nd ` u ) ( (/) Nat (/) ) ( 2nd ` v ) ) |-> ( x e. ( Base ` (/) ) |-> ( ( b ` ( m ` x ) ) ( <. ( k ` ( f ` x ) ) , ( k ` ( m ` x ) ) >. ( comp ` E ) ( r ` ( m ` x ) ) ) ( ( ( f ` x ) l ( m ` x ) ) ` ( a ` x ) ) ) ) ) ) e. _V ) -> ( ( o.func |` ( ( (/) Func E ) X. ( (/) Func (/) ) ) ) =/= ( o.func |` W ) -> <. ( o.func |` ( ( (/) Func E ) X. ( (/) Func (/) ) ) ) , ( u e. ( ( (/) Func E ) X. ( (/) Func (/) ) ) , v e. ( ( (/) Func E ) X. ( (/) Func (/) ) ) |-> [_ ( 1st ` ( 2nd ` u ) ) / f ]_ [_ ( 1st ` ( 1st ` u ) ) / k ]_ [_ ( 2nd ` ( 1st ` u ) ) / l ]_ [_ ( 1st ` ( 2nd ` v ) ) / m ]_ [_ ( 1st ` ( 1st ` v ) ) / r ]_ ( b e. ( ( 1st ` u ) ( (/) Nat E ) ( 1st ` v ) ) , a e. ( ( 2nd ` u ) ( (/) Nat (/) ) ( 2nd ` v ) ) |-> ( x e. ( Base ` (/) ) |-> ( ( b ` ( m ` x ) ) ( <. ( k ` ( f ` x ) ) , ( k ` ( m ` x ) ) >. ( comp ` E ) ( r ` ( m ` x ) ) ) ( ( ( f ` x ) l ( m ` x ) ) ` ( a ` x ) ) ) ) ) ) >. =/= <. ( o.func |` W ) , ( u e. W , v e. W |-> [_ ( 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 ) ) ) ) ) ) >. ) )
66 63 64 65 mp2an 
 |-  ( ( o.func |` ( ( (/) Func E ) X. ( (/) Func (/) ) ) ) =/= ( o.func |` W ) -> <. ( o.func |` ( ( (/) Func E ) X. ( (/) Func (/) ) ) ) , ( u e. ( ( (/) Func E ) X. ( (/) Func (/) ) ) , v e. ( ( (/) Func E ) X. ( (/) Func (/) ) ) |-> [_ ( 1st ` ( 2nd ` u ) ) / f ]_ [_ ( 1st ` ( 1st ` u ) ) / k ]_ [_ ( 2nd ` ( 1st ` u ) ) / l ]_ [_ ( 1st ` ( 2nd ` v ) ) / m ]_ [_ ( 1st ` ( 1st ` v ) ) / r ]_ ( b e. ( ( 1st ` u ) ( (/) Nat E ) ( 1st ` v ) ) , a e. ( ( 2nd ` u ) ( (/) Nat (/) ) ( 2nd ` v ) ) |-> ( x e. ( Base ` (/) ) |-> ( ( b ` ( m ` x ) ) ( <. ( k ` ( f ` x ) ) , ( k ` ( m ` x ) ) >. ( comp ` E ) ( r ` ( m ` x ) ) ) ( ( ( f ` x ) l ( m ` x ) ) ` ( a ` x ) ) ) ) ) ) >. =/= <. ( o.func |` W ) , ( u e. W , v e. W |-> [_ ( 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 ) ) ) ) ) ) >. )
67 58 66 syl 
 |-  ( ph -> <. ( o.func |` ( ( (/) Func E ) X. ( (/) Func (/) ) ) ) , ( u e. ( ( (/) Func E ) X. ( (/) Func (/) ) ) , v e. ( ( (/) Func E ) X. ( (/) Func (/) ) ) |-> [_ ( 1st ` ( 2nd ` u ) ) / f ]_ [_ ( 1st ` ( 1st ` u ) ) / k ]_ [_ ( 2nd ` ( 1st ` u ) ) / l ]_ [_ ( 1st ` ( 2nd ` v ) ) / m ]_ [_ ( 1st ` ( 1st ` v ) ) / r ]_ ( b e. ( ( 1st ` u ) ( (/) Nat E ) ( 1st ` v ) ) , a e. ( ( 2nd ` u ) ( (/) Nat (/) ) ( 2nd ` v ) ) |-> ( x e. ( Base ` (/) ) |-> ( ( b ` ( m ` x ) ) ( <. ( k ` ( f ` x ) ) , ( k ` ( m ` x ) ) >. ( comp ` E ) ( r ` ( m ` x ) ) ) ( ( ( f ` x ) l ( m ` x ) ) ` ( a ` x ) ) ) ) ) ) >. =/= <. ( o.func |` W ) , ( u e. W , v e. W |-> [_ ( 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 ) ) ) ) ) ) >. )
68 16 67 eqnetrd 
 |-  ( ph -> .o. =/= <. ( o.func |` W ) , ( u e. W , v e. W |-> [_ ( 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 ) ) ) ) ) ) >. )