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 ( ∀ 𝑑 ∈ ( { 𝐶 , ( 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 relfunc ⊢ Rel ( ( SetCat ‘ 1o ) Func 𝐶 )
31 1st2ndbr ⊢ ( ( Rel ( ( SetCat ‘ 1o ) Func 𝐶 ) ∧ 𝑓 ∈ ( ( SetCat ‘ 1o ) Func 𝐶 ) ) → ( 1st ‘ 𝑓 ) ( ( SetCat ‘ 1o ) Func 𝐶 ) ( 2nd ‘ 𝑓 ) )
32 30 31 mpan ⊢ ( 𝑓 ∈ ( ( SetCat ‘ 1o ) Func 𝐶 ) → ( 1st ‘ 𝑓 ) ( ( SetCat ‘ 1o ) Func 𝐶 ) ( 2nd ‘ 𝑓 ) )
33 32 funcrcl3 ⊢ ( 𝑓 ∈ ( ( SetCat ‘ 1o ) Func 𝐶 ) → 𝐶 ∈ Cat )
34 33 exlimiv ⊢ ( ∃ 𝑓 𝑓 ∈ ( ( SetCat ‘ 1o ) Func 𝐶 ) → 𝐶 ∈ Cat )
35 29 34 syl ⊢ ( ∃! 𝑓 𝑓 ∈ ( ( SetCat ‘ 1o ) Func 𝐶 ) → 𝐶 ∈ Cat )
36 17 35 sylbi ⊢ ( ( ( SetCat ‘ 1o ) Func 𝐶 ) ≈ 1o → 𝐶 ∈ Cat )
37 prid1g ⊢ ( 𝐶 ∈ Cat → 𝐶 ∈ { 𝐶 , ( SetCat ‘ 1o ) } )
38 36 37 syl ⊢ ( ( ( SetCat ‘ 1o ) Func 𝐶 ) ≈ 1o → 𝐶 ∈ { 𝐶 , ( SetCat ‘ 1o ) } )
39 38 36 elind ⊢ ( ( ( SetCat ‘ 1o ) Func 𝐶 ) ≈ 1o → 𝐶 ∈ ( { 𝐶 , ( SetCat ‘ 1o ) } ∩ Cat ) )
40 24 25 28 39 istermo ⊢ ( ( ( SetCat ‘ 1o ) Func 𝐶 ) ≈ 1o → ( 𝐶 ∈ ( TermO ‘ ( CatCat ‘ { 𝐶 , ( SetCat ‘ 1o ) } ) ) ↔ ∀ 𝑑 ∈ ( { 𝐶 , ( SetCat ‘ 1o ) } ∩ Cat ) ∃! 𝑓 𝑓 ∈ ( 𝑑 ( Hom ‘ ( CatCat ‘ { 𝐶 , ( SetCat ‘ 1o ) } ) ) 𝐶 ) ) )
41 20 a1i ⊢ ( ( ( ( SetCat ‘ 1o ) Func 𝐶 ) ≈ 1o ∧ 𝑑 ∈ ( { 𝐶 , ( SetCat ‘ 1o ) } ∩ Cat ) ) → { 𝐶 , ( SetCat ‘ 1o ) } ∈ V )
42 simpr ⊢ ( ( ( ( SetCat ‘ 1o ) Func 𝐶 ) ≈ 1o ∧ 𝑑 ∈ ( { 𝐶 , ( SetCat ‘ 1o ) } ∩ Cat ) ) → 𝑑 ∈ ( { 𝐶 , ( SetCat ‘ 1o ) } ∩ Cat ) )
43 39 adantr ⊢ ( ( ( ( SetCat ‘ 1o ) Func 𝐶 ) ≈ 1o ∧ 𝑑 ∈ ( { 𝐶 , ( SetCat ‘ 1o ) } ∩ Cat ) ) → 𝐶 ∈ ( { 𝐶 , ( SetCat ‘ 1o ) } ∩ Cat ) )
44 1 24 41 25 42 43 catchom ⊢ ( ( ( ( SetCat ‘ 1o ) Func 𝐶 ) ≈ 1o ∧ 𝑑 ∈ ( { 𝐶 , ( SetCat ‘ 1o ) } ∩ Cat ) ) → ( 𝑑 ( Hom ‘ ( CatCat ‘ { 𝐶 , ( SetCat ‘ 1o ) } ) ) 𝐶 ) = ( 𝑑 Func 𝐶 ) )
45 44 eleq2d ⊢ ( ( ( ( SetCat ‘ 1o ) Func 𝐶 ) ≈ 1o ∧ 𝑑 ∈ ( { 𝐶 , ( SetCat ‘ 1o ) } ∩ Cat ) ) → ( 𝑓 ∈ ( 𝑑 ( Hom ‘ ( CatCat ‘ { 𝐶 , ( SetCat ‘ 1o ) } ) ) 𝐶 ) ↔ 𝑓 ∈ ( 𝑑 Func 𝐶 ) ) )
46 45 eubidv ⊢ ( ( ( ( SetCat ‘ 1o ) Func 𝐶 ) ≈ 1o ∧ 𝑑 ∈ ( { 𝐶 , ( SetCat ‘ 1o ) } ∩ Cat ) ) → ( ∃! 𝑓 𝑓 ∈ ( 𝑑 ( Hom ‘ ( CatCat ‘ { 𝐶 , ( SetCat ‘ 1o ) } ) ) 𝐶 ) ↔ ∃! 𝑓 𝑓 ∈ ( 𝑑 Func 𝐶 ) ) )
47 46 ralbidva ⊢ ( ( ( SetCat ‘ 1o ) Func 𝐶 ) ≈ 1o → ( ∀ 𝑑 ∈ ( { 𝐶 , ( SetCat ‘ 1o ) } ∩ Cat ) ∃! 𝑓 𝑓 ∈ ( 𝑑 ( Hom ‘ ( CatCat ‘ { 𝐶 , ( SetCat ‘ 1o ) } ) ) 𝐶 ) ↔ ∀ 𝑑 ∈ ( { 𝐶 , ( SetCat ‘ 1o ) } ∩ Cat ) ∃! 𝑓 𝑓 ∈ ( 𝑑 Func 𝐶 ) ) )
48 40 47 bitrd ⊢ ( ( ( SetCat ‘ 1o ) Func 𝐶 ) ≈ 1o → ( 𝐶 ∈ ( TermO ‘ ( CatCat ‘ { 𝐶 , ( SetCat ‘ 1o ) } ) ) ↔ ∀ 𝑑 ∈ ( { 𝐶 , ( SetCat ‘ 1o ) } ∩ Cat ) ∃! 𝑓 𝑓 ∈ ( 𝑑 Func 𝐶 ) ) )
49 18 48 syl ⊢ ( ∀ 𝑑 ∈ ( { 𝐶 , ( SetCat ‘ 1o ) } ∩ Cat ) ∃! 𝑓 𝑓 ∈ ( 𝑑 Func 𝐶 ) → ( 𝐶 ∈ ( TermO ‘ ( CatCat ‘ { 𝐶 , ( SetCat ‘ 1o ) } ) ) ↔ ∀ 𝑑 ∈ ( { 𝐶 , ( SetCat ‘ 1o ) } ∩ Cat ) ∃! 𝑓 𝑓 ∈ ( 𝑑 Func 𝐶 ) ) )
50 49 ibir ⊢ ( ∀ 𝑑 ∈ ( { 𝐶 , ( SetCat ‘ 1o ) } ∩ Cat ) ∃! 𝑓 𝑓 ∈ ( 𝑑 Func 𝐶 ) → 𝐶 ∈ ( TermO ‘ ( CatCat ‘ { 𝐶 , ( SetCat ‘ 1o ) } ) ) )
51 1 7 50 termcterm2 ⊢ ( ∀ 𝑑 ∈ ( { 𝐶 , ( SetCat ‘ 1o ) } ∩ Cat ) ∃! 𝑓 𝑓 ∈ ( 𝑑 Func 𝐶 ) → 𝐶 ∈ TermCat )