Metamath Proof Explorer

Theorem termcarweu

Description: There exists a unique disjointified arrow in a terminal category. (Contributed by Zhi Wang, 20-Oct-2025)

Ref Expression
Assertion termcarweu 
|- ( C e. TermCat -> E! a a e. ( Arrow ` C ) )

Proof

Step Hyp Ref Expression
1 id 
 |-  ( C e. TermCat -> C e. TermCat )
2 eqid 
 |-  ( Base ` C ) = ( Base ` C )
3 1 2 termcbas 
 |-  ( C e. TermCat -> E. x ( Base ` C ) = { x } )
4 eqid 
 |-  ( HomA ` C ) = ( HomA ` C )
5 1 adantr 
 |-  ( ( C e. TermCat /\ ( Base ` C ) = { x } ) -> C e. TermCat )
6 5 termccd 
 |-  ( ( C e. TermCat /\ ( Base ` C ) = { x } ) -> C e. Cat )
7 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
8 vsnid 
 |-  x e. { x }
9 simpr 
 |-  ( ( C e. TermCat /\ ( Base ` C ) = { x } ) -> ( Base ` C ) = { x } )
10 8 9 eleqtrrid 
 |-  ( ( C e. TermCat /\ ( Base ` C ) = { x } ) -> x e. ( Base ` C ) )
11 eqid 
 |-  ( Id ` C ) = ( Id ` C )
12 2 7 11 6 10 catidcl 
 |-  ( ( C e. TermCat /\ ( Base ` C ) = { x } ) -> ( ( Id ` C ) ` x ) e. ( x ( Hom ` C ) x ) )
13 4 2 6 7 10 10 12 elhomai2 
 |-  ( ( C e. TermCat /\ ( Base ` C ) = { x } ) -> <. x , x , ( ( Id ` C ) ` x ) >. e. ( x ( HomA ` C ) x ) )
14 eqid 
 |-  ( Arrow ` C ) = ( Arrow ` C )
15 14 arwdmcd 
 |-  ( a e. ( Arrow ` C ) -> a = <. ( domA ` a ) , ( codA ` a ) , ( 2nd ` a ) >. )
16 15 adantl 
 |-  ( ( ( C e. TermCat /\ ( Base ` C ) = { x } ) /\ a e. ( Arrow ` C ) ) -> a = <. ( domA ` a ) , ( codA ` a ) , ( 2nd ` a ) >. )
17 5 adantr 
 |-  ( ( ( C e. TermCat /\ ( Base ` C ) = { x } ) /\ a e. ( Arrow ` C ) ) -> C e. TermCat )
18 14 2 arwdm 
 |-  ( a e. ( Arrow ` C ) -> ( domA ` a ) e. ( Base ` C ) )
19 18 adantl 
 |-  ( ( ( C e. TermCat /\ ( Base ` C ) = { x } ) /\ a e. ( Arrow ` C ) ) -> ( domA ` a ) e. ( Base ` C ) )
20 10 adantr 
 |-  ( ( ( C e. TermCat /\ ( Base ` C ) = { x } ) /\ a e. ( Arrow ` C ) ) -> x e. ( Base ` C ) )
21 17 2 19 20 termcbasmo 
 |-  ( ( ( C e. TermCat /\ ( Base ` C ) = { x } ) /\ a e. ( Arrow ` C ) ) -> ( domA ` a ) = x )
22 14 2 arwcd 
 |-  ( a e. ( Arrow ` C ) -> ( codA ` a ) e. ( Base ` C ) )
23 22 adantl 
 |-  ( ( ( C e. TermCat /\ ( Base ` C ) = { x } ) /\ a e. ( Arrow ` C ) ) -> ( codA ` a ) e. ( Base ` C ) )
24 17 2 23 20 termcbasmo 
 |-  ( ( ( C e. TermCat /\ ( Base ` C ) = { x } ) /\ a e. ( Arrow ` C ) ) -> ( codA ` a ) = x )
25 14 7 arwhom 
 |-  ( a e. ( Arrow ` C ) -> ( 2nd ` a ) e. ( ( domA ` a ) ( Hom ` C ) ( codA ` a ) ) )
26 25 adantl 
 |-  ( ( ( C e. TermCat /\ ( Base ` C ) = { x } ) /\ a e. ( Arrow ` C ) ) -> ( 2nd ` a ) e. ( ( domA ` a ) ( Hom ` C ) ( codA ` a ) ) )
27 12 adantr 
 |-  ( ( ( C e. TermCat /\ ( Base ` C ) = { x } ) /\ a e. ( Arrow ` C ) ) -> ( ( Id ` C ) ` x ) e. ( x ( Hom ` C ) x ) )
28 17 2 19 23 7 26 20 20 27 termchommo 
 |-  ( ( ( C e. TermCat /\ ( Base ` C ) = { x } ) /\ a e. ( Arrow ` C ) ) -> ( 2nd ` a ) = ( ( Id ` C ) ` x ) )
29 21 24 28 oteq123d 
 |-  ( ( ( C e. TermCat /\ ( Base ` C ) = { x } ) /\ a e. ( Arrow ` C ) ) -> <. ( domA ` a ) , ( codA ` a ) , ( 2nd ` a ) >. = <. x , x , ( ( Id ` C ) ` x ) >. )
30 16 29 eqtrd 
 |-  ( ( ( C e. TermCat /\ ( Base ` C ) = { x } ) /\ a e. ( Arrow ` C ) ) -> a = <. x , x , ( ( Id ` C ) ` x ) >. )
31 simpr 
 |-  ( ( ( C e. TermCat /\ ( Base ` C ) = { x } ) /\ a = <. x , x , ( ( Id ` C ) ` x ) >. ) -> a = <. x , x , ( ( Id ` C ) ` x ) >. )
32 14 4 homarw 
 |-  ( x ( HomA ` C ) x ) C_ ( Arrow ` C )
33 32 13 sselid 
 |-  ( ( C e. TermCat /\ ( Base ` C ) = { x } ) -> <. x , x , ( ( Id ` C ) ` x ) >. e. ( Arrow ` C ) )
34 33 adantr 
 |-  ( ( ( C e. TermCat /\ ( Base ` C ) = { x } ) /\ a = <. x , x , ( ( Id ` C ) ` x ) >. ) -> <. x , x , ( ( Id ` C ) ` x ) >. e. ( Arrow ` C ) )
35 31 34 eqeltrd 
 |-  ( ( ( C e. TermCat /\ ( Base ` C ) = { x } ) /\ a = <. x , x , ( ( Id ` C ) ` x ) >. ) -> a e. ( Arrow ` C ) )
36 30 35 impbida 
 |-  ( ( C e. TermCat /\ ( Base ` C ) = { x } ) -> ( a e. ( Arrow ` C ) <-> a = <. x , x , ( ( Id ` C ) ` x ) >. ) )
37 36 alrimiv 
 |-  ( ( C e. TermCat /\ ( Base ` C ) = { x } ) -> A. a ( a e. ( Arrow ` C ) <-> a = <. x , x , ( ( Id ` C ) ` x ) >. ) )
38 eqeq2 
 |-  ( b = <. x , x , ( ( Id ` C ) ` x ) >. -> ( a = b <-> a = <. x , x , ( ( Id ` C ) ` x ) >. ) )
39 38 bibi2d 
 |-  ( b = <. x , x , ( ( Id ` C ) ` x ) >. -> ( ( a e. ( Arrow ` C ) <-> a = b ) <-> ( a e. ( Arrow ` C ) <-> a = <. x , x , ( ( Id ` C ) ` x ) >. ) ) )
40 39 albidv 
 |-  ( b = <. x , x , ( ( Id ` C ) ` x ) >. -> ( A. a ( a e. ( Arrow ` C ) <-> a = b ) <-> A. a ( a e. ( Arrow ` C ) <-> a = <. x , x , ( ( Id ` C ) ` x ) >. ) ) )
41 13 37 40 spcedv 
 |-  ( ( C e. TermCat /\ ( Base ` C ) = { x } ) -> E. b A. a ( a e. ( Arrow ` C ) <-> a = b ) )
42 3 41 exlimddv 
 |-  ( C e. TermCat -> E. b A. a ( a e. ( Arrow ` C ) <-> a = b ) )
43 eu6im 
 |-  ( E. b A. a ( a e. ( Arrow ` C ) <-> a = b ) -> E! a a e. ( Arrow ` C ) )
44 42 43 syl 
 |-  ( C e. TermCat -> E! a a e. ( Arrow ` C ) )