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 ⊢ A = Base C
func0g.b ⊢ B = Base D
func0g.d ⊢ φ → B = ∅
func0g.f ⊢ φ → F C Func D G
Assertion func0g ⊢ φ → A = ∅

Proof

Step Hyp Ref Expression
1 func0g.a ⊢ A = Base C
2 func0g.b ⊢ B = Base D
3 func0g.d ⊢ φ → B = ∅
4 func0g.f ⊢ φ → F C Func D G
5 1 2 4 funcf1 ⊢ φ → F : A ⟶ B
6 5 f002 ⊢ φ → B = ∅ → A = ∅
7 3 6 mpd ⊢ φ → A = ∅