Theorem func0g

Description: The source category of a functor to the empty category must be empty as well. (Contributed by Zhi Wang, 19-Oct-2025)

	Ref	Expression
Hypotheses	func0g.a	$$⊢A={\mathrm{Base}}_C$$
	func0g.b	$$⊢B={\mathrm{Base}}_D$$
	func0g.d	$$⊢\phi \to B=\varnothing$$
	func0g.f	$$⊢\phi \to F\left(C\mathrm{Func}D\right)G$$
Assertion	func0g	$$⊢\phi \to A=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		func0g.a	$$⊢A={\mathrm{Base}}_C$$
2		func0g.b	$$⊢B={\mathrm{Base}}_D$$
3		func0g.d	$$⊢\phi \to B=\varnothing$$
4		func0g.f	$$⊢\phi \to F\left(C\mathrm{Func}D\right)G$$
5	1 2 4	funcf1	$$⊢\phi \to F:A⟶B$$
6	5	f002	$$⊢\phi \to \left(B=\varnothing \to A=\varnothing \right)$$
7	3 6	mpd	$$⊢\phi \to A=\varnothing$$