Metamath Proof Explorer

Theorem 0func

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

Ref Expression
Hypothesis 0func.c 
|- ( ph -> C e. Cat )
Assertion 0func 
|- ( ph -> ( (/) Func C ) = { <. (/) , (/) >. } )

Proof

Step Hyp Ref Expression
1 0func.c 
 |-  ( ph -> C e. Cat )
2 relfunc 
 |-  Rel ( (/) Func C )
3 0ex 
 |-  (/) e. _V
4 3 3 relsnop 
 |-  Rel { <. (/) , (/) >. }
5 base0 
 |-  (/) = ( Base ` (/) )
6 eqid 
 |-  ( Base ` C ) = ( Base ` C )
7 eqid 
 |-  ( Hom ` (/) ) = ( Hom ` (/) )
8 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
9 eqid 
 |-  ( Id ` (/) ) = ( Id ` (/) )
10 eqid 
 |-  ( Id ` C ) = ( Id ` C )
11 eqid 
 |-  ( comp ` (/) ) = ( comp ` (/) )
12 eqid 
 |-  ( comp ` C ) = ( comp ` C )
13 0cat 
 |-  (/) e. Cat
14 13 a1i 
 |-  ( ph -> (/) e. Cat )
15 5 6 7 8 9 10 11 12 14 1 isfunc 
 |-  ( ph -> ( f ( (/) Func C ) g <-> ( f : (/) --> ( Base ` C ) /\ g e. X_ z e. ( (/) X. (/) ) ( ( ( f ` ( 1st ` z ) ) ( Hom ` C ) ( f ` ( 2nd ` z ) ) ) ^m ( ( Hom ` (/) ) ` z ) ) /\ A. x e. (/) ( ( ( x g x ) ` ( ( Id ` (/) ) ` x ) ) = ( ( Id ` C ) ` ( f ` x ) ) /\ A. y e. (/) A. z e. (/) A. m e. ( x ( Hom ` (/) ) y ) A. n e. ( y ( Hom ` (/) ) z ) ( ( x g z ) ` ( n ( <. x , y >. ( comp ` (/) ) z ) m ) ) = ( ( ( y g z ) ` n ) ( <. ( f ` x ) , ( f ` y ) >. ( comp ` C ) ( f ` z ) ) ( ( x g y ) ` m ) ) ) ) ) )
16 f0bi 
 |-  ( f : (/) --> ( Base ` C ) <-> f = (/) )
17 ral0 
 |-  A. x e. (/) A. y e. (/) ( x g y ) : ( x ( Hom ` (/) ) y ) --> ( ( f ` x ) ( Hom ` C ) ( f ` y ) )
18 5 funcf2lem2 
 |-  ( g e. X_ z e. ( (/) X. (/) ) ( ( ( f ` ( 1st ` z ) ) ( Hom ` C ) ( f ` ( 2nd ` z ) ) ) ^m ( ( Hom ` (/) ) ` z ) ) <-> ( g Fn ( (/) X. (/) ) /\ A. x e. (/) A. y e. (/) ( x g y ) : ( x ( Hom ` (/) ) y ) --> ( ( f ` x ) ( Hom ` C ) ( f ` y ) ) ) )
19 17 18 mpbiran2 
 |-  ( g e. X_ z e. ( (/) X. (/) ) ( ( ( f ` ( 1st ` z ) ) ( Hom ` C ) ( f ` ( 2nd ` z ) ) ) ^m ( ( Hom ` (/) ) ` z ) ) <-> g Fn ( (/) X. (/) ) )
20 0xp 
 |-  ( (/) X. (/) ) = (/)
21 20 fneq2i 
 |-  ( g Fn ( (/) X. (/) ) <-> g Fn (/) )
22 fn0 
 |-  ( g Fn (/) <-> g = (/) )
23 19 21 22 3bitri 
 |-  ( g e. X_ z e. ( (/) X. (/) ) ( ( ( f ` ( 1st ` z ) ) ( Hom ` C ) ( f ` ( 2nd ` z ) ) ) ^m ( ( Hom ` (/) ) ` z ) ) <-> g = (/) )
24 ral0 
 |-  A. x e. (/) ( ( ( x g x ) ` ( ( Id ` (/) ) ` x ) ) = ( ( Id ` C ) ` ( f ` x ) ) /\ A. y e. (/) A. z e. (/) A. m e. ( x ( Hom ` (/) ) y ) A. n e. ( y ( Hom ` (/) ) z ) ( ( x g z ) ` ( n ( <. x , y >. ( comp ` (/) ) z ) m ) ) = ( ( ( y g z ) ` n ) ( <. ( f ` x ) , ( f ` y ) >. ( comp ` C ) ( f ` z ) ) ( ( x g y ) ` m ) ) )
25 15 16 23 24 0funclem 
 |-  ( ph -> ( f ( (/) Func C ) g <-> ( f = (/) /\ g = (/) ) ) )
26 brsnop 
 |-  ( ( (/) e. _V /\ (/) e. _V ) -> ( f { <. (/) , (/) >. } g <-> ( f = (/) /\ g = (/) ) ) )
27 3 3 26 mp2an 
 |-  ( f { <. (/) , (/) >. } g <-> ( f = (/) /\ g = (/) ) )
28 25 27 bitr4di 
 |-  ( ph -> ( f ( (/) Func C ) g <-> f { <. (/) , (/) >. } g ) )
29 2 4 28 eqbrrdiv 
 |-  ( ph -> ( (/) Func C ) = { <. (/) , (/) >. } )