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 ( ∀ 𝑑 ∈ ( { 𝐶 , ( SetCat ‘ 1o ) } ∩ Cat ) ∃! 𝑓 𝑓 ∈ ( 𝑑 Func 𝐶 ) → 𝐶 ∈ TermCat )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( CatCat ‘ { 𝐶 , ( SetCat ‘ 1o ) } ) = ( CatCat ‘ { 𝐶 , ( SetCat ‘ 1o ) } )
2 fvex ⊢ ( SetCat ‘ 1o ) ∈ V
3 2 prid2 ⊢ ( SetCat ‘ 1o ) ∈ { 𝐶 , ( SetCat ‘ 1o ) }
4 setc1oterm ⊢ ( SetCat ‘ 1o ) ∈ TermCat
5 3 4 elini ⊢ ( SetCat ‘ 1o ) ∈ ( { 𝐶 , ( SetCat ‘ 1o ) } ∩ TermCat )
6 5 ne0ii ⊢ ( { 𝐶 , ( SetCat ‘ 1o ) } ∩ TermCat ) ≠ ∅
7 6 a1i ⊢ ( ∀ 𝑑 ∈ ( { 𝐶 , ( SetCat ‘ 1o ) } ∩ Cat ) ∃! 𝑓 𝑓 ∈ ( 𝑑 Func 𝐶 ) → ( { 𝐶 , ( SetCat ‘ 1o ) } ∩ TermCat ) ≠ ∅ )
8 4 a1i ⊢ ( ⊤ → ( SetCat ‘ 1o ) ∈ TermCat )
9 8 termccd ⊢ ( ⊤ → ( SetCat ‘ 1o ) ∈ Cat )
10 9 mptru ⊢ ( SetCat ‘ 1o ) ∈ Cat
11 3 10 elini ⊢ ( SetCat ‘ 1o ) ∈ ( { 𝐶 , ( SetCat ‘ 1o ) } ∩ Cat )
12 oveq1 ⊢ ( 𝑑 = ( SetCat ‘ 1o ) → ( 𝑑 Func 𝐶 ) = ( ( SetCat ‘ 1o ) Func 𝐶 ) )
13 12 eleq2d ⊢ ( 𝑑 = ( SetCat ‘ 1o ) → ( 𝑓 ∈ ( 𝑑 Func 𝐶 ) ↔ 𝑓 ∈ ( ( SetCat ‘ 1o ) Func 𝐶 ) ) )
14 13 eubidv ⊢ ( 𝑑 = ( SetCat ‘ 1o ) → ( ∃! 𝑓 𝑓 ∈ ( 𝑑 Func 𝐶 ) ↔ ∃! 𝑓 𝑓 ∈ ( ( SetCat ‘ 1o ) Func 𝐶 ) ) )
15 14 rspcv ⊢ ( ( SetCat ‘ 1o ) ∈ ( { 𝐶 , ( SetCat ‘ 1o ) } ∩ Cat ) → ( ∀ 𝑑 ∈ ( { 𝐶 , ( SetCat ‘ 1o ) } ∩ Cat ) ∃! 𝑓 𝑓 ∈ ( 𝑑 Func 𝐶 ) → ∃! 𝑓 𝑓 ∈ ( ( SetCat ‘ 1o ) Func 𝐶 ) ) )
16 11 15 ax-mp ⊢ ( ∀ 𝑑 ∈ ( { 𝐶 , ( SetCat ‘ 1o ) } ∩ Cat ) ∃! 𝑓 𝑓 ∈ ( 𝑑 Func 𝐶 ) → ∃! 𝑓 𝑓 ∈ ( ( SetCat ‘ 1o ) Func 𝐶 ) )
17 euen1b ⊢ ( ( ( SetCat ‘ 1o ) Func 𝐶 ) ≈ 1o ↔ ∃! 𝑓 𝑓 ∈ ( ( SetCat ‘ 1o ) Func 𝐶 ) )
18 16 17 sylibr ⊢ ( ∀ 𝑑 ∈ ( { 𝐶 , ( SetCat ‘ 1o ) } ∩ Cat ) ∃! 𝑓 𝑓 ∈ ( 𝑑 Func 𝐶 ) → ( ( SetCat ‘ 1o ) Func 𝐶 ) ≈ 1o )
19 eqid ⊢ ( Base ‘ ( CatCat ‘ { 𝐶 , ( SetCat ‘ 1o ) } ) ) = ( Base ‘ ( CatCat ‘ { 𝐶 , ( SetCat ‘ 1o ) } ) )
20 prex ⊢ { 𝐶 , ( SetCat ‘ 1o ) } ∈ V
21 20 a1i ⊢ ( ⊤ → { 𝐶 , ( SetCat ‘ 1o ) } ∈ V )
22 1 19 21 catcbas ⊢ ( ⊤ → ( Base ‘ ( CatCat ‘ { 𝐶 , ( SetCat ‘ 1o ) } ) ) = ( { 𝐶 , ( SetCat ‘ 1o ) } ∩ Cat ) )
23 22 mptru ⊢ ( Base ‘ ( CatCat ‘ { 𝐶 , ( SetCat ‘ 1o ) } ) ) = ( { 𝐶 , ( SetCat ‘ 1o ) } ∩ Cat )
24 23 eqcomi ⊢ ( { 𝐶 , ( SetCat ‘ 1o ) } ∩ Cat ) = ( Base ‘ ( CatCat ‘ { 𝐶 , ( SetCat ‘ 1o ) } ) )
25 eqid ⊢ ( Hom ‘ ( CatCat ‘ { 𝐶 , ( SetCat ‘ 1o ) } ) ) = ( Hom ‘ ( CatCat ‘ { 𝐶 , ( SetCat ‘ 1o ) } ) )
26 1 catccat ⊢ ( { 𝐶 , ( SetCat ‘ 1o ) } ∈ V → ( CatCat ‘ { 𝐶 , ( SetCat ‘ 1o ) } ) ∈ Cat )
27 20 26 ax-mp ⊢ ( CatCat ‘ { 𝐶 , ( SetCat ‘ 1o ) } ) ∈ Cat
28 27 a1i ⊢ ( ( ( SetCat ‘ 1o ) Func 𝐶 ) ≈ 1o → ( CatCat ‘ { 𝐶 , ( SetCat ‘ 1o ) } ) ∈ Cat )
29 euex ⊢ ( ∃! 𝑓 𝑓 ∈ ( ( SetCat ‘ 1o ) Func 𝐶 ) → ∃ 𝑓 𝑓 ∈ ( ( SetCat ‘ 1o ) Func 𝐶 ) )
30 funcrcl ⊢ ( 𝑓 ∈ ( ( SetCat ‘ 1o ) Func 𝐶 ) → ( ( SetCat ‘ 1o ) ∈ Cat ∧ 𝐶 ∈ Cat ) )
31 30 simprd ⊢ ( 𝑓 ∈ ( ( SetCat ‘ 1o ) Func 𝐶 ) → 𝐶 ∈ Cat )
32 31 exlimiv ⊢ ( ∃ 𝑓 𝑓 ∈ ( ( SetCat ‘ 1o ) Func 𝐶 ) → 𝐶 ∈ Cat )
33 29 32 syl ⊢ ( ∃! 𝑓 𝑓 ∈ ( ( SetCat ‘ 1o ) Func 𝐶 ) → 𝐶 ∈ Cat )
34 17 33 sylbi ⊢ ( ( ( SetCat ‘ 1o ) Func 𝐶 ) ≈ 1o → 𝐶 ∈ Cat )
35 prid1g ⊢ ( 𝐶 ∈ Cat → 𝐶 ∈ { 𝐶 , ( SetCat ‘ 1o ) } )
36 34 35 syl ⊢ ( ( ( SetCat ‘ 1o ) Func 𝐶 ) ≈ 1o → 𝐶 ∈ { 𝐶 , ( SetCat ‘ 1o ) } )
37 36 34 elind ⊢ ( ( ( SetCat ‘ 1o ) Func 𝐶 ) ≈ 1o → 𝐶 ∈ ( { 𝐶 , ( SetCat ‘ 1o ) } ∩ Cat ) )
38 24 25 28 37 istermo ⊢ ( ( ( SetCat ‘ 1o ) Func 𝐶 ) ≈ 1o → ( 𝐶 ∈ ( TermO ‘ ( CatCat ‘ { 𝐶 , ( SetCat ‘ 1o ) } ) ) ↔ ∀ 𝑑 ∈ ( { 𝐶 , ( SetCat ‘ 1o ) } ∩ Cat ) ∃! 𝑓 𝑓 ∈ ( 𝑑 ( Hom ‘ ( CatCat ‘ { 𝐶 , ( SetCat ‘ 1o ) } ) ) 𝐶 ) ) )
39 20 a1i ⊢ ( ( ( ( SetCat ‘ 1o ) Func 𝐶 ) ≈ 1o ∧ 𝑑 ∈ ( { 𝐶 , ( SetCat ‘ 1o ) } ∩ Cat ) ) → { 𝐶 , ( SetCat ‘ 1o ) } ∈ V )
40 simpr ⊢ ( ( ( ( SetCat ‘ 1o ) Func 𝐶 ) ≈ 1o ∧ 𝑑 ∈ ( { 𝐶 , ( SetCat ‘ 1o ) } ∩ Cat ) ) → 𝑑 ∈ ( { 𝐶 , ( SetCat ‘ 1o ) } ∩ Cat ) )
41 37 adantr ⊢ ( ( ( ( SetCat ‘ 1o ) Func 𝐶 ) ≈ 1o ∧ 𝑑 ∈ ( { 𝐶 , ( SetCat ‘ 1o ) } ∩ Cat ) ) → 𝐶 ∈ ( { 𝐶 , ( SetCat ‘ 1o ) } ∩ Cat ) )
42 1 24 39 25 40 41 catchom ⊢ ( ( ( ( SetCat ‘ 1o ) Func 𝐶 ) ≈ 1o ∧ 𝑑 ∈ ( { 𝐶 , ( SetCat ‘ 1o ) } ∩ Cat ) ) → ( 𝑑 ( Hom ‘ ( CatCat ‘ { 𝐶 , ( SetCat ‘ 1o ) } ) ) 𝐶 ) = ( 𝑑 Func 𝐶 ) )
43 42 eleq2d ⊢ ( ( ( ( SetCat ‘ 1o ) Func 𝐶 ) ≈ 1o ∧ 𝑑 ∈ ( { 𝐶 , ( SetCat ‘ 1o ) } ∩ Cat ) ) → ( 𝑓 ∈ ( 𝑑 ( Hom ‘ ( CatCat ‘ { 𝐶 , ( SetCat ‘ 1o ) } ) ) 𝐶 ) ↔ 𝑓 ∈ ( 𝑑 Func 𝐶 ) ) )
44 43 eubidv ⊢ ( ( ( ( SetCat ‘ 1o ) Func 𝐶 ) ≈ 1o ∧ 𝑑 ∈ ( { 𝐶 , ( SetCat ‘ 1o ) } ∩ Cat ) ) → ( ∃! 𝑓 𝑓 ∈ ( 𝑑 ( Hom ‘ ( CatCat ‘ { 𝐶 , ( SetCat ‘ 1o ) } ) ) 𝐶 ) ↔ ∃! 𝑓 𝑓 ∈ ( 𝑑 Func 𝐶 ) ) )
45 44 ralbidva ⊢ ( ( ( SetCat ‘ 1o ) Func 𝐶 ) ≈ 1o → ( ∀ 𝑑 ∈ ( { 𝐶 , ( SetCat ‘ 1o ) } ∩ Cat ) ∃! 𝑓 𝑓 ∈ ( 𝑑 ( Hom ‘ ( CatCat ‘ { 𝐶 , ( SetCat ‘ 1o ) } ) ) 𝐶 ) ↔ ∀ 𝑑 ∈ ( { 𝐶 , ( SetCat ‘ 1o ) } ∩ Cat ) ∃! 𝑓 𝑓 ∈ ( 𝑑 Func 𝐶 ) ) )
46 38 45 bitrd ⊢ ( ( ( SetCat ‘ 1o ) Func 𝐶 ) ≈ 1o → ( 𝐶 ∈ ( TermO ‘ ( CatCat ‘ { 𝐶 , ( SetCat ‘ 1o ) } ) ) ↔ ∀ 𝑑 ∈ ( { 𝐶 , ( SetCat ‘ 1o ) } ∩ Cat ) ∃! 𝑓 𝑓 ∈ ( 𝑑 Func 𝐶 ) ) )
47 18 46 syl ⊢ ( ∀ 𝑑 ∈ ( { 𝐶 , ( SetCat ‘ 1o ) } ∩ Cat ) ∃! 𝑓 𝑓 ∈ ( 𝑑 Func 𝐶 ) → ( 𝐶 ∈ ( TermO ‘ ( CatCat ‘ { 𝐶 , ( SetCat ‘ 1o ) } ) ) ↔ ∀ 𝑑 ∈ ( { 𝐶 , ( SetCat ‘ 1o ) } ∩ Cat ) ∃! 𝑓 𝑓 ∈ ( 𝑑 Func 𝐶 ) ) )
48 47 ibir ⊢ ( ∀ 𝑑 ∈ ( { 𝐶 , ( SetCat ‘ 1o ) } ∩ Cat ) ∃! 𝑓 𝑓 ∈ ( 𝑑 Func 𝐶 ) → 𝐶 ∈ ( TermO ‘ ( CatCat ‘ { 𝐶 , ( SetCat ‘ 1o ) } ) ) )
49 1 7 48 termcterm2 ⊢ ( ∀ 𝑑 ∈ ( { 𝐶 , ( SetCat ‘ 1o ) } ∩ Cat ) ∃! 𝑓 𝑓 ∈ ( 𝑑 Func 𝐶 ) → 𝐶 ∈ TermCat )