Metamath Proof Explorer

Theorem termc2

Description: If there exists a unique functor from both the category itself and the trivial category, then the category is terminal. Note that the converse also holds, so that it is a biconditional. See the proof of termc for hints. See also eufunc and euendfunc2 for some insights on why two categories are sufficient. (Contributed by Zhi Wang, 18-Oct-2025) (Proof shortened by Zhi Wang, 20-Oct-2025)

Ref Expression
Assertion termc2 Could not format assertion : No typesetting found for |- ( A. d e. ( { C , ( SetCat ` 1o ) } i^i Cat ) E! f f e. ( d Func C ) -> C e. TermCat ) with typecode |-

Proof

Step Hyp Ref Expression
1 eqid ⊢ CatCat ⁡ C SetCat ⁡ 1 𝑜 = CatCat ⁡ C SetCat ⁡ 1 𝑜
2 fvex ⊢ SetCat ⁡ 1 𝑜 ∈ V
3 2 prid2 ⊢ SetCat ⁡ 1 𝑜 ∈ C SetCat ⁡ 1 𝑜
4 setc1oterm Could not format ( SetCat ` 1o ) e. TermCat : No typesetting found for |- ( SetCat ` 1o ) e. TermCat with typecode |-
5 3 4 elini Could not format ( SetCat ` 1o ) e. ( { C , ( SetCat ` 1o ) } i^i TermCat ) : No typesetting found for |- ( SetCat ` 1o ) e. ( { C , ( SetCat ` 1o ) } i^i TermCat ) with typecode |-
6 5 ne0ii Could not format ( { C , ( SetCat ` 1o ) } i^i TermCat ) =/= (/) : No typesetting found for |- ( { C , ( SetCat ` 1o ) } i^i TermCat ) =/= (/) with typecode |-
7 6 a1i Could not format ( A. d e. ( { C , ( SetCat ` 1o ) } i^i Cat ) E! f f e. ( d Func C ) -> ( { C , ( SetCat ` 1o ) } i^i TermCat ) =/= (/) ) : No typesetting found for |- ( A. d e. ( { C , ( SetCat ` 1o ) } i^i Cat ) E! f f e. ( d Func C ) -> ( { C , ( SetCat ` 1o ) } i^i TermCat ) =/= (/) ) with typecode |-
8 4 a1i Could not format ( T. -> ( SetCat ` 1o ) e. TermCat ) : No typesetting found for |- ( T. -> ( SetCat ` 1o ) e. TermCat ) with typecode |-
9 8 termccd ⊢ ⊤ → SetCat ⁡ 1 𝑜 ∈ Cat
10 9 mptru ⊢ SetCat ⁡ 1 𝑜 ∈ Cat
11 3 10 elini ⊢ SetCat ⁡ 1 𝑜 ∈ C SetCat ⁡ 1 𝑜 ∩ Cat
12 oveq1 ⊢ d = SetCat ⁡ 1 𝑜 → d Func C = SetCat ⁡ 1 𝑜 Func C
13 12 eleq2d ⊢ d = SetCat ⁡ 1 𝑜 → f ∈ d Func C ↔ f ∈ SetCat ⁡ 1 𝑜 Func C
14 13 eubidv ⊢ d = SetCat ⁡ 1 𝑜 → ∃! f f ∈ d Func C ↔ ∃! f f ∈ SetCat ⁡ 1 𝑜 Func C
15 14 rspcv ⊢ SetCat ⁡ 1 𝑜 ∈ C SetCat ⁡ 1 𝑜 ∩ Cat → ∀ d ∈ C SetCat ⁡ 1 𝑜 ∩ Cat ∃! f f ∈ d Func C → ∃! f f ∈ SetCat ⁡ 1 𝑜 Func C
16 11 15 ax-mp ⊢ ∀ d ∈ C SetCat ⁡ 1 𝑜 ∩ Cat ∃! f f ∈ d Func C → ∃! f f ∈ SetCat ⁡ 1 𝑜 Func C
17 euen1b ⊢ SetCat ⁡ 1 𝑜 Func C ≈ 1 𝑜 ↔ ∃! f f ∈ SetCat ⁡ 1 𝑜 Func C
18 16 17 sylibr ⊢ ∀ d ∈ C SetCat ⁡ 1 𝑜 ∩ Cat ∃! f f ∈ d Func C → SetCat ⁡ 1 𝑜 Func C ≈ 1 𝑜
19 eqid ⊢ Base CatCat ⁡ C SetCat ⁡ 1 𝑜 = Base CatCat ⁡ C SetCat ⁡ 1 𝑜
20 prex ⊢ C SetCat ⁡ 1 𝑜 ∈ V
21 20 a1i ⊢ ⊤ → C SetCat ⁡ 1 𝑜 ∈ V
22 1 19 21 catcbas ⊢ ⊤ → Base CatCat ⁡ C SetCat ⁡ 1 𝑜 = C SetCat ⁡ 1 𝑜 ∩ Cat
23 22 mptru ⊢ Base CatCat ⁡ C SetCat ⁡ 1 𝑜 = C SetCat ⁡ 1 𝑜 ∩ Cat
24 23 eqcomi ⊢ C SetCat ⁡ 1 𝑜 ∩ Cat = Base CatCat ⁡ C SetCat ⁡ 1 𝑜
25 eqid ⊢ Hom ⁡ CatCat ⁡ C SetCat ⁡ 1 𝑜 = Hom ⁡ CatCat ⁡ C SetCat ⁡ 1 𝑜
26 1 catccat ⊢ C SetCat ⁡ 1 𝑜 ∈ V → CatCat ⁡ C SetCat ⁡ 1 𝑜 ∈ Cat
27 20 26 ax-mp ⊢ CatCat ⁡ C SetCat ⁡ 1 𝑜 ∈ Cat
28 27 a1i ⊢ SetCat ⁡ 1 𝑜 Func C ≈ 1 𝑜 → CatCat ⁡ C SetCat ⁡ 1 𝑜 ∈ Cat
29 euex ⊢ ∃! f f ∈ SetCat ⁡ 1 𝑜 Func C → ∃ f f ∈ SetCat ⁡ 1 𝑜 Func C
30 funcrcl ⊢ f ∈ SetCat ⁡ 1 𝑜 Func C → SetCat ⁡ 1 𝑜 ∈ Cat ∧ C ∈ Cat
31 30 simprd ⊢ f ∈ SetCat ⁡ 1 𝑜 Func C → C ∈ Cat
32 31 exlimiv ⊢ ∃ f f ∈ SetCat ⁡ 1 𝑜 Func C → C ∈ Cat
33 29 32 syl ⊢ ∃! f f ∈ SetCat ⁡ 1 𝑜 Func C → C ∈ Cat
34 17 33 sylbi ⊢ SetCat ⁡ 1 𝑜 Func C ≈ 1 𝑜 → C ∈ Cat
35 prid1g ⊢ C ∈ Cat → C ∈ C SetCat ⁡ 1 𝑜
36 34 35 syl ⊢ SetCat ⁡ 1 𝑜 Func C ≈ 1 𝑜 → C ∈ C SetCat ⁡ 1 𝑜
37 36 34 elind ⊢ SetCat ⁡ 1 𝑜 Func C ≈ 1 𝑜 → C ∈ C SetCat ⁡ 1 𝑜 ∩ Cat
38 24 25 28 37 istermo ⊢ SetCat ⁡ 1 𝑜 Func C ≈ 1 𝑜 → C ∈ TermO ⁡ CatCat ⁡ C SetCat ⁡ 1 𝑜 ↔ ∀ d ∈ C SetCat ⁡ 1 𝑜 ∩ Cat ∃! f f ∈ d Hom ⁡ CatCat ⁡ C SetCat ⁡ 1 𝑜 C
39 20 a1i ⊢ SetCat ⁡ 1 𝑜 Func C ≈ 1 𝑜 ∧ d ∈ C SetCat ⁡ 1 𝑜 ∩ Cat → C SetCat ⁡ 1 𝑜 ∈ V
40 simpr ⊢ SetCat ⁡ 1 𝑜 Func C ≈ 1 𝑜 ∧ d ∈ C SetCat ⁡ 1 𝑜 ∩ Cat → d ∈ C SetCat ⁡ 1 𝑜 ∩ Cat
41 37 adantr ⊢ SetCat ⁡ 1 𝑜 Func C ≈ 1 𝑜 ∧ d ∈ C SetCat ⁡ 1 𝑜 ∩ Cat → C ∈ C SetCat ⁡ 1 𝑜 ∩ Cat
42 1 24 39 25 40 41 catchom ⊢ SetCat ⁡ 1 𝑜 Func C ≈ 1 𝑜 ∧ d ∈ C SetCat ⁡ 1 𝑜 ∩ Cat → d Hom ⁡ CatCat ⁡ C SetCat ⁡ 1 𝑜 C = d Func C
43 42 eleq2d ⊢ SetCat ⁡ 1 𝑜 Func C ≈ 1 𝑜 ∧ d ∈ C SetCat ⁡ 1 𝑜 ∩ Cat → f ∈ d Hom ⁡ CatCat ⁡ C SetCat ⁡ 1 𝑜 C ↔ f ∈ d Func C
44 43 eubidv ⊢ SetCat ⁡ 1 𝑜 Func C ≈ 1 𝑜 ∧ d ∈ C SetCat ⁡ 1 𝑜 ∩ Cat → ∃! f f ∈ d Hom ⁡ CatCat ⁡ C SetCat ⁡ 1 𝑜 C ↔ ∃! f f ∈ d Func C
45 44 ralbidva ⊢ SetCat ⁡ 1 𝑜 Func C ≈ 1 𝑜 → ∀ d ∈ C SetCat ⁡ 1 𝑜 ∩ Cat ∃! f f ∈ d Hom ⁡ CatCat ⁡ C SetCat ⁡ 1 𝑜 C ↔ ∀ d ∈ C SetCat ⁡ 1 𝑜 ∩ Cat ∃! f f ∈ d Func C
46 38 45 bitrd ⊢ SetCat ⁡ 1 𝑜 Func C ≈ 1 𝑜 → C ∈ TermO ⁡ CatCat ⁡ C SetCat ⁡ 1 𝑜 ↔ ∀ d ∈ C SetCat ⁡ 1 𝑜 ∩ Cat ∃! f f ∈ d Func C
47 18 46 syl ⊢ ∀ d ∈ C SetCat ⁡ 1 𝑜 ∩ Cat ∃! f f ∈ d Func C → C ∈ TermO ⁡ CatCat ⁡ C SetCat ⁡ 1 𝑜 ↔ ∀ d ∈ C SetCat ⁡ 1 𝑜 ∩ Cat ∃! f f ∈ d Func C
48 47 ibir ⊢ ∀ d ∈ C SetCat ⁡ 1 𝑜 ∩ Cat ∃! f f ∈ d Func C → C ∈ TermO ⁡ CatCat ⁡ C SetCat ⁡ 1 𝑜
49 1 7 48 termcterm2 Could not format ( A. d e. ( { C , ( SetCat ` 1o ) } i^i Cat ) E! f f e. ( d Func C ) -> C e. TermCat ) : No typesetting found for |- ( A. d e. ( { C , ( SetCat ` 1o ) } i^i Cat ) E! f f e. ( d Func C ) -> C e. TermCat ) with typecode |-