Metamath Proof Explorer

Theorem functermc

Description: Functor to a terminal category. (Contributed by Zhi Wang, 17-Oct-2025)

Ref Expression
Hypotheses functermc.d 
|- ( ph -> D e. Cat )
functermc.e 
|- ( ph -> E e. TermCat )
functermc.b 
|- B = ( Base ` D )
functermc.c 
|- C = ( Base ` E )
functermc.h 
|- H = ( Hom ` D )
functermc.j 
|- J = ( Hom ` E )
functermc.f 
|- F = ( B X. C )
functermc.g 
|- G = ( x e. B , y e. B |-> ( ( x H y ) X. ( ( F ` x ) J ( F ` y ) ) ) )
Assertion functermc 
|- ( ph -> ( K ( D Func E ) L <-> ( K = F /\ L = G ) ) )

Proof

Step Hyp Ref Expression
1 functermc.d 
 |-  ( ph -> D e. Cat )
2 functermc.e 
 |-  ( ph -> E e. TermCat )
3 functermc.b 
 |-  B = ( Base ` D )
4 functermc.c 
 |-  C = ( Base ` E )
5 functermc.h 
 |-  H = ( Hom ` D )
6 functermc.j 
 |-  J = ( Hom ` E )
7 functermc.f 
 |-  F = ( B X. C )
8 functermc.g 
 |-  G = ( x e. B , y e. B |-> ( ( x H y ) X. ( ( F ` x ) J ( F ` y ) ) ) )
9 simpr 
 |-  ( ( ph /\ K ( D Func E ) L ) -> K ( D Func E ) L )
10 3 4 9 funcf1 
 |-  ( ( ph /\ K ( D Func E ) L ) -> K : B --> C )
11 2 4 termcbas 
 |-  ( ph -> E. z C = { z } )
12 feq3 
 |-  ( C = { z } -> ( K : B --> C <-> K : B --> { z } ) )
13 vex 
 |-  z e. _V
14 13 fconst2 
 |-  ( K : B --> { z } <-> K = ( B X. { z } ) )
15 xpeq2 
 |-  ( C = { z } -> ( B X. C ) = ( B X. { z } ) )
16 7 15 eqtrid 
 |-  ( C = { z } -> F = ( B X. { z } ) )
17 16 eqeq2d 
 |-  ( C = { z } -> ( K = F <-> K = ( B X. { z } ) ) )
18 14 17 bitr4id 
 |-  ( C = { z } -> ( K : B --> { z } <-> K = F ) )
19 12 18 bitrd 
 |-  ( C = { z } -> ( K : B --> C <-> K = F ) )
20 19 exlimiv 
 |-  ( E. z C = { z } -> ( K : B --> C <-> K = F ) )
21 11 20 syl 
 |-  ( ph -> ( K : B --> C <-> K = F ) )
22 21 biimpa 
 |-  ( ( ph /\ K : B --> C ) -> K = F )
23 10 22 syldan 
 |-  ( ( ph /\ K ( D Func E ) L ) -> K = F )
24 2 termcthind 
 |-  ( ph -> E e. ThinCat )
25 13 fconst 
 |-  ( B X. { z } ) : B --> { z }
26 16 feq1d 
 |-  ( C = { z } -> ( F : B --> C <-> ( B X. { z } ) : B --> C ) )
27 feq3 
 |-  ( C = { z } -> ( ( B X. { z } ) : B --> C <-> ( B X. { z } ) : B --> { z } ) )
28 26 27 bitrd 
 |-  ( C = { z } -> ( F : B --> C <-> ( B X. { z } ) : B --> { z } ) )
29 25 28 mpbiri 
 |-  ( C = { z } -> F : B --> C )
30 29 exlimiv 
 |-  ( E. z C = { z } -> F : B --> C )
31 11 30 syl 
 |-  ( ph -> F : B --> C )
32 2 adantr 
 |-  ( ( ph /\ ( z e. B /\ w e. B ) ) -> E e. TermCat )
33 31 ffvelcdmda 
 |-  ( ( ph /\ z e. B ) -> ( F ` z ) e. C )
34 33 adantrr 
 |-  ( ( ph /\ ( z e. B /\ w e. B ) ) -> ( F ` z ) e. C )
35 31 ffvelcdmda 
 |-  ( ( ph /\ w e. B ) -> ( F ` w ) e. C )
36 35 adantrl 
 |-  ( ( ph /\ ( z e. B /\ w e. B ) ) -> ( F ` w ) e. C )
37 32 4 34 36 6 termchomn0 
 |-  ( ( ph /\ ( z e. B /\ w e. B ) ) -> -. ( ( F ` z ) J ( F ` w ) ) = (/) )
38 37 pm2.21d 
 |-  ( ( ph /\ ( z e. B /\ w e. B ) ) -> ( ( ( F ` z ) J ( F ` w ) ) = (/) -> ( z H w ) = (/) ) )
39 38 ralrimivva 
 |-  ( ph -> A. z e. B A. w e. B ( ( ( F ` z ) J ( F ` w ) ) = (/) -> ( z H w ) = (/) ) )
40 3 4 5 6 1 24 31 8 39 functhinc 
 |-  ( ph -> ( F ( D Func E ) L <-> L = G ) )
41 23 40 functermclem 
 |-  ( ph -> ( K ( D Func E ) L <-> ( K = F /\ L = G ) ) )