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 ‘ 𝑐 ) ∈ V
2	1	inex1	⊢ ( ( InitO ‘ 𝑐 ) ∩ ( TermO ‘ 𝑐 ) ) ∈ V
3		df-zeroo	⊢ ZeroO = ( 𝑐 ∈ Cat ↦ ( ( InitO ‘ 𝑐 ) ∩ ( TermO ‘ 𝑐 ) ) )
4	2 3	fnmpti	⊢ ZeroO Fn Cat