Metamath Proof Explorer

Theorem termcterm

Description: A terminal category is a terminal object of the category of small categories. (Contributed by Zhi Wang, 17-Oct-2025)

Ref Expression
Hypotheses termcterm.e ⊢ E = CatCat ⁡ U
termcterm.u ⊢ φ → U ∈ V
termcterm.c ⊢ φ → C ∈ U
termcterm.t No typesetting found for |- ( ph -> C e. TermCat ) with typecode |-
Assertion termcterm ⊢ φ → C ∈ TermO ⁡ E

Proof

Step Hyp Ref Expression
1 termcterm.e ⊢ E = CatCat ⁡ U
2 termcterm.u ⊢ φ → U ∈ V
3 termcterm.c ⊢ φ → C ∈ U
4 termcterm.t Could not format ( ph -> C e. TermCat ) : No typesetting found for |- ( ph -> C e. TermCat ) with typecode |-
5 simpr ⊢ φ ∧ d ∈ Base E → d ∈ Base E
6 eqid ⊢ Base E = Base E
7 1 6 2 catcbas ⊢ φ → Base E = U ∩ Cat
8 7 adantr ⊢ φ ∧ d ∈ Base E → Base E = U ∩ Cat
9 5 8 eleqtrd ⊢ φ ∧ d ∈ Base E → d ∈ U ∩ Cat
10 9 elin2d ⊢ φ ∧ d ∈ Base E → d ∈ Cat
11 4 adantr Could not format ( ( ph /\ d e. ( Base ` E ) ) -> C e. TermCat ) : No typesetting found for |- ( ( ph /\ d e. ( Base ` E ) ) -> C e. TermCat ) with typecode |-
12 10 11 functermceu ⊢ φ ∧ d ∈ Base E → ∃! f f ∈ d Func C
13 2 adantr ⊢ φ ∧ d ∈ Base E → U ∈ V
14 eqid ⊢ Hom ⁡ E = Hom ⁡ E
15 4 termccatd ⊢ φ → C ∈ Cat
16 3 15 elind ⊢ φ → C ∈ U ∩ Cat
17 16 7 eleqtrrd ⊢ φ → C ∈ Base E
18 17 adantr ⊢ φ ∧ d ∈ Base E → C ∈ Base E
19 1 6 13 14 5 18 catchom ⊢ φ ∧ d ∈ Base E → d Hom ⁡ E C = d Func C
20 19 eleq2d ⊢ φ ∧ d ∈ Base E → f ∈ d Hom ⁡ E C ↔ f ∈ d Func C
21 20 eubidv ⊢ φ ∧ d ∈ Base E → ∃! f f ∈ d Hom ⁡ E C ↔ ∃! f f ∈ d Func C
22 12 21 mpbird ⊢ φ ∧ d ∈ Base E → ∃! f f ∈ d Hom ⁡ E C
23 22 ralrimiva ⊢ φ → ∀ d ∈ Base E ∃! f f ∈ d Hom ⁡ E C
24 1 catccat ⊢ U ∈ V → E ∈ Cat
25 2 24 syl ⊢ φ → E ∈ Cat
26 6 14 25 17 istermo ⊢ φ → C ∈ TermO ⁡ E ↔ ∀ d ∈ Base E ∃! f f ∈ d Hom ⁡ E C
27 23 26 mpbird ⊢ φ → C ∈ TermO ⁡ E