This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem zeroofn

Description: ZeroO is a function on Cat . (Contributed by Zhi Wang, 29-Aug-2024)

		Ref	Expression
	Assertion	zeroofn	$⊢ ZeroO Fn Cat$

Step	Hyp	Ref	Expression
1		fvex	$⊢ InitO (c) \in V$
2	1	inex1	$⊢ InitO (c) \cap TermO (c) \in V$
3		df-zeroo	$⊢ ZeroO = (c \in Cat ⟼ InitO (c) \cap TermO (c))$
4	2 3	fnmpti	$⊢ ZeroO Fn Cat$