Metamath Proof Explorer

Theorem 0funcg2

Description: The functor from the empty category. (Contributed by Zhi Wang, 17-Oct-2025)

Ref Expression
Hypotheses 0funcg.c 
|- ( ph -> C e. V )
0funcg.b 
|- ( ph -> (/) = ( Base ` C ) )
0funcg.d 
|- ( ph -> D e. Cat )
Assertion 0funcg2 
|- ( ph -> ( F ( C Func D ) G <-> ( F = (/) /\ G = (/) ) ) )

Proof

Step Hyp Ref Expression
1 0funcg.c 
 |-  ( ph -> C e. V )
2 0funcg.b 
 |-  ( ph -> (/) = ( Base ` C ) )
3 0funcg.d 
 |-  ( ph -> D e. Cat )
4 eqid 
 |-  ( Base ` C ) = ( Base ` C )
5 eqid 
 |-  ( Base ` D ) = ( Base ` D )
6 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
7 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
8 eqid 
 |-  ( Id ` C ) = ( Id ` C )
9 eqid 
 |-  ( Id ` D ) = ( Id ` D )
10 eqid 
 |-  ( comp ` C ) = ( comp ` C )
11 eqid 
 |-  ( comp ` D ) = ( comp ` D )
12 0catg 
 |-  ( ( C e. V /\ (/) = ( Base ` C ) ) -> C e. Cat )
13 1 2 12 syl2anc 
 |-  ( ph -> C e. Cat )
14 4 5 6 7 8 9 10 11 13 3 isfunc 
 |-  ( ph -> ( F ( C Func D ) G <-> ( F : ( Base ` C ) --> ( Base ` D ) /\ G e. X_ z e. ( ( Base ` C ) X. ( Base ` C ) ) ( ( ( F ` ( 1st ` z ) ) ( Hom ` D ) ( F ` ( 2nd ` z ) ) ) ^m ( ( Hom ` C ) ` z ) ) /\ A. x e. ( Base ` C ) ( ( ( x G x ) ` ( ( Id ` C ) ` x ) ) = ( ( Id ` D ) ` ( F ` x ) ) /\ A. y e. ( Base ` C ) A. z e. ( Base ` C ) A. m e. ( x ( Hom ` C ) y ) A. n e. ( y ( Hom ` C ) z ) ( ( x G z ) ` ( n ( <. x , y >. ( comp ` C ) z ) m ) ) = ( ( ( y G z ) ` n ) ( <. ( F ` x ) , ( F ` y ) >. ( comp ` D ) ( F ` z ) ) ( ( x G y ) ` m ) ) ) ) ) )
15 2 feq2d 
 |-  ( ph -> ( F : (/) --> ( Base ` D ) <-> F : ( Base ` C ) --> ( Base ` D ) ) )
16 f0bi 
 |-  ( F : (/) --> ( Base ` D ) <-> F = (/) )
17 15 16 bitr3di 
 |-  ( ph -> ( F : ( Base ` C ) --> ( Base ` D ) <-> F = (/) ) )
18 2 eqcomd 
 |-  ( ph -> ( Base ` C ) = (/) )
19 rzal 
 |-  ( ( Base ` C ) = (/) -> A. x e. ( Base ` C ) A. y e. ( Base ` C ) ( x G y ) : ( x ( Hom ` C ) y ) --> ( ( F ` x ) ( Hom ` D ) ( F ` y ) ) )
20 18 19 syl 
 |-  ( ph -> A. x e. ( Base ` C ) A. y e. ( Base ` C ) ( x G y ) : ( x ( Hom ` C ) y ) --> ( ( F ` x ) ( Hom ` D ) ( F ` y ) ) )
21 4 funcf2lem2 
 |-  ( G e. X_ z e. ( ( Base ` C ) X. ( Base ` C ) ) ( ( ( F ` ( 1st ` z ) ) ( Hom ` D ) ( F ` ( 2nd ` z ) ) ) ^m ( ( Hom ` C ) ` z ) ) <-> ( G Fn ( ( Base ` C ) X. ( Base ` C ) ) /\ A. x e. ( Base ` C ) A. y e. ( Base ` C ) ( x G y ) : ( x ( Hom ` C ) y ) --> ( ( F ` x ) ( Hom ` D ) ( F ` y ) ) ) )
22 21 a1i 
 |-  ( ph -> ( G e. X_ z e. ( ( Base ` C ) X. ( Base ` C ) ) ( ( ( F ` ( 1st ` z ) ) ( Hom ` D ) ( F ` ( 2nd ` z ) ) ) ^m ( ( Hom ` C ) ` z ) ) <-> ( G Fn ( ( Base ` C ) X. ( Base ` C ) ) /\ A. x e. ( Base ` C ) A. y e. ( Base ` C ) ( x G y ) : ( x ( Hom ` C ) y ) --> ( ( F ` x ) ( Hom ` D ) ( F ` y ) ) ) ) )
23 20 22 mpbiran2d 
 |-  ( ph -> ( G e. X_ z e. ( ( Base ` C ) X. ( Base ` C ) ) ( ( ( F ` ( 1st ` z ) ) ( Hom ` D ) ( F ` ( 2nd ` z ) ) ) ^m ( ( Hom ` C ) ` z ) ) <-> G Fn ( ( Base ` C ) X. ( Base ` C ) ) ) )
24 2 sqxpeqd 
 |-  ( ph -> ( (/) X. (/) ) = ( ( Base ` C ) X. ( Base ` C ) ) )
25 0xp 
 |-  ( (/) X. (/) ) = (/)
26 24 25 eqtr3di 
 |-  ( ph -> ( ( Base ` C ) X. ( Base ` C ) ) = (/) )
27 26 fneq2d 
 |-  ( ph -> ( G Fn ( ( Base ` C ) X. ( Base ` C ) ) <-> G Fn (/) ) )
28 fn0 
 |-  ( G Fn (/) <-> G = (/) )
29 27 28 bitrdi 
 |-  ( ph -> ( G Fn ( ( Base ` C ) X. ( Base ` C ) ) <-> G = (/) ) )
30 23 29 bitrd 
 |-  ( ph -> ( G e. X_ z e. ( ( Base ` C ) X. ( Base ` C ) ) ( ( ( F ` ( 1st ` z ) ) ( Hom ` D ) ( F ` ( 2nd ` z ) ) ) ^m ( ( Hom ` C ) ` z ) ) <-> G = (/) ) )
31 rzal 
 |-  ( ( Base ` C ) = (/) -> A. x e. ( Base ` C ) ( ( ( x G x ) ` ( ( Id ` C ) ` x ) ) = ( ( Id ` D ) ` ( F ` x ) ) /\ A. y e. ( Base ` C ) A. z e. ( Base ` C ) A. m e. ( x ( Hom ` C ) y ) A. n e. ( y ( Hom ` C ) z ) ( ( x G z ) ` ( n ( <. x , y >. ( comp ` C ) z ) m ) ) = ( ( ( y G z ) ` n ) ( <. ( F ` x ) , ( F ` y ) >. ( comp ` D ) ( F ` z ) ) ( ( x G y ) ` m ) ) ) )
32 18 31 syl 
 |-  ( ph -> A. x e. ( Base ` C ) ( ( ( x G x ) ` ( ( Id ` C ) ` x ) ) = ( ( Id ` D ) ` ( F ` x ) ) /\ A. y e. ( Base ` C ) A. z e. ( Base ` C ) A. m e. ( x ( Hom ` C ) y ) A. n e. ( y ( Hom ` C ) z ) ( ( x G z ) ` ( n ( <. x , y >. ( comp ` C ) z ) m ) ) = ( ( ( y G z ) ` n ) ( <. ( F ` x ) , ( F ` y ) >. ( comp ` D ) ( F ` z ) ) ( ( x G y ) ` m ) ) ) )
33 14 17 30 32 0funcglem 
 |-  ( ph -> ( F ( C Func D ) G <-> ( F = (/) /\ G = (/) ) ) )