Theorem zerooval

Description: The value of the zero object function, i.e. the set of all zero objects of a category. (Contributed by AV, 3-Apr-2020)

	Ref	Expression
Hypotheses	initoval.c	|- ( ph -> C e. Cat )
	initoval.b	|- B = ( Base ` C )
	initoval.h	|- H = ( Hom ` C )
Assertion	zerooval	|- ( ph -> ( ZeroO ` C ) = ( ( InitO ` C ) i^i ( TermO ` C ) ) )

Proof

Step	Hyp	Ref	Expression
1		initoval.c	|- ( ph -> C e. Cat )
2		initoval.b	|- B = ( Base ` C )
3		initoval.h	|- H = ( Hom ` C )
4		df-zeroo	|- ZeroO = ( c e. Cat |-> ( ( InitO ` c ) i^i ( TermO ` c ) ) )
5		fveq2	|- ( c = C -> ( InitO ` c ) = ( InitO ` C ) )
6		fveq2	|- ( c = C -> ( TermO ` c ) = ( TermO ` C ) )
7	5 6	ineq12d	|- ( c = C -> ( ( InitO ` c ) i^i ( TermO ` c ) ) = ( ( InitO ` C ) i^i ( TermO ` C ) ) )
8		fvex	|- ( InitO ` C ) e. _V
9	8	inex1	|- ( ( InitO ` C ) i^i ( TermO ` C ) ) e. _V
10	9	a1i	|- ( ph -> ( ( InitO ` C ) i^i ( TermO ` C ) ) e. _V )
11	4 7 1 10	fvmptd3	|- ( ph -> ( ZeroO ` C ) = ( ( InitO ` C ) i^i ( TermO ` C ) ) )