Theorem 0func

Description: The functor from the empty category. (Contributed by Zhi Wang, 7-Oct-2025) (Proof shortened by Zhi Wang, 17-Oct-2025)

	Ref	Expression
Hypothesis	0func.c	$$⊢\phi \to C\in \mathrm{Cat}$$
Assertion	0func	$$⊢\phi \to \varnothing \mathrm{Func}C=\left\{⟨\varnothing ,\varnothing ⟩\right\}$$

Proof

Step	Hyp	Ref	Expression
1		0func.c	$$⊢\phi \to C\in \mathrm{Cat}$$
2		0ex	$$⊢\varnothing \in \mathrm{V}$$
3	2	a1i	$$⊢\phi \to \varnothing \in \mathrm{V}$$
4		base0	$$⊢\varnothing ={\mathrm{Base}}_{\varnothing }$$
5	4	a1i	$$⊢\phi \to \varnothing ={\mathrm{Base}}_{\varnothing }$$
6	3 5 1	0funcg	$$⊢\phi \to \varnothing \mathrm{Func}C=\left\{⟨\varnothing ,\varnothing ⟩\right\}$$