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	⊢ 𝐴 = ( Base ‘ 𝐶 )
	func0g.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
	func0g.d	⊢ ( 𝜑 → 𝐵 = ∅ )
	func0g.f	⊢ ( 𝜑 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
Assertion	func0g	⊢ ( 𝜑 → 𝐴 = ∅ )

Proof

Step	Hyp	Ref	Expression
1		func0g.a	⊢ 𝐴 = ( Base ‘ 𝐶 )
2		func0g.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
3		func0g.d	⊢ ( 𝜑 → 𝐵 = ∅ )
4		func0g.f	⊢ ( 𝜑 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
5	1 2 4	funcf1	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
6	5	f002	⊢ ( 𝜑 → ( 𝐵 = ∅ → 𝐴 = ∅ ) )
7	3 6	mpd	⊢ ( 𝜑 → 𝐴 = ∅ )