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

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 ( 𝐶 ∈ 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 ‘ 𝐶 ) )