Theorem 0funcg

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	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 ) = { <. (/) , (/) >. } )