Theorem zeroofn

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

	Ref	Expression
Assertion	zeroofn	|- ZeroO Fn Cat

Proof

Step	Hyp	Ref	Expression
1		fvex	|- ( InitO ` c ) e. _V
2	1	inex1	|- ( ( InitO ` c ) i^i ( TermO ` c ) ) e. _V
3		df-zeroo	|- ZeroO = ( c e. Cat |-> ( ( InitO ` c ) i^i ( TermO ` c ) ) )
4	2 3	fnmpti	|- ZeroO Fn Cat