Metamath Proof Explorer

Theorem 0func

Description: The functor from the empty category. (Contributed by Zhi Wang, 7-Oct-2025)

Ref Expression
Hypothesis 0func.c ⊢ φ → C ∈ Cat
Assertion 0func ⊢ φ → ∅ Func C = ∅ ∅

Proof

Step Hyp Ref Expression
1 0func.c ⊢ φ → C ∈ Cat
2 relfunc ⊢ Rel ⁡ ∅ Func C
3 0ex ⊢ ∅ ∈ V
4 3 3 relsnop ⊢ Rel ⁡ ∅ ∅
5 base0 ⊢ ∅ = Base ∅
6 eqid ⊢ Base C = Base C
7 eqid ⊢ Hom ⁡ ∅ = Hom ⁡ ∅
8 eqid ⊢ Hom ⁡ C = Hom ⁡ C
9 eqid ⊢ Id ⁡ ∅ = Id ⁡ ∅
10 eqid ⊢ Id ⁡ C = Id ⁡ C
11 eqid ⊢ comp ⁡ ∅ = comp ⁡ ∅
12 eqid ⊢ comp ⁡ C = comp ⁡ C
13 0cat ⊢ ∅ ∈ Cat
14 13 a1i ⊢ φ → ∅ ∈ Cat
15 5 6 7 8 9 10 11 12 14 1 isfunc ⊢ φ → f ∅ Func C g ↔ f : ∅ ⟶ Base C ∧ g ∈ ⨉ z ∈ ∅ × ∅ f ⁡ 1 st ⁡ z Hom ⁡ C f ⁡ 2 nd ⁡ z Hom ⁡ ∅ ⁡ z ∧ ∀ x ∈ ∅ x g x ⁡ Id ⁡ ∅ ⁡ x = Id ⁡ C ⁡ f ⁡ x ∧ ∀ y ∈ ∅ ∀ z ∈ ∅ ∀ m ∈ x Hom ⁡ ∅ y ∀ n ∈ y Hom ⁡ ∅ z x g z ⁡ n x y comp ⁡ ∅ z m = y g z ⁡ n f ⁡ x f ⁡ y comp ⁡ C f ⁡ z x g y ⁡ m
16 f0bi ⊢ f : ∅ ⟶ Base C ↔ f = ∅
17 ral0 ⊢ ∀ x ∈ ∅ ∀ y ∈ ∅ x g y : x Hom ⁡ ∅ y ⟶ f ⁡ x Hom ⁡ C f ⁡ y
18 5 funcf2lem2 ⊢ g ∈ ⨉ z ∈ ∅ × ∅ f ⁡ 1 st ⁡ z Hom ⁡ C f ⁡ 2 nd ⁡ z Hom ⁡ ∅ ⁡ z ↔ g Fn ∅ × ∅ ∧ ∀ x ∈ ∅ ∀ y ∈ ∅ x g y : x Hom ⁡ ∅ y ⟶ f ⁡ x Hom ⁡ C f ⁡ y
19 17 18 mpbiran2 ⊢ g ∈ ⨉ z ∈ ∅ × ∅ f ⁡ 1 st ⁡ z Hom ⁡ C f ⁡ 2 nd ⁡ z Hom ⁡ ∅ ⁡ z ↔ g Fn ∅ × ∅
20 0xp ⊢ ∅ × ∅ = ∅
21 20 fneq2i ⊢ g Fn ∅ × ∅ ↔ g Fn ∅
22 fn0 ⊢ g Fn ∅ ↔ g = ∅
23 19 21 22 3bitri ⊢ g ∈ ⨉ z ∈ ∅ × ∅ f ⁡ 1 st ⁡ z Hom ⁡ C f ⁡ 2 nd ⁡ z Hom ⁡ ∅ ⁡ z ↔ g = ∅
24 ral0 ⊢ ∀ x ∈ ∅ x g x ⁡ Id ⁡ ∅ ⁡ x = Id ⁡ C ⁡ f ⁡ x ∧ ∀ y ∈ ∅ ∀ z ∈ ∅ ∀ m ∈ x Hom ⁡ ∅ y ∀ n ∈ y Hom ⁡ ∅ z x g z ⁡ n x y comp ⁡ ∅ z m = y g z ⁡ n f ⁡ x f ⁡ y comp ⁡ C f ⁡ z x g y ⁡ m
25 15 16 23 24 0funclem ⊢ φ → f ∅ Func C g ↔ f = ∅ ∧ g = ∅
26 brsnop ⊢ ∅ ∈ V ∧ ∅ ∈ V → f ∅ ∅ g ↔ f = ∅ ∧ g = ∅
27 3 3 26 mp2an ⊢ f ∅ ∅ g ↔ f = ∅ ∧ g = ∅
28 25 27 bitr4di ⊢ φ → f ∅ Func C g ↔ f ∅ ∅ g
29 2 4 28 eqbrrdiv ⊢ φ → ∅ Func C = ∅ ∅