Metamath Proof Explorer

Theorem funcsn

Description: The category of one functor to a thin category is terminal. (Contributed by Zhi Wang, 17-Nov-2025)

Ref Expression
Hypotheses funcsn.q ⊢ Q = C FuncCat D
funcsn.f ⊢ φ → F ∈ V
funcsn.c ⊢ φ → C Func D = F
funcsn.d ⊢ φ → D ∈ ThinCat
Assertion funcsn Could not format assertion : No typesetting found for |- ( ph -> Q e. TermCat ) with typecode |-

Proof

Step Hyp Ref Expression
1 funcsn.q ⊢ Q = C FuncCat D
2 funcsn.f ⊢ φ → F ∈ V
3 funcsn.c ⊢ φ → C Func D = F
4 funcsn.d ⊢ φ → D ∈ ThinCat
5 1 fucbas ⊢ C Func D = Base Q
6 5 a1i ⊢ φ → C Func D = Base Q
7 eqid ⊢ C Nat D = C Nat D
8 1 7 fuchom ⊢ C Nat D = Hom ⁡ Q
9 8 a1i ⊢ φ → C Nat D = Hom ⁡ Q
10 simprl ⊢ φ ∧ a ∈ f C Nat D g ∧ b ∈ f C Nat D g → a ∈ f C Nat D g
11 7 10 nat1st2nd ⊢ φ ∧ 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 ⊢ φ ∧ a ∈ f C Nat D g ∧ b ∈ f C Nat D g → a Fn Base C
14 simprr ⊢ φ ∧ a ∈ f C Nat D g ∧ b ∈ f C Nat D g → b ∈ f C Nat D g
15 7 14 nat1st2nd ⊢ φ ∧ 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
16 7 15 12 natfn ⊢ φ ∧ a ∈ f C Nat D g ∧ b ∈ f C Nat D g → b Fn Base C
17 eqid ⊢ Base D = Base D
18 7 11 natrcl2 ⊢ φ ∧ a ∈ f C Nat D g ∧ b ∈ f C Nat D g → 1 st ⁡ f C Func D 2 nd ⁡ f
19 12 17 18 funcf1 ⊢ φ ∧ a ∈ f C Nat D g ∧ b ∈ f C Nat D g → 1 st ⁡ f : Base C ⟶ Base D
20 19 ffvelcdmda ⊢ φ ∧ a ∈ f C Nat D g ∧ b ∈ f C Nat D g ∧ x ∈ Base C → 1 st ⁡ f ⁡ x ∈ Base D
21 7 11 natrcl3 ⊢ φ ∧ a ∈ f C Nat D g ∧ b ∈ f C Nat D g → 1 st ⁡ g C Func D 2 nd ⁡ g
22 12 17 21 funcf1 ⊢ φ ∧ a ∈ f C Nat D g ∧ b ∈ f C Nat D g → 1 st ⁡ g : Base C ⟶ Base D
23 22 ffvelcdmda ⊢ φ ∧ a ∈ f C Nat D g ∧ b ∈ f C Nat D g ∧ x ∈ Base C → 1 st ⁡ g ⁡ x ∈ Base D
24 11 adantr ⊢ φ ∧ a ∈ f C Nat D g ∧ b ∈ f C Nat D g ∧ x ∈ Base C → a ∈ 1 st ⁡ f 2 nd ⁡ f C Nat D 1 st ⁡ g 2 nd ⁡ g
25 eqid ⊢ Hom ⁡ D = Hom ⁡ D
26 simpr ⊢ φ ∧ a ∈ f C Nat D g ∧ b ∈ f C Nat D g ∧ x ∈ Base C → x ∈ Base C
27 7 24 12 25 26 natcl ⊢ φ ∧ a ∈ f C Nat D g ∧ b ∈ f C Nat D g ∧ x ∈ Base C → a ⁡ x ∈ 1 st ⁡ f ⁡ x Hom ⁡ D 1 st ⁡ g ⁡ x
28 15 adantr ⊢ φ ∧ a ∈ f C Nat D g ∧ b ∈ f C Nat D g ∧ x ∈ Base C → b ∈ 1 st ⁡ f 2 nd ⁡ f C Nat D 1 st ⁡ g 2 nd ⁡ g
29 7 28 12 25 26 natcl ⊢ φ ∧ a ∈ f C Nat D g ∧ b ∈ f C Nat D g ∧ x ∈ Base C → b ⁡ x ∈ 1 st ⁡ f ⁡ x Hom ⁡ D 1 st ⁡ g ⁡ x
30 4 ad2antrr ⊢ φ ∧ a ∈ f C Nat D g ∧ b ∈ f C Nat D g ∧ x ∈ Base C → D ∈ ThinCat
31 20 23 27 29 17 25 30 thincmo2 ⊢ φ ∧ a ∈ f C Nat D g ∧ b ∈ f C Nat D g ∧ x ∈ Base C → a ⁡ x = b ⁡ x
32 13 16 31 eqfnfvd ⊢ φ ∧ a ∈ f C Nat D g ∧ b ∈ f C Nat D g → a = b
33 32 ralrimivva ⊢ φ → ∀ a ∈ f C Nat D g ∀ b ∈ f C Nat D g a = b
34 moel ⊢ ∃* a a ∈ f C Nat D g ↔ ∀ a ∈ f C Nat D g ∀ b ∈ f C Nat D g a = b
35 33 34 sylibr ⊢ φ → ∃* a a ∈ f C Nat D g
36 35 adantr ⊢ φ ∧ f ∈ C Func D ∧ g ∈ C Func D → ∃* a a ∈ f C Nat D g
37 snidg ⊢ F ∈ V → F ∈ F
38 2 37 syl ⊢ φ → F ∈ F
39 38 3 eleqtrrd ⊢ φ → F ∈ C Func D
40 39 func1st2nd ⊢ φ → 1 st ⁡ F C Func D 2 nd ⁡ F
41 40 funcrcl2 ⊢ φ → C ∈ Cat
42 4 thinccd ⊢ φ → D ∈ Cat
43 1 41 42 fuccat ⊢ φ → Q ∈ Cat
44 6 9 36 43 isthincd ⊢ φ → Q ∈ ThinCat
45 sneq ⊢ f = F → f = F
46 45 eqeq2d ⊢ f = F → C Func D = f ↔ C Func D = F
47 2 3 46 spcedv ⊢ φ → ∃ f C Func D = f
48 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 |-
49 44 47 48 sylanbrc Could not format ( ph -> Q e. TermCat ) : No typesetting found for |- ( ph -> Q e. TermCat ) with typecode |-