This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → 𝐴 = ∅ )