Theorem func0g2

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$$
	func0g2.f	$$⊢\phi \to F\in \left(C\mathrm{Func}D\right)$$
Assertion	func0g2	$$⊢\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		func0g2.f	$$⊢\phi \to F\in \left(C\mathrm{Func}D\right)$$
5	4	func1st2nd	$$⊢\phi \to 1^{st}\left(F\right)\left(C\mathrm{Func}D\right)2^{nd}\left(F\right)$$
6	1 2 3 5	func0g	$$⊢\phi \to A=\varnothing$$