Metamath Proof Explorer

Theorem funcsn

Description: The category of one functor to a thin category is terminal. (Contributed by Zhi Wang, 17-Nov-2025)

Ref Expression
Hypotheses funcsn.q 
|- Q = ( C FuncCat D )
funcsn.f 
|- ( ph -> F e. V )
funcsn.c 
|- ( ph -> ( C Func D ) = { F } )
funcsn.d 
|- ( ph -> D e. ThinCat )
Assertion funcsn 
|- ( ph -> Q e. TermCat )

Proof

Step Hyp Ref Expression
1 funcsn.q 
 |-  Q = ( C FuncCat D )
2 funcsn.f 
 |-  ( ph -> F e. V )
3 funcsn.c 
 |-  ( ph -> ( C Func D ) = { F } )
4 funcsn.d 
 |-  ( ph -> D e. ThinCat )
5 1 fucbas 
 |-  ( C Func D ) = ( Base ` Q )
6 5 a1i 
 |-  ( ph -> ( C Func D ) = ( Base ` Q ) )
7 eqid 
 |-  ( C Nat D ) = ( C Nat D )
8 1 7 fuchom 
 |-  ( C Nat D ) = ( Hom ` Q )
9 8 a1i 
 |-  ( ph -> ( C Nat D ) = ( Hom ` Q ) )
10 simprl 
 |-  ( ( ph /\ ( a e. ( f ( C Nat D ) g ) /\ b e. ( f ( C Nat D ) g ) ) ) -> a e. ( f ( C Nat D ) g ) )
11 7 10 nat1st2nd 
 |-  ( ( ph /\ ( a e. ( f ( C Nat D ) g ) /\ b e. ( f ( C Nat D ) g ) ) ) -> a e. ( <. ( 1st ` f ) , ( 2nd ` f ) >. ( C Nat D ) <. ( 1st ` g ) , ( 2nd ` g ) >. ) )
12 eqid 
 |-  ( Base ` C ) = ( Base ` C )
13 7 11 12 natfn 
 |-  ( ( ph /\ ( a e. ( f ( C Nat D ) g ) /\ b e. ( f ( C Nat D ) g ) ) ) -> a Fn ( Base ` C ) )
14 simprr 
 |-  ( ( ph /\ ( a e. ( f ( C Nat D ) g ) /\ b e. ( f ( C Nat D ) g ) ) ) -> b e. ( f ( C Nat D ) g ) )
15 7 14 nat1st2nd 
 |-  ( ( ph /\ ( a e. ( f ( C Nat D ) g ) /\ b e. ( f ( C Nat D ) g ) ) ) -> b e. ( <. ( 1st ` f ) , ( 2nd ` f ) >. ( C Nat D ) <. ( 1st ` g ) , ( 2nd ` g ) >. ) )
16 7 15 12 natfn 
 |-  ( ( ph /\ ( a e. ( f ( C Nat D ) g ) /\ b e. ( f ( C Nat D ) g ) ) ) -> b Fn ( Base ` C ) )
17 eqid 
 |-  ( Base ` D ) = ( Base ` D )
18 7 11 natrcl2 
 |-  ( ( ph /\ ( a e. ( f ( C Nat D ) g ) /\ b e. ( f ( C Nat D ) g ) ) ) -> ( 1st ` f ) ( C Func D ) ( 2nd ` f ) )
19 12 17 18 funcf1 
 |-  ( ( ph /\ ( a e. ( f ( C Nat D ) g ) /\ b e. ( f ( C Nat D ) g ) ) ) -> ( 1st ` f ) : ( Base ` C ) --> ( Base ` D ) )
20 19 ffvelcdmda 
 |-  ( ( ( ph /\ ( a e. ( f ( C Nat D ) g ) /\ b e. ( f ( C Nat D ) g ) ) ) /\ x e. ( Base ` C ) ) -> ( ( 1st ` f ) ` x ) e. ( Base ` D ) )
21 7 11 natrcl3 
 |-  ( ( ph /\ ( a e. ( f ( C Nat D ) g ) /\ b e. ( f ( C Nat D ) g ) ) ) -> ( 1st ` g ) ( C Func D ) ( 2nd ` g ) )
22 12 17 21 funcf1 
 |-  ( ( ph /\ ( a e. ( f ( C Nat D ) g ) /\ b e. ( f ( C Nat D ) g ) ) ) -> ( 1st ` g ) : ( Base ` C ) --> ( Base ` D ) )
23 22 ffvelcdmda 
 |-  ( ( ( ph /\ ( a e. ( f ( C Nat D ) g ) /\ b e. ( f ( C Nat D ) g ) ) ) /\ x e. ( Base ` C ) ) -> ( ( 1st ` g ) ` x ) e. ( Base ` D ) )
24 11 adantr 
 |-  ( ( ( ph /\ ( a e. ( f ( C Nat D ) g ) /\ b e. ( f ( C Nat D ) g ) ) ) /\ x e. ( Base ` C ) ) -> a e. ( <. ( 1st ` f ) , ( 2nd ` f ) >. ( C Nat D ) <. ( 1st ` g ) , ( 2nd ` g ) >. ) )
25 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
26 simpr 
 |-  ( ( ( ph /\ ( a e. ( f ( C Nat D ) g ) /\ b e. ( f ( C Nat D ) g ) ) ) /\ x e. ( Base ` C ) ) -> x e. ( Base ` C ) )
27 7 24 12 25 26 natcl 
 |-  ( ( ( ph /\ ( a e. ( f ( C Nat D ) g ) /\ b e. ( f ( C Nat D ) g ) ) ) /\ x e. ( Base ` C ) ) -> ( a ` x ) e. ( ( ( 1st ` f ) ` x ) ( Hom ` D ) ( ( 1st ` g ) ` x ) ) )
28 15 adantr 
 |-  ( ( ( ph /\ ( a e. ( f ( C Nat D ) g ) /\ b e. ( f ( C Nat D ) g ) ) ) /\ x e. ( Base ` C ) ) -> b e. ( <. ( 1st ` f ) , ( 2nd ` f ) >. ( C Nat D ) <. ( 1st ` g ) , ( 2nd ` g ) >. ) )
29 7 28 12 25 26 natcl 
 |-  ( ( ( ph /\ ( a e. ( f ( C Nat D ) g ) /\ b e. ( f ( C Nat D ) g ) ) ) /\ x e. ( Base ` C ) ) -> ( b ` x ) e. ( ( ( 1st ` f ) ` x ) ( Hom ` D ) ( ( 1st ` g ) ` x ) ) )
30 4 ad2antrr 
 |-  ( ( ( ph /\ ( a e. ( f ( C Nat D ) g ) /\ b e. ( f ( C Nat D ) g ) ) ) /\ x e. ( Base ` C ) ) -> D e. ThinCat )
31 20 23 27 29 17 25 30 thincmo2 
 |-  ( ( ( ph /\ ( a e. ( f ( C Nat D ) g ) /\ b e. ( f ( C Nat D ) g ) ) ) /\ x e. ( Base ` C ) ) -> ( a ` x ) = ( b ` x ) )
32 13 16 31 eqfnfvd 
 |-  ( ( ph /\ ( a e. ( f ( C Nat D ) g ) /\ b e. ( f ( C Nat D ) g ) ) ) -> a = b )
33 32 ralrimivva 
 |-  ( ph -> A. a e. ( f ( C Nat D ) g ) A. b e. ( f ( C Nat D ) g ) a = b )
34 moel 
 |-  ( E* a a e. ( f ( C Nat D ) g ) <-> A. a e. ( f ( C Nat D ) g ) A. b e. ( f ( C Nat D ) g ) a = b )
35 33 34 sylibr 
 |-  ( ph -> E* a a e. ( f ( C Nat D ) g ) )
36 35 adantr 
 |-  ( ( ph /\ ( f e. ( C Func D ) /\ g e. ( C Func D ) ) ) -> E* a a e. ( f ( C Nat D ) g ) )
37 snidg 
 |-  ( F e. V -> F e. { F } )
38 2 37 syl 
 |-  ( ph -> F e. { F } )
39 38 3 eleqtrrd 
 |-  ( ph -> F e. ( C Func D ) )
40 39 func1st2nd 
 |-  ( ph -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
41 40 funcrcl2 
 |-  ( ph -> C e. Cat )
42 4 thinccd 
 |-  ( ph -> D e. Cat )
43 1 41 42 fuccat 
 |-  ( ph -> Q e. Cat )
44 6 9 36 43 isthincd 
 |-  ( ph -> Q e. ThinCat )
45 sneq 
 |-  ( f = F -> { f } = { F } )
46 45 eqeq2d 
 |-  ( f = F -> ( ( C Func D ) = { f } <-> ( C Func D ) = { F } ) )
47 2 3 46 spcedv 
 |-  ( ph -> E. f ( C Func D ) = { f } )
48 5 istermc 
 |-  ( Q e. TermCat <-> ( Q e. ThinCat /\ E. f ( C Func D ) = { f } ) )
49 44 47 48 sylanbrc 
 |-  ( ph -> Q e. TermCat )