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

Metamath Proof Explorer

Theorem func0g

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