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 = Base C
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 = Base C
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