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

Proof

Step Hyp Ref Expression
1 func0g.a ⊢ A = Base C
2 func0g.b ⊢ B = Base D
3 func0g.d ⊢ φ → B = ∅
4 func0g2.f ⊢ φ → F ∈ C Func D
5 4 func1st2nd ⊢ φ → 1 st ⁡ F C Func D 2 nd ⁡ F
6 1 2 3 5 func0g ⊢ φ → A = ∅