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	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	initoval.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	initoval.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
Assertion	zerooval	⊢ ( 𝜑 → ( ZeroO ‘ 𝐶 ) = ( ( InitO ‘ 𝐶 ) ∩ ( TermO ‘ 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		initoval.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
2		initoval.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
3		initoval.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
4		df-zeroo	⊢ ZeroO = ( 𝑐 ∈ Cat ↦ ( ( InitO ‘ 𝑐 ) ∩ ( TermO ‘ 𝑐 ) ) )
5		fveq2	⊢ ( 𝑐 = 𝐶 → ( InitO ‘ 𝑐 ) = ( InitO ‘ 𝐶 ) )
6		fveq2	⊢ ( 𝑐 = 𝐶 → ( TermO ‘ 𝑐 ) = ( TermO ‘ 𝐶 ) )
7	5 6	ineq12d	⊢ ( 𝑐 = 𝐶 → ( ( InitO ‘ 𝑐 ) ∩ ( TermO ‘ 𝑐 ) ) = ( ( InitO ‘ 𝐶 ) ∩ ( TermO ‘ 𝐶 ) ) )
8		fvex	⊢ ( InitO ‘ 𝐶 ) ∈ V
9	8	inex1	⊢ ( ( InitO ‘ 𝐶 ) ∩ ( TermO ‘ 𝐶 ) ) ∈ V
10	9	a1i	⊢ ( 𝜑 → ( ( InitO ‘ 𝐶 ) ∩ ( TermO ‘ 𝐶 ) ) ∈ V )
11	4 7 1 10	fvmptd3	⊢ ( 𝜑 → ( ZeroO ‘ 𝐶 ) = ( ( InitO ‘ 𝐶 ) ∩ ( TermO ‘ 𝐶 ) ) )