This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 0funcg

Description: The functor from the empty category. Corollary of Definition 3.47 of Adamek p. 40, Definition 7.1 of Adamek p. 101, Example 3.3(4.c) of Adamek p. 24, and Example 7.2(3) of Adamek p. 101. (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 0funcg 
|- ( ph -> ( C Func D ) = { <. (/) , (/) >. } )

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 relfunc 
 |-  Rel ( C Func D )
5 0ex 
 |-  (/) e. _V
6 5 5 relsnop 
 |-  Rel { <. (/) , (/) >. }
7 1 2 3 0funcg2 
 |-  ( ph -> ( f ( C Func D ) g <-> ( f = (/) /\ g = (/) ) ) )
8 brsnop 
 |-  ( ( (/) e. _V /\ (/) e. _V ) -> ( f { <. (/) , (/) >. } g <-> ( f = (/) /\ g = (/) ) ) )
9 5 5 8 mp2an 
 |-  ( f { <. (/) , (/) >. } g <-> ( f = (/) /\ g = (/) ) )
10 7 9 bitr4di 
 |-  ( ph -> ( f ( C Func D ) g <-> f { <. (/) , (/) >. } g ) )
11 4 6 10 eqbrrdiv 
 |-  ( ph -> ( C Func D ) = { <. (/) , (/) >. } )