This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 0fucterm

Description: The category of functors from an initial category is terminal. (Contributed by Zhi Wang, 17-Nov-2025)

Ref Expression
Hypotheses 0fucterm.c 
|- ( ph -> C e. V )
0fucterm.b 
|- ( ph -> (/) = ( Base ` C ) )
0fucterm.d 
|- ( ph -> D e. Cat )
0fucterm.q 
|- Q = ( C FuncCat D )
Assertion 0fucterm 
|- ( ph -> Q e. TermCat )

Proof

Step Hyp Ref Expression
1 0fucterm.c 
 |-  ( ph -> C e. V )
2 0fucterm.b 
 |-  ( ph -> (/) = ( Base ` C ) )
3 0fucterm.d 
 |-  ( ph -> D e. Cat )
4 0fucterm.q 
 |-  Q = ( C FuncCat D )
5 4 fucbas 
 |-  ( C Func D ) = ( Base ` Q )
6 5 a1i 
 |-  ( ph -> ( C Func D ) = ( Base ` Q ) )
7 eqid 
 |-  ( C Nat D ) = ( C Nat D )
8 4 7 fuchom 
 |-  ( C Nat D ) = ( Hom ` Q )
9 8 a1i 
 |-  ( ph -> ( C Nat D ) = ( Hom ` Q ) )
10 simprl 
 |-  ( ( ( ph /\ ( f e. ( C Func D ) /\ g e. ( C Func D ) ) ) /\ ( 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 /\ ( f e. ( C Func D ) /\ g e. ( C Func D ) ) ) /\ ( 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 /\ ( f e. ( C Func D ) /\ g e. ( C Func D ) ) ) /\ ( a e. ( f ( C Nat D ) g ) /\ b e. ( f ( C Nat D ) g ) ) ) -> a Fn ( Base ` C ) )
14 2 ad2antrr 
 |-  ( ( ( ph /\ ( f e. ( C Func D ) /\ g e. ( C Func D ) ) ) /\ ( a e. ( f ( C Nat D ) g ) /\ b e. ( f ( C Nat D ) g ) ) ) -> (/) = ( Base ` C ) )
15 14 fneq2d 
 |-  ( ( ( ph /\ ( f e. ( C Func D ) /\ g e. ( C Func D ) ) ) /\ ( a e. ( f ( C Nat D ) g ) /\ b e. ( f ( C Nat D ) g ) ) ) -> ( a Fn (/) <-> a Fn ( Base ` C ) ) )
16 13 15 mpbird 
 |-  ( ( ( ph /\ ( f e. ( C Func D ) /\ g e. ( C Func D ) ) ) /\ ( a e. ( f ( C Nat D ) g ) /\ b e. ( f ( C Nat D ) g ) ) ) -> a Fn (/) )
17 fn0 
 |-  ( a Fn (/) <-> a = (/) )
18 16 17 sylib 
 |-  ( ( ( ph /\ ( f e. ( C Func D ) /\ g e. ( C Func D ) ) ) /\ ( a e. ( f ( C Nat D ) g ) /\ b e. ( f ( C Nat D ) g ) ) ) -> a = (/) )
19 simprr 
 |-  ( ( ( ph /\ ( f e. ( C Func D ) /\ g e. ( C Func D ) ) ) /\ ( a e. ( f ( C Nat D ) g ) /\ b e. ( f ( C Nat D ) g ) ) ) -> b e. ( f ( C Nat D ) g ) )
20 7 19 nat1st2nd 
 |-  ( ( ( ph /\ ( f e. ( C Func D ) /\ g e. ( C Func D ) ) ) /\ ( 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 ) >. ) )
21 7 20 12 natfn 
 |-  ( ( ( ph /\ ( f e. ( C Func D ) /\ g e. ( C Func D ) ) ) /\ ( a e. ( f ( C Nat D ) g ) /\ b e. ( f ( C Nat D ) g ) ) ) -> b Fn ( Base ` C ) )
22 14 fneq2d 
 |-  ( ( ( ph /\ ( f e. ( C Func D ) /\ g e. ( C Func D ) ) ) /\ ( a e. ( f ( C Nat D ) g ) /\ b e. ( f ( C Nat D ) g ) ) ) -> ( b Fn (/) <-> b Fn ( Base ` C ) ) )
23 21 22 mpbird 
 |-  ( ( ( ph /\ ( f e. ( C Func D ) /\ g e. ( C Func D ) ) ) /\ ( a e. ( f ( C Nat D ) g ) /\ b e. ( f ( C Nat D ) g ) ) ) -> b Fn (/) )
24 fn0 
 |-  ( b Fn (/) <-> b = (/) )
25 23 24 sylib 
 |-  ( ( ( ph /\ ( f e. ( C Func D ) /\ g e. ( C Func D ) ) ) /\ ( a e. ( f ( C Nat D ) g ) /\ b e. ( f ( C Nat D ) g ) ) ) -> b = (/) )
26 18 25 eqtr4d 
 |-  ( ( ( ph /\ ( f e. ( C Func D ) /\ g e. ( C Func D ) ) ) /\ ( a e. ( f ( C Nat D ) g ) /\ b e. ( f ( C Nat D ) g ) ) ) -> a = b )
27 26 ralrimivva 
 |-  ( ( ph /\ ( f e. ( C Func D ) /\ g e. ( C Func D ) ) ) -> A. a e. ( f ( C Nat D ) g ) A. b e. ( f ( C Nat D ) g ) a = b )
28 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 )
29 27 28 sylibr 
 |-  ( ( ph /\ ( f e. ( C Func D ) /\ g e. ( C Func D ) ) ) -> E* a a e. ( f ( C Nat D ) g ) )
30 0catg 
 |-  ( ( C e. V /\ (/) = ( Base ` C ) ) -> C e. Cat )
31 1 2 30 syl2anc 
 |-  ( ph -> C e. Cat )
32 4 31 3 fuccat 
 |-  ( ph -> Q e. Cat )
33 6 9 29 32 isthincd 
 |-  ( ph -> Q e. ThinCat )
34 opex 
 |-  <. (/) , (/) >. e. _V
35 34 a1i 
 |-  ( ph -> <. (/) , (/) >. e. _V )
36 1 2 3 0funcg 
 |-  ( ph -> ( C Func D ) = { <. (/) , (/) >. } )
37 sneq 
 |-  ( f = <. (/) , (/) >. -> { f } = { <. (/) , (/) >. } )
38 37 eqeq2d 
 |-  ( f = <. (/) , (/) >. -> ( ( C Func D ) = { f } <-> ( C Func D ) = { <. (/) , (/) >. } ) )
39 35 36 38 spcedv 
 |-  ( ph -> E. f ( C Func D ) = { f } )
40 5 istermc 
 |-  ( Q e. TermCat <-> ( Q e. ThinCat /\ E. f ( C Func D ) = { f } ) )
41 33 39 40 sylanbrc 
 |-  ( ph -> Q e. TermCat )