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. (Contributed by Zhi Wang, 18-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 relfunc ⊢ Rel ⁡ SetCat ⁡ 1 𝑜 Func C
31 1st2ndbr ⊢ Rel ⁡ SetCat ⁡ 1 𝑜 Func C ∧ f ∈ SetCat ⁡ 1 𝑜 Func C → 1 st ⁡ f SetCat ⁡ 1 𝑜 Func C 2 nd ⁡ f
32 30 31 mpan ⊢ f ∈ SetCat ⁡ 1 𝑜 Func C → 1 st ⁡ f SetCat ⁡ 1 𝑜 Func C 2 nd ⁡ f
33 32 funcrcl3 ⊢ f ∈ SetCat ⁡ 1 𝑜 Func C → C ∈ Cat
34 33 exlimiv ⊢ ∃ f f ∈ SetCat ⁡ 1 𝑜 Func C → C ∈ Cat
35 29 34 syl ⊢ ∃! f f ∈ SetCat ⁡ 1 𝑜 Func C → C ∈ Cat
36 17 35 sylbi ⊢ SetCat ⁡ 1 𝑜 Func C ≈ 1 𝑜 → C ∈ Cat
37 prid1g ⊢ C ∈ Cat → C ∈ C SetCat ⁡ 1 𝑜
38 36 37 syl ⊢ SetCat ⁡ 1 𝑜 Func C ≈ 1 𝑜 → C ∈ C SetCat ⁡ 1 𝑜
39 38 36 elind ⊢ SetCat ⁡ 1 𝑜 Func C ≈ 1 𝑜 → C ∈ C SetCat ⁡ 1 𝑜 ∩ Cat
40 24 25 28 39 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
41 20 a1i ⊢ SetCat ⁡ 1 𝑜 Func C ≈ 1 𝑜 ∧ d ∈ C SetCat ⁡ 1 𝑜 ∩ Cat → C SetCat ⁡ 1 𝑜 ∈ V
42 simpr ⊢ SetCat ⁡ 1 𝑜 Func C ≈ 1 𝑜 ∧ d ∈ C SetCat ⁡ 1 𝑜 ∩ Cat → d ∈ C SetCat ⁡ 1 𝑜 ∩ Cat
43 39 adantr ⊢ SetCat ⁡ 1 𝑜 Func C ≈ 1 𝑜 ∧ d ∈ C SetCat ⁡ 1 𝑜 ∩ Cat → C ∈ C SetCat ⁡ 1 𝑜 ∩ Cat
44 1 24 41 25 42 43 catchom ⊢ SetCat ⁡ 1 𝑜 Func C ≈ 1 𝑜 ∧ d ∈ C SetCat ⁡ 1 𝑜 ∩ Cat → d Hom ⁡ CatCat ⁡ C SetCat ⁡ 1 𝑜 C = d Func C
45 44 eleq2d ⊢ SetCat ⁡ 1 𝑜 Func C ≈ 1 𝑜 ∧ d ∈ C SetCat ⁡ 1 𝑜 ∩ Cat → f ∈ d Hom ⁡ CatCat ⁡ C SetCat ⁡ 1 𝑜 C ↔ f ∈ d Func C
46 45 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
47 46 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
48 40 47 bitrd ⊢ SetCat ⁡ 1 𝑜 Func C ≈ 1 𝑜 → C ∈ TermO ⁡ CatCat ⁡ C SetCat ⁡ 1 𝑜 ↔ ∀ d ∈ C SetCat ⁡ 1 𝑜 ∩ Cat ∃! f f ∈ d Func C
49 18 48 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
50 49 ibir ⊢ ∀ d ∈ C SetCat ⁡ 1 𝑜 ∩ Cat ∃! f f ∈ d Func C → C ∈ TermO ⁡ CatCat ⁡ C SetCat ⁡ 1 𝑜
51 1 7 50 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 |-