Metamath Proof Explorer

Theorem arweutermc

Description: If a structure has a unique disjointified arrow, then the structure is a terminal category. (Contributed by Zhi Wang, 20-Oct-2025)

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

Proof

Step Hyp Ref Expression
1 arweuthinc ⊢ ( ∃! 𝑎 𝑎 ∈ ( Arrow ‘ 𝐶 ) → 𝐶 ∈ ThinCat )
2 euex ⊢ ( ∃! 𝑎 𝑎 ∈ ( Arrow ‘ 𝐶 ) → ∃ 𝑎 𝑎 ∈ ( Arrow ‘ 𝐶 ) )
3 eqid ⊢ ( Arrow ‘ 𝐶 ) = ( Arrow ‘ 𝐶 )
4 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
5 3 4 arwdm ⊢ ( 𝑎 ∈ ( Arrow ‘ 𝐶 ) → ( doma ‘ 𝑎 ) ∈ ( Base ‘ 𝐶 ) )
6 eleq1 ⊢ ( 𝑥 = ( doma ‘ 𝑎 ) → ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↔ ( doma ‘ 𝑎 ) ∈ ( Base ‘ 𝐶 ) ) )
7 5 5 6 spcedv ⊢ ( 𝑎 ∈ ( Arrow ‘ 𝐶 ) → ∃ 𝑥 𝑥 ∈ ( Base ‘ 𝐶 ) )
8 7 exlimiv ⊢ ( ∃ 𝑎 𝑎 ∈ ( Arrow ‘ 𝐶 ) → ∃ 𝑥 𝑥 ∈ ( Base ‘ 𝐶 ) )
9 2 8 syl ⊢ ( ∃! 𝑎 𝑎 ∈ ( Arrow ‘ 𝐶 ) → ∃ 𝑥 𝑥 ∈ ( Base ‘ 𝐶 ) )
10 eqeq1 ⊢ ( 𝑎 = ⟨ 𝑥 , 𝑥 , ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ⟩ → ( 𝑎 = 𝑏 ↔ ⟨ 𝑥 , 𝑥 , ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ⟩ = 𝑏 ) )
11 eqeq2 ⊢ ( 𝑏 = ⟨ 𝑦 , 𝑦 , ( ( Id ‘ 𝐶 ) ‘ 𝑦 ) ⟩ → ( ⟨ 𝑥 , 𝑥 , ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ⟩ = 𝑏 ↔ ⟨ 𝑥 , 𝑥 , ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ⟩ = ⟨ 𝑦 , 𝑦 , ( ( Id ‘ 𝐶 ) ‘ 𝑦 ) ⟩ ) )
12 eumo ⊢ ( ∃! 𝑎 𝑎 ∈ ( Arrow ‘ 𝐶 ) → ∃* 𝑎 𝑎 ∈ ( Arrow ‘ 𝐶 ) )
13 12 adantr ⊢ ( ( ∃! 𝑎 𝑎 ∈ ( Arrow ‘ 𝐶 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ∃* 𝑎 𝑎 ∈ ( Arrow ‘ 𝐶 ) )
14 moel ⊢ ( ∃* 𝑎 𝑎 ∈ ( Arrow ‘ 𝐶 ) ↔ ∀ 𝑎 ∈ ( Arrow ‘ 𝐶 ) ∀ 𝑏 ∈ ( Arrow ‘ 𝐶 ) 𝑎 = 𝑏 )
15 13 14 sylib ⊢ ( ( ∃! 𝑎 𝑎 ∈ ( Arrow ‘ 𝐶 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ∀ 𝑎 ∈ ( Arrow ‘ 𝐶 ) ∀ 𝑏 ∈ ( Arrow ‘ 𝐶 ) 𝑎 = 𝑏 )
16 eqid ⊢ ( Homa ‘ 𝐶 ) = ( Homa ‘ 𝐶 )
17 3 16 homarw ⊢ ( 𝑥 ( Homa ‘ 𝐶 ) 𝑥 ) ⊆ ( Arrow ‘ 𝐶 )
18 1 adantr ⊢ ( ( ∃! 𝑎 𝑎 ∈ ( Arrow ‘ 𝐶 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → 𝐶 ∈ ThinCat )
19 18 thinccd ⊢ ( ( ∃! 𝑎 𝑎 ∈ ( Arrow ‘ 𝐶 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → 𝐶 ∈ Cat )
20 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
21 simprl ⊢ ( ( ∃! 𝑎 𝑎 ∈ ( Arrow ‘ 𝐶 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
22 eqid ⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
23 4 20 22 19 21 catidcl ⊢ ( ( ∃! 𝑎 𝑎 ∈ ( Arrow ‘ 𝐶 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) )
24 16 4 19 20 21 21 23 elhomai2 ⊢ ( ( ∃! 𝑎 𝑎 ∈ ( Arrow ‘ 𝐶 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ⟨ 𝑥 , 𝑥 , ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ⟩ ∈ ( 𝑥 ( Homa ‘ 𝐶 ) 𝑥 ) )
25 17 24 sselid ⊢ ( ( ∃! 𝑎 𝑎 ∈ ( Arrow ‘ 𝐶 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ⟨ 𝑥 , 𝑥 , ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ⟩ ∈ ( Arrow ‘ 𝐶 ) )
26 3 16 homarw ⊢ ( 𝑦 ( Homa ‘ 𝐶 ) 𝑦 ) ⊆ ( Arrow ‘ 𝐶 )
27 simprr ⊢ ( ( ∃! 𝑎 𝑎 ∈ ( Arrow ‘ 𝐶 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑦 ∈ ( Base ‘ 𝐶 ) )
28 4 20 22 19 27 catidcl ⊢ ( ( ∃! 𝑎 𝑎 ∈ ( Arrow ‘ 𝐶 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( Id ‘ 𝐶 ) ‘ 𝑦 ) ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑦 ) )
29 16 4 19 20 27 27 28 elhomai2 ⊢ ( ( ∃! 𝑎 𝑎 ∈ ( Arrow ‘ 𝐶 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ⟨ 𝑦 , 𝑦 , ( ( Id ‘ 𝐶 ) ‘ 𝑦 ) ⟩ ∈ ( 𝑦 ( Homa ‘ 𝐶 ) 𝑦 ) )
30 26 29 sselid ⊢ ( ( ∃! 𝑎 𝑎 ∈ ( Arrow ‘ 𝐶 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ⟨ 𝑦 , 𝑦 , ( ( Id ‘ 𝐶 ) ‘ 𝑦 ) ⟩ ∈ ( Arrow ‘ 𝐶 ) )
31 10 11 15 25 30 rspc2dv ⊢ ( ( ∃! 𝑎 𝑎 ∈ ( Arrow ‘ 𝐶 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ⟨ 𝑥 , 𝑥 , ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ⟩ = ⟨ 𝑦 , 𝑦 , ( ( Id ‘ 𝐶 ) ‘ 𝑦 ) ⟩ )
32 vex ⊢ 𝑥 ∈ V
33 fvex ⊢ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ V
34 32 32 33 otth ⊢ ( ⟨ 𝑥 , 𝑥 , ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ⟩ = ⟨ 𝑦 , 𝑦 , ( ( Id ‘ 𝐶 ) ‘ 𝑦 ) ⟩ ↔ ( 𝑥 = 𝑦 ∧ 𝑥 = 𝑦 ∧ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑦 ) ) )
35 34 simp1bi ⊢ ( ⟨ 𝑥 , 𝑥 , ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ⟩ = ⟨ 𝑦 , 𝑦 , ( ( Id ‘ 𝐶 ) ‘ 𝑦 ) ⟩ → 𝑥 = 𝑦 )
36 31 35 syl ⊢ ( ( ∃! 𝑎 𝑎 ∈ ( Arrow ‘ 𝐶 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑥 = 𝑦 )
37 36 ralrimivva ⊢ ( ∃! 𝑎 𝑎 ∈ ( Arrow ‘ 𝐶 ) → ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) 𝑥 = 𝑦 )
38 moel ⊢ ( ∃* 𝑥 𝑥 ∈ ( Base ‘ 𝐶 ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) 𝑥 = 𝑦 )
39 37 38 sylibr ⊢ ( ∃! 𝑎 𝑎 ∈ ( Arrow ‘ 𝐶 ) → ∃* 𝑥 𝑥 ∈ ( Base ‘ 𝐶 ) )
40 df-eu ⊢ ( ∃! 𝑥 𝑥 ∈ ( Base ‘ 𝐶 ) ↔ ( ∃ 𝑥 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ ∃* 𝑥 𝑥 ∈ ( Base ‘ 𝐶 ) ) )
41 9 39 40 sylanbrc ⊢ ( ∃! 𝑎 𝑎 ∈ ( Arrow ‘ 𝐶 ) → ∃! 𝑥 𝑥 ∈ ( Base ‘ 𝐶 ) )
42 4 istermc2 ⊢ ( 𝐶 ∈ TermCat ↔ ( 𝐶 ∈ ThinCat ∧ ∃! 𝑥 𝑥 ∈ ( Base ‘ 𝐶 ) ) )
43 1 41 42 sylanbrc ⊢ ( ∃! 𝑎 𝑎 ∈ ( Arrow ‘ 𝐶 ) → 𝐶 ∈ TermCat )