Metamath Proof Explorer

Theorem 0fucterm

Description: The category of functors from an initial category is terminal. (Contributed by Zhi Wang, 17-Nov-2025)

Ref Expression
Hypotheses 0fucterm.c ⊢ φ → C ∈ V
0fucterm.b ⊢ φ → ∅ = Base C
0fucterm.d ⊢ φ → D ∈ Cat
0fucterm.q ⊢ Q = C FuncCat D
Assertion 0fucterm Could not format assertion : No typesetting found for |- ( ph -> Q e. TermCat ) with typecode |-

Proof

Step Hyp Ref Expression
1 0fucterm.c ⊢ φ → C ∈ V
2 0fucterm.b ⊢ φ → ∅ = Base C
3 0fucterm.d ⊢ φ → D ∈ Cat
4 0fucterm.q ⊢ Q = C FuncCat D
5 4 fucbas ⊢ C Func D = Base Q
6 5 a1i ⊢ φ → C Func D = Base Q
7 eqid ⊢ C Nat D = C Nat D
8 4 7 fuchom ⊢ C Nat D = Hom ⁡ Q
9 8 a1i ⊢ φ → C Nat D = Hom ⁡ Q
10 simprl ⊢ φ ∧ f ∈ C Func D ∧ g ∈ C Func D ∧ a ∈ f C Nat D g ∧ b ∈ f C Nat D g → a ∈ f C Nat D g
11 7 10 nat1st2nd ⊢ φ ∧ f ∈ C Func D ∧ g ∈ C Func D ∧ a ∈ f C Nat D g ∧ b ∈ f C Nat D g → a ∈ 1 st ⁡ f 2 nd ⁡ f C Nat D 1 st ⁡ g 2 nd ⁡ g
12 eqid ⊢ Base C = Base C
13 7 11 12 natfn ⊢ φ ∧ f ∈ C Func D ∧ g ∈ C Func D ∧ a ∈ f C Nat D g ∧ b ∈ f C Nat D g → a Fn Base C
14 2 ad2antrr ⊢ φ ∧ f ∈ C Func D ∧ g ∈ C Func D ∧ a ∈ f C Nat D g ∧ b ∈ f C Nat D g → ∅ = Base C
15 14 fneq2d ⊢ φ ∧ f ∈ C Func D ∧ g ∈ C Func D ∧ a ∈ f C Nat D g ∧ b ∈ f C Nat D g → a Fn ∅ ↔ a Fn Base C
16 13 15 mpbird ⊢ φ ∧ f ∈ C Func D ∧ g ∈ C Func D ∧ a ∈ f C Nat D g ∧ b ∈ f C Nat D g → a Fn ∅
17 fn0 ⊢ a Fn ∅ ↔ a = ∅
18 16 17 sylib ⊢ φ ∧ f ∈ C Func D ∧ g ∈ C Func D ∧ a ∈ f C Nat D g ∧ b ∈ f C Nat D g → a = ∅
19 simprr ⊢ φ ∧ f ∈ C Func D ∧ g ∈ C Func D ∧ a ∈ f C Nat D g ∧ b ∈ f C Nat D g → b ∈ f C Nat D g
20 7 19 nat1st2nd ⊢ φ ∧ f ∈ C Func D ∧ g ∈ C Func D ∧ a ∈ f C Nat D g ∧ b ∈ f C Nat D g → b ∈ 1 st ⁡ f 2 nd ⁡ f C Nat D 1 st ⁡ g 2 nd ⁡ g
21 7 20 12 natfn ⊢ φ ∧ f ∈ C Func D ∧ g ∈ C Func D ∧ a ∈ f C Nat D g ∧ b ∈ f C Nat D g → b Fn Base C
22 14 fneq2d ⊢ φ ∧ f ∈ C Func D ∧ g ∈ C Func D ∧ a ∈ f C Nat D g ∧ b ∈ f C Nat D g → b Fn ∅ ↔ b Fn Base C
23 21 22 mpbird ⊢ φ ∧ f ∈ C Func D ∧ g ∈ C Func D ∧ a ∈ f C Nat D g ∧ b ∈ f C Nat D g → b Fn ∅
24 fn0 ⊢ b Fn ∅ ↔ b = ∅
25 23 24 sylib ⊢ φ ∧ f ∈ C Func D ∧ g ∈ C Func D ∧ a ∈ f C Nat D g ∧ b ∈ f C Nat D g → b = ∅
26 18 25 eqtr4d ⊢ φ ∧ f ∈ C Func D ∧ g ∈ C Func D ∧ a ∈ f C Nat D g ∧ b ∈ f C Nat D g → a = b
27 26 ralrimivva ⊢ φ ∧ f ∈ C Func D ∧ g ∈ C Func D → ∀ a ∈ f C Nat D g ∀ b ∈ f C Nat D g a = b
28 moel ⊢ ∃* a a ∈ f C Nat D g ↔ ∀ a ∈ f C Nat D g ∀ b ∈ f C Nat D g a = b
29 27 28 sylibr ⊢ φ ∧ f ∈ C Func D ∧ g ∈ C Func D → ∃* a a ∈ f C Nat D g
30 0catg ⊢ C ∈ V ∧ ∅ = Base C → C ∈ Cat
31 1 2 30 syl2anc ⊢ φ → C ∈ Cat
32 4 31 3 fuccat ⊢ φ → Q ∈ Cat
33 6 9 29 32 isthincd ⊢ φ → Q ∈ ThinCat
34 opex ⊢ ∅ ∅ ∈ V
35 34 a1i ⊢ φ → ∅ ∅ ∈ V
36 1 2 3 0funcg ⊢ φ → C Func D = ∅ ∅
37 sneq ⊢ f = ∅ ∅ → f = ∅ ∅
38 37 eqeq2d ⊢ f = ∅ ∅ → C Func D = f ↔ C Func D = ∅ ∅
39 35 36 38 spcedv ⊢ φ → ∃ f C Func D = f
40 5 istermc Could not format ( Q e. TermCat <-> ( Q e. ThinCat /\ E. f ( C Func D ) = { f } ) ) : No typesetting found for |- ( Q e. TermCat <-> ( Q e. ThinCat /\ E. f ( C Func D ) = { f } ) ) with typecode |-
41 33 39 40 sylanbrc Could not format ( ph -> Q e. TermCat ) : No typesetting found for |- ( ph -> Q e. TermCat ) with typecode |-