Metamath Proof Explorer

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 ⊢φ→C∈Cat
initoval.b ⊢B=BaseC
initoval.h ⊢H=Hom⁡C
Assertion zerooval ⊢φ→ZeroO⁡C=InitO⁡C∩TermO⁡C

Proof

Step Hyp Ref Expression
1 initoval.c ⊢φ→C∈Cat
2 initoval.b ⊢B=BaseC
3 initoval.h ⊢H=Hom⁡C
4 df-zeroo ⊢ZeroO=c∈Cat⟼InitO⁡c∩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∩TermO⁡c=InitO⁡C∩TermO⁡C
8 fvex ⊢InitO⁡C∈V
9 8 inex1 ⊢InitO⁡C∩TermO⁡C∈V
10 9 a1i ⊢φ→InitO⁡C∩TermO⁡C∈V
11 4 7 1 10 fvmptd3 ⊢φ→ZeroO⁡C=InitO⁡C∩TermO⁡C