Metamath Proof Explorer

Theorem 0funcg

Description: The functor from the empty category. Corollary of Definition 3.47 of Adamek p. 40, Definition 7.1 of Adamek p. 101, Example 3.3(4.c) of Adamek p. 24, and Example 7.2(3) of Adamek p. 101. (Contributed by Zhi Wang, 17-Oct-2025)

Ref Expression
Hypotheses 0funcg.c ⊢ φ → C ∈ V
0funcg.b ⊢ φ → ∅ = Base C
0funcg.d ⊢ φ → D ∈ Cat
Assertion 0funcg ⊢ φ → C Func D = ∅ ∅

Proof

Step Hyp Ref Expression
1 0funcg.c ⊢ φ → C ∈ V
2 0funcg.b ⊢ φ → ∅ = Base C
3 0funcg.d ⊢ φ → D ∈ Cat
4 relfunc ⊢ Rel ⁡ C Func D
5 0ex ⊢ ∅ ∈ V
6 5 5 relsnop ⊢ Rel ⁡ ∅ ∅
7 1 2 3 0funcg2 ⊢ φ → f C Func D g ↔ f = ∅ ∧ g = ∅
8 brsnop ⊢ ∅ ∈ V ∧ ∅ ∈ V → f ∅ ∅ g ↔ f = ∅ ∧ g = ∅
9 5 5 8 mp2an ⊢ f ∅ ∅ g ↔ f = ∅ ∧ g = ∅
10 7 9 bitr4di ⊢ φ → f C Func D g ↔ f ∅ ∅ g
11 4 6 10 eqbrrdiv ⊢ φ → C Func D = ∅ ∅