Theorem func0g2

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 = (/) )
	func0g2.f	|- ( ph -> F e. ( C Func D ) )
Assertion	func0g2	|- ( 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		func0g2.f	|- ( ph -> F e. ( C Func D ) )
5	4	func1st2nd	|- ( ph -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
6	1 2 3 5	func0g	|- ( ph -> A = (/) )