Theorem func0g

Description: The source cateogry 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 = ( Base ` C )
	func0g.b	|- B = ( Base ` D )
	func0g.d	|- ( ph -> B = (/) )
	func0g.f	|- ( ph -> F ( C Func D ) G )
Assertion	func0g	|- ( ph -> A = (/) )

Proof

Step	Hyp	Ref	Expression
1		func0g.a	|- A = ( Base ` C )
2		func0g.b	|- B = ( Base ` D )
3		func0g.d	|- ( ph -> B = (/) )
4		func0g.f	|- ( ph -> F ( C Func D ) G )
5	1 2 4	funcf1	|- ( ph -> F : A --> B )
6	5	f002	|- ( ph -> ( B = (/) -> A = (/) ) )
7	3 6	mpd	|- ( ph -> A = (/) )