Theorem termcarweu

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

	Ref	Expression
Assertion	termcarweu	Could not format assertion : No typesetting found for |- ( C e. TermCat -> E! a a e. ( Arrow ` C ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		id	Could not format ( C e. TermCat -> C e. TermCat ) : No typesetting found for |- ( C e. TermCat -> C e. TermCat ) with typecode |-
2		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
3	1 2	termcbas	Could not format ( C e. TermCat -> E. x ( Base ` C ) = { x } ) : No typesetting found for |- ( C e. TermCat -> E. x ( Base ` C ) = { x } ) with typecode |-
4		eqid	$$⊢{Hom}_a\left(C\right)={Hom}_a\left(C\right)$$
5	1	adantr	Could not format ( ( C e. TermCat /\ ( Base ` C ) = { x } ) -> C e. TermCat ) : No typesetting found for |- ( ( C e. TermCat /\ ( Base ` C ) = { x } ) -> C e. TermCat ) with typecode |-
6	5	termccatd	Could not format ( ( C e. TermCat /\ ( Base ` C ) = { x } ) -> C e. Cat ) : No typesetting found for |- ( ( C e. TermCat /\ ( Base ` C ) = { x } ) -> C e. Cat ) with typecode |-
7		eqid	$$⊢\mathrm{Hom}\left(C\right)=\mathrm{Hom}\left(C\right)$$
8		vsnid	$$⊢x\in \left\{x\right\}$$
9		simpr	Could not format ( ( C e. TermCat /\ ( Base ` C ) = { x } ) -> ( Base ` C ) = { x } ) : No typesetting found for |- ( ( C e. TermCat /\ ( Base ` C ) = { x } ) -> ( Base ` C ) = { x } ) with typecode |-
10	8 9	eleqtrrid	Could not format ( ( C e. TermCat /\ ( Base ` C ) = { x } ) -> x e. ( Base ` C ) ) : No typesetting found for |- ( ( C e. TermCat /\ ( Base ` C ) = { x } ) -> x e. ( Base ` C ) ) with typecode |-
11		eqid	$$⊢\mathrm{Id}\left(C\right)=\mathrm{Id}\left(C\right)$$
12	2 7 11 6 10	catidcl	Could not format ( ( C e. TermCat /\ ( Base ` C ) = { x } ) -> ( ( Id ` C ) ` x ) e. ( x ( Hom ` C ) x ) ) : No typesetting found for |- ( ( C e. TermCat /\ ( Base ` C ) = { x } ) -> ( ( Id ` C ) ` x ) e. ( x ( Hom ` C ) x ) ) with typecode |-
13	4 2 6 7 10 10 12	elhomai2	Could not format ( ( C e. TermCat /\ ( Base ` C ) = { x } ) -> <. x , x , ( ( Id ` C ) ` x ) >. e. ( x ( HomA ` C ) x ) ) : No typesetting found for |- ( ( C e. TermCat /\ ( Base ` C ) = { x } ) -> <. x , x , ( ( Id ` C ) ` x ) >. e. ( x ( HomA ` C ) x ) ) with typecode |-
14		eqid	$$⊢\mathrm{Arrow}\left(C\right)=\mathrm{Arrow}\left(C\right)$$
15	14	arwdmcd	$$⊢a\in \mathrm{Arrow}\left(C\right)\to a=⟨{dom}_a\left(a\right),{cod}_a\left(a\right),2^{nd}\left(a\right)⟩$$
16	15	adantl	Could not format ( ( ( C e. TermCat /\ ( Base ` C ) = { x } ) /\ a e. ( Arrow ` C ) ) -> a = <. ( domA ` a ) , ( codA ` a ) , ( 2nd ` a ) >. ) : No typesetting found for |- ( ( ( C e. TermCat /\ ( Base ` C ) = { x } ) /\ a e. ( Arrow ` C ) ) -> a = <. ( domA ` a ) , ( codA ` a ) , ( 2nd ` a ) >. ) with typecode |-
17	5	adantr	Could not format ( ( ( C e. TermCat /\ ( Base ` C ) = { x } ) /\ a e. ( Arrow ` C ) ) -> C e. TermCat ) : No typesetting found for |- ( ( ( C e. TermCat /\ ( Base ` C ) = { x } ) /\ a e. ( Arrow ` C ) ) -> C e. TermCat ) with typecode |-
18	14 2	arwdm	$$⊢a\in \mathrm{Arrow}\left(C\right)\to {dom}_a\left(a\right)\in {\mathrm{Base}}_C$$
19	18	adantl	Could not format ( ( ( C e. TermCat /\ ( Base ` C ) = { x } ) /\ a e. ( Arrow ` C ) ) -> ( domA ` a ) e. ( Base ` C ) ) : No typesetting found for |- ( ( ( C e. TermCat /\ ( Base ` C ) = { x } ) /\ a e. ( Arrow ` C ) ) -> ( domA ` a ) e. ( Base ` C ) ) with typecode |-
20	10	adantr	Could not format ( ( ( C e. TermCat /\ ( Base ` C ) = { x } ) /\ a e. ( Arrow ` C ) ) -> x e. ( Base ` C ) ) : No typesetting found for |- ( ( ( C e. TermCat /\ ( Base ` C ) = { x } ) /\ a e. ( Arrow ` C ) ) -> x e. ( Base ` C ) ) with typecode |-
21	17 2 19 20	termcbasmo	Could not format ( ( ( C e. TermCat /\ ( Base ` C ) = { x } ) /\ a e. ( Arrow ` C ) ) -> ( domA ` a ) = x ) : No typesetting found for |- ( ( ( C e. TermCat /\ ( Base ` C ) = { x } ) /\ a e. ( Arrow ` C ) ) -> ( domA ` a ) = x ) with typecode |-
22	14 2	arwcd	$$⊢a\in \mathrm{Arrow}\left(C\right)\to {cod}_a\left(a\right)\in {\mathrm{Base}}_C$$
23	22	adantl	Could not format ( ( ( C e. TermCat /\ ( Base ` C ) = { x } ) /\ a e. ( Arrow ` C ) ) -> ( codA ` a ) e. ( Base ` C ) ) : No typesetting found for |- ( ( ( C e. TermCat /\ ( Base ` C ) = { x } ) /\ a e. ( Arrow ` C ) ) -> ( codA ` a ) e. ( Base ` C ) ) with typecode |-
24	17 2 23 20	termcbasmo	Could not format ( ( ( C e. TermCat /\ ( Base ` C ) = { x } ) /\ a e. ( Arrow ` C ) ) -> ( codA ` a ) = x ) : No typesetting found for |- ( ( ( C e. TermCat /\ ( Base ` C ) = { x } ) /\ a e. ( Arrow ` C ) ) -> ( codA ` a ) = x ) with typecode |-
25	14 7	arwhom	$$⊢a\in \mathrm{Arrow}\left(C\right)\to 2^{nd}\left(a\right)\in \left({dom}_a\left(a\right)\mathrm{Hom}\left(C\right){cod}_a\left(a\right)\right)$$
26	25	adantl	Could not format ( ( ( C e. TermCat /\ ( Base ` C ) = { x } ) /\ a e. ( Arrow ` C ) ) -> ( 2nd ` a ) e. ( ( domA ` a ) ( Hom ` C ) ( codA ` a ) ) ) : No typesetting found for |- ( ( ( C e. TermCat /\ ( Base ` C ) = { x } ) /\ a e. ( Arrow ` C ) ) -> ( 2nd ` a ) e. ( ( domA ` a ) ( Hom ` C ) ( codA ` a ) ) ) with typecode |-
27	12	adantr	Could not format ( ( ( C e. TermCat /\ ( Base ` C ) = { x } ) /\ a e. ( Arrow ` C ) ) -> ( ( Id ` C ) ` x ) e. ( x ( Hom ` C ) x ) ) : No typesetting found for |- ( ( ( C e. TermCat /\ ( Base ` C ) = { x } ) /\ a e. ( Arrow ` C ) ) -> ( ( Id ` C ) ` x ) e. ( x ( Hom ` C ) x ) ) with typecode |-
28	17 2 19 23 7 26 20 20 27	termchommo	Could not format ( ( ( C e. TermCat /\ ( Base ` C ) = { x } ) /\ a e. ( Arrow ` C ) ) -> ( 2nd ` a ) = ( ( Id ` C ) ` x ) ) : No typesetting found for |- ( ( ( C e. TermCat /\ ( Base ` C ) = { x } ) /\ a e. ( Arrow ` C ) ) -> ( 2nd ` a ) = ( ( Id ` C ) ` x ) ) with typecode |-
29	21 24 28	oteq123d	Could not format ( ( ( C e. TermCat /\ ( Base ` C ) = { x } ) /\ a e. ( Arrow ` C ) ) -> <. ( domA ` a ) , ( codA ` a ) , ( 2nd ` a ) >. = <. x , x , ( ( Id ` C ) ` x ) >. ) : No typesetting found for |- ( ( ( C e. TermCat /\ ( Base ` C ) = { x } ) /\ a e. ( Arrow ` C ) ) -> <. ( domA ` a ) , ( codA ` a ) , ( 2nd ` a ) >. = <. x , x , ( ( Id ` C ) ` x ) >. ) with typecode |-
30	16 29	eqtrd	Could not format ( ( ( C e. TermCat /\ ( Base ` C ) = { x } ) /\ a e. ( Arrow ` C ) ) -> a = <. x , x , ( ( Id ` C ) ` x ) >. ) : No typesetting found for |- ( ( ( C e. TermCat /\ ( Base ` C ) = { x } ) /\ a e. ( Arrow ` C ) ) -> a = <. x , x , ( ( Id ` C ) ` x ) >. ) with typecode |-
31		simpr	Could not format ( ( ( C e. TermCat /\ ( Base ` C ) = { x } ) /\ a = <. x , x , ( ( Id ` C ) ` x ) >. ) -> a = <. x , x , ( ( Id ` C ) ` x ) >. ) : No typesetting found for |- ( ( ( C e. TermCat /\ ( Base ` C ) = { x } ) /\ a = <. x , x , ( ( Id ` C ) ` x ) >. ) -> a = <. x , x , ( ( Id ` C ) ` x ) >. ) with typecode |-
32	14 4	homarw	$$⊢x{Hom}_a\left(C\right)x\subseteq \mathrm{Arrow}\left(C\right)$$
33	32 13	sselid	Could not format ( ( C e. TermCat /\ ( Base ` C ) = { x } ) -> <. x , x , ( ( Id ` C ) ` x ) >. e. ( Arrow ` C ) ) : No typesetting found for |- ( ( C e. TermCat /\ ( Base ` C ) = { x } ) -> <. x , x , ( ( Id ` C ) ` x ) >. e. ( Arrow ` C ) ) with typecode |-
34	33	adantr	Could not format ( ( ( C e. TermCat /\ ( Base ` C ) = { x } ) /\ a = <. x , x , ( ( Id ` C ) ` x ) >. ) -> <. x , x , ( ( Id ` C ) ` x ) >. e. ( Arrow ` C ) ) : No typesetting found for |- ( ( ( C e. TermCat /\ ( Base ` C ) = { x } ) /\ a = <. x , x , ( ( Id ` C ) ` x ) >. ) -> <. x , x , ( ( Id ` C ) ` x ) >. e. ( Arrow ` C ) ) with typecode |-
35	31 34	eqeltrd	Could not format ( ( ( C e. TermCat /\ ( Base ` C ) = { x } ) /\ a = <. x , x , ( ( Id ` C ) ` x ) >. ) -> a e. ( Arrow ` C ) ) : No typesetting found for |- ( ( ( C e. TermCat /\ ( Base ` C ) = { x } ) /\ a = <. x , x , ( ( Id ` C ) ` x ) >. ) -> a e. ( Arrow ` C ) ) with typecode |-
36	30 35	impbida	Could not format ( ( C e. TermCat /\ ( Base ` C ) = { x } ) -> ( a e. ( Arrow ` C ) <-> a = <. x , x , ( ( Id ` C ) ` x ) >. ) ) : No typesetting found for |- ( ( C e. TermCat /\ ( Base ` C ) = { x } ) -> ( a e. ( Arrow ` C ) <-> a = <. x , x , ( ( Id ` C ) ` x ) >. ) ) with typecode |-
37	36	alrimiv	Could not format ( ( C e. TermCat /\ ( Base ` C ) = { x } ) -> A. a ( a e. ( Arrow ` C ) <-> a = <. x , x , ( ( Id ` C ) ` x ) >. ) ) : No typesetting found for |- ( ( C e. TermCat /\ ( Base ` C ) = { x } ) -> A. a ( a e. ( Arrow ` C ) <-> a = <. x , x , ( ( Id ` C ) ` x ) >. ) ) with typecode |-
38		eqeq2	$$⊢b=⟨x,x,\mathrm{Id}\left(C\right)\left(x\right)⟩\to \left(a=b\leftrightarrow a=⟨x,x,\mathrm{Id}\left(C\right)\left(x\right)⟩\right)$$
39	38	bibi2d	$$⊢b=⟨x,x,\mathrm{Id}\left(C\right)\left(x\right)⟩\to \left(\left(a\in \mathrm{Arrow}\left(C\right)\leftrightarrow a=b\right)\leftrightarrow \left(a\in \mathrm{Arrow}\left(C\right)\leftrightarrow a=⟨x,x,\mathrm{Id}\left(C\right)\left(x\right)⟩\right)\right)$$
40	39	albidv	$$⊢b=⟨x,x,\mathrm{Id}\left(C\right)\left(x\right)⟩\to \left(\forall a\left(a\in \mathrm{Arrow}\left(C\right)\leftrightarrow a=b\right)\leftrightarrow \forall a\left(a\in \mathrm{Arrow}\left(C\right)\leftrightarrow a=⟨x,x,\mathrm{Id}\left(C\right)\left(x\right)⟩\right)\right)$$
41	13 37 40	spcedv	Could not format ( ( C e. TermCat /\ ( Base ` C ) = { x } ) -> E. b A. a ( a e. ( Arrow ` C ) <-> a = b ) ) : No typesetting found for |- ( ( C e. TermCat /\ ( Base ` C ) = { x } ) -> E. b A. a ( a e. ( Arrow ` C ) <-> a = b ) ) with typecode |-
42	3 41	exlimddv	Could not format ( C e. TermCat -> E. b A. a ( a e. ( Arrow ` C ) <-> a = b ) ) : No typesetting found for |- ( C e. TermCat -> E. b A. a ( a e. ( Arrow ` C ) <-> a = b ) ) with typecode |-
43		eu6im	$$⊢\exists b\forall a\left(a\in \mathrm{Arrow}\left(C\right)\leftrightarrow a=b\right)\to \exists !aa\in \mathrm{Arrow}\left(C\right)$$
44	42 43	syl	Could not format ( C e. TermCat -> E! a a e. ( Arrow ` C ) ) : No typesetting found for |- ( C e. TermCat -> E! a a e. ( Arrow ` C ) ) with typecode |-