Metamath Proof Explorer

Theorem 0funcg

Description: The functor from the empty category. (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 = ∅ ∅