Theorem zeroofn

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

	Ref	Expression
Assertion	zeroofn	$$⊢\mathrm{ZeroO}Fn\mathrm{Cat}$$

Proof

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