Theorem termcarweu

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

	Ref	Expression
Assertion	termcarweu	⊢ ( 𝐶 ∈ TermCat → ∃! 𝑎 𝑎 ∈ ( Arrow ‘ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		id	⊢ ( 𝐶 ∈ TermCat → 𝐶 ∈ TermCat )
2		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
3	1 2	termcbas	⊢ ( 𝐶 ∈ TermCat → ∃ 𝑥 ( Base ‘ 𝐶 ) = { 𝑥 } )
4		eqid	⊢ ( Homa ‘ 𝐶 ) = ( Homa ‘ 𝐶 )
5	1	adantr	⊢ ( ( 𝐶 ∈ TermCat ∧ ( Base ‘ 𝐶 ) = { 𝑥 } ) → 𝐶 ∈ TermCat )
6	5	termccd	⊢ ( ( 𝐶 ∈ TermCat ∧ ( Base ‘ 𝐶 ) = { 𝑥 } ) → 𝐶 ∈ Cat )
7		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
8		vsnid	⊢ 𝑥 ∈ { 𝑥 }
9		simpr	⊢ ( ( 𝐶 ∈ TermCat ∧ ( Base ‘ 𝐶 ) = { 𝑥 } ) → ( Base ‘ 𝐶 ) = { 𝑥 } )
10	8 9	eleqtrrid	⊢ ( ( 𝐶 ∈ TermCat ∧ ( Base ‘ 𝐶 ) = { 𝑥 } ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
11		eqid	⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
12	2 7 11 6 10	catidcl	⊢ ( ( 𝐶 ∈ TermCat ∧ ( Base ‘ 𝐶 ) = { 𝑥 } ) → ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) )
13	4 2 6 7 10 10 12	elhomai2	⊢ ( ( 𝐶 ∈ TermCat ∧ ( Base ‘ 𝐶 ) = { 𝑥 } ) → ⟨ 𝑥 , 𝑥 , ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ⟩ ∈ ( 𝑥 ( Homa ‘ 𝐶 ) 𝑥 ) )
14		eqid	⊢ ( Arrow ‘ 𝐶 ) = ( Arrow ‘ 𝐶 )
15	14	arwdmcd	⊢ ( 𝑎 ∈ ( Arrow ‘ 𝐶 ) → 𝑎 = ⟨ ( doma ‘ 𝑎 ) , ( coda ‘ 𝑎 ) , ( 2nd ‘ 𝑎 ) ⟩ )
16	15	adantl	⊢ ( ( ( 𝐶 ∈ TermCat ∧ ( Base ‘ 𝐶 ) = { 𝑥 } ) ∧ 𝑎 ∈ ( Arrow ‘ 𝐶 ) ) → 𝑎 = ⟨ ( doma ‘ 𝑎 ) , ( coda ‘ 𝑎 ) , ( 2nd ‘ 𝑎 ) ⟩ )
17	5	adantr	⊢ ( ( ( 𝐶 ∈ TermCat ∧ ( Base ‘ 𝐶 ) = { 𝑥 } ) ∧ 𝑎 ∈ ( Arrow ‘ 𝐶 ) ) → 𝐶 ∈ TermCat )
18	14 2	arwdm	⊢ ( 𝑎 ∈ ( Arrow ‘ 𝐶 ) → ( doma ‘ 𝑎 ) ∈ ( Base ‘ 𝐶 ) )
19	18	adantl	⊢ ( ( ( 𝐶 ∈ TermCat ∧ ( Base ‘ 𝐶 ) = { 𝑥 } ) ∧ 𝑎 ∈ ( Arrow ‘ 𝐶 ) ) → ( doma ‘ 𝑎 ) ∈ ( Base ‘ 𝐶 ) )
20	10	adantr	⊢ ( ( ( 𝐶 ∈ TermCat ∧ ( Base ‘ 𝐶 ) = { 𝑥 } ) ∧ 𝑎 ∈ ( Arrow ‘ 𝐶 ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
21	17 2 19 20	termcbasmo	⊢ ( ( ( 𝐶 ∈ TermCat ∧ ( Base ‘ 𝐶 ) = { 𝑥 } ) ∧ 𝑎 ∈ ( Arrow ‘ 𝐶 ) ) → ( doma ‘ 𝑎 ) = 𝑥 )
22	14 2	arwcd	⊢ ( 𝑎 ∈ ( Arrow ‘ 𝐶 ) → ( coda ‘ 𝑎 ) ∈ ( Base ‘ 𝐶 ) )
23	22	adantl	⊢ ( ( ( 𝐶 ∈ TermCat ∧ ( Base ‘ 𝐶 ) = { 𝑥 } ) ∧ 𝑎 ∈ ( Arrow ‘ 𝐶 ) ) → ( coda ‘ 𝑎 ) ∈ ( Base ‘ 𝐶 ) )
24	17 2 23 20	termcbasmo	⊢ ( ( ( 𝐶 ∈ TermCat ∧ ( Base ‘ 𝐶 ) = { 𝑥 } ) ∧ 𝑎 ∈ ( Arrow ‘ 𝐶 ) ) → ( coda ‘ 𝑎 ) = 𝑥 )
25	14 7	arwhom	⊢ ( 𝑎 ∈ ( Arrow ‘ 𝐶 ) → ( 2nd ‘ 𝑎 ) ∈ ( ( doma ‘ 𝑎 ) ( Hom ‘ 𝐶 ) ( coda ‘ 𝑎 ) ) )
26	25	adantl	⊢ ( ( ( 𝐶 ∈ TermCat ∧ ( Base ‘ 𝐶 ) = { 𝑥 } ) ∧ 𝑎 ∈ ( Arrow ‘ 𝐶 ) ) → ( 2nd ‘ 𝑎 ) ∈ ( ( doma ‘ 𝑎 ) ( Hom ‘ 𝐶 ) ( coda ‘ 𝑎 ) ) )
27	12	adantr	⊢ ( ( ( 𝐶 ∈ TermCat ∧ ( Base ‘ 𝐶 ) = { 𝑥 } ) ∧ 𝑎 ∈ ( Arrow ‘ 𝐶 ) ) → ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) )
28	17 2 19 23 7 26 20 20 27	termchommo	⊢ ( ( ( 𝐶 ∈ TermCat ∧ ( Base ‘ 𝐶 ) = { 𝑥 } ) ∧ 𝑎 ∈ ( Arrow ‘ 𝐶 ) ) → ( 2nd ‘ 𝑎 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) )
29	21 24 28	oteq123d	⊢ ( ( ( 𝐶 ∈ TermCat ∧ ( Base ‘ 𝐶 ) = { 𝑥 } ) ∧ 𝑎 ∈ ( Arrow ‘ 𝐶 ) ) → ⟨ ( doma ‘ 𝑎 ) , ( coda ‘ 𝑎 ) , ( 2nd ‘ 𝑎 ) ⟩ = ⟨ 𝑥 , 𝑥 , ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ⟩ )
30	16 29	eqtrd	⊢ ( ( ( 𝐶 ∈ TermCat ∧ ( Base ‘ 𝐶 ) = { 𝑥 } ) ∧ 𝑎 ∈ ( Arrow ‘ 𝐶 ) ) → 𝑎 = ⟨ 𝑥 , 𝑥 , ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ⟩ )
31		simpr	⊢ ( ( ( 𝐶 ∈ TermCat ∧ ( Base ‘ 𝐶 ) = { 𝑥 } ) ∧ 𝑎 = ⟨ 𝑥 , 𝑥 , ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ⟩ ) → 𝑎 = ⟨ 𝑥 , 𝑥 , ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ⟩ )
32	14 4	homarw	⊢ ( 𝑥 ( Homa ‘ 𝐶 ) 𝑥 ) ⊆ ( Arrow ‘ 𝐶 )
33	32 13	sselid	⊢ ( ( 𝐶 ∈ TermCat ∧ ( Base ‘ 𝐶 ) = { 𝑥 } ) → ⟨ 𝑥 , 𝑥 , ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ⟩ ∈ ( Arrow ‘ 𝐶 ) )
34	33	adantr	⊢ ( ( ( 𝐶 ∈ TermCat ∧ ( Base ‘ 𝐶 ) = { 𝑥 } ) ∧ 𝑎 = ⟨ 𝑥 , 𝑥 , ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ⟩ ) → ⟨ 𝑥 , 𝑥 , ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ⟩ ∈ ( Arrow ‘ 𝐶 ) )
35	31 34	eqeltrd	⊢ ( ( ( 𝐶 ∈ TermCat ∧ ( Base ‘ 𝐶 ) = { 𝑥 } ) ∧ 𝑎 = ⟨ 𝑥 , 𝑥 , ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ⟩ ) → 𝑎 ∈ ( Arrow ‘ 𝐶 ) )
36	30 35	impbida	⊢ ( ( 𝐶 ∈ TermCat ∧ ( Base ‘ 𝐶 ) = { 𝑥 } ) → ( 𝑎 ∈ ( Arrow ‘ 𝐶 ) ↔ 𝑎 = ⟨ 𝑥 , 𝑥 , ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ⟩ ) )
37	36	alrimiv	⊢ ( ( 𝐶 ∈ TermCat ∧ ( Base ‘ 𝐶 ) = { 𝑥 } ) → ∀ 𝑎 ( 𝑎 ∈ ( Arrow ‘ 𝐶 ) ↔ 𝑎 = ⟨ 𝑥 , 𝑥 , ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ⟩ ) )
38		eqeq2	⊢ ( 𝑏 = ⟨ 𝑥 , 𝑥 , ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ⟩ → ( 𝑎 = 𝑏 ↔ 𝑎 = ⟨ 𝑥 , 𝑥 , ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ⟩ ) )
39	38	bibi2d	⊢ ( 𝑏 = ⟨ 𝑥 , 𝑥 , ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ⟩ → ( ( 𝑎 ∈ ( Arrow ‘ 𝐶 ) ↔ 𝑎 = 𝑏 ) ↔ ( 𝑎 ∈ ( Arrow ‘ 𝐶 ) ↔ 𝑎 = ⟨ 𝑥 , 𝑥 , ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ⟩ ) ) )
40	39	albidv	⊢ ( 𝑏 = ⟨ 𝑥 , 𝑥 , ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ⟩ → ( ∀ 𝑎 ( 𝑎 ∈ ( Arrow ‘ 𝐶 ) ↔ 𝑎 = 𝑏 ) ↔ ∀ 𝑎 ( 𝑎 ∈ ( Arrow ‘ 𝐶 ) ↔ 𝑎 = ⟨ 𝑥 , 𝑥 , ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ⟩ ) ) )
41	13 37 40	spcedv	⊢ ( ( 𝐶 ∈ TermCat ∧ ( Base ‘ 𝐶 ) = { 𝑥 } ) → ∃ 𝑏 ∀ 𝑎 ( 𝑎 ∈ ( Arrow ‘ 𝐶 ) ↔ 𝑎 = 𝑏 ) )
42	3 41	exlimddv	⊢ ( 𝐶 ∈ TermCat → ∃ 𝑏 ∀ 𝑎 ( 𝑎 ∈ ( Arrow ‘ 𝐶 ) ↔ 𝑎 = 𝑏 ) )
43		eu6im	⊢ ( ∃ 𝑏 ∀ 𝑎 ( 𝑎 ∈ ( Arrow ‘ 𝐶 ) ↔ 𝑎 = 𝑏 ) → ∃! 𝑎 𝑎 ∈ ( Arrow ‘ 𝐶 ) )
44	42 43	syl	⊢ ( 𝐶 ∈ TermCat → ∃! 𝑎 𝑎 ∈ ( Arrow ‘ 𝐶 ) )