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

Proof

Step	Hyp	Ref	Expression
1		func0g.a	⊢ 𝐴 = ( Base ‘ 𝐶 )
2		func0g.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
3		func0g.d	⊢ ( 𝜑 → 𝐵 = ∅ )
4		func0g2.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
5	4	func1st2nd	⊢ ( 𝜑 → ( 1st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2nd ‘ 𝐹 ) )
6	1 2 3 5	func0g	⊢ ( 𝜑 → 𝐴 = ∅ )