Metamath Proof Explorer

Theorem arweuthinc

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

Ref Expression
Assertion arweuthinc ⊢ ∃! a a ∈ Arrow ⁡ C → C ∈ ThinCat

Proof

Step Hyp Ref Expression
1 eqidd ⊢ ∃! a a ∈ Arrow ⁡ C → Base C = Base C
2 eqidd ⊢ ∃! a a ∈ Arrow ⁡ C → Hom ⁡ C = Hom ⁡ C
3 eqeq1 ⊢ a = x y f → a = b ↔ x y f = b
4 eqeq2 ⊢ b = x y g → x y f = b ↔ x y f = x y g
5 eumo ⊢ ∃! a a ∈ Arrow ⁡ C → ∃* a a ∈ Arrow ⁡ C
6 5 ad2antrr ⊢ ∃! a a ∈ Arrow ⁡ C ∧ x ∈ Base C ∧ y ∈ Base C ∧ f ∈ x Hom ⁡ C y ∧ g ∈ x Hom ⁡ C y → ∃* a a ∈ Arrow ⁡ C
7 moel ⊢ ∃* a a ∈ Arrow ⁡ C ↔ ∀ a ∈ Arrow ⁡ C ∀ b ∈ Arrow ⁡ C a = b
8 6 7 sylib ⊢ ∃! a a ∈ Arrow ⁡ C ∧ x ∈ Base C ∧ y ∈ Base C ∧ f ∈ x Hom ⁡ C y ∧ g ∈ x Hom ⁡ C y → ∀ a ∈ Arrow ⁡ C ∀ b ∈ Arrow ⁡ C a = b
9 eqid ⊢ Arrow ⁡ C = Arrow ⁡ C
10 eqid ⊢ Hom a ⁡ C = Hom a ⁡ C
11 9 10 homarw ⊢ x Hom a ⁡ C y ⊆ Arrow ⁡ C
12 eqid ⊢ Base C = Base C
13 euex ⊢ ∃! a a ∈ Arrow ⁡ C → ∃ a a ∈ Arrow ⁡ C
14 9 arwrcl ⊢ a ∈ Arrow ⁡ C → C ∈ Cat
15 14 exlimiv ⊢ ∃ a a ∈ Arrow ⁡ C → C ∈ Cat
16 13 15 syl ⊢ ∃! a a ∈ Arrow ⁡ C → C ∈ Cat
17 16 ad2antrr ⊢ ∃! a a ∈ Arrow ⁡ C ∧ x ∈ Base C ∧ y ∈ Base C ∧ f ∈ x Hom ⁡ C y ∧ g ∈ x Hom ⁡ C y → C ∈ Cat
18 eqid ⊢ Hom ⁡ C = Hom ⁡ C
19 simplrl ⊢ ∃! a a ∈ Arrow ⁡ C ∧ x ∈ Base C ∧ y ∈ Base C ∧ f ∈ x Hom ⁡ C y ∧ g ∈ x Hom ⁡ C y → x ∈ Base C
20 simplrr ⊢ ∃! a a ∈ Arrow ⁡ C ∧ x ∈ Base C ∧ y ∈ Base C ∧ f ∈ x Hom ⁡ C y ∧ g ∈ x Hom ⁡ C y → y ∈ Base C
21 simprl ⊢ ∃! a a ∈ Arrow ⁡ C ∧ x ∈ Base C ∧ y ∈ Base C ∧ f ∈ x Hom ⁡ C y ∧ g ∈ x Hom ⁡ C y → f ∈ x Hom ⁡ C y
22 10 12 17 18 19 20 21 elhomai2 ⊢ ∃! a a ∈ Arrow ⁡ C ∧ x ∈ Base C ∧ y ∈ Base C ∧ f ∈ x Hom ⁡ C y ∧ g ∈ x Hom ⁡ C y → x y f ∈ x Hom a ⁡ C y
23 11 22 sselid ⊢ ∃! a a ∈ Arrow ⁡ C ∧ x ∈ Base C ∧ y ∈ Base C ∧ f ∈ x Hom ⁡ C y ∧ g ∈ x Hom ⁡ C y → x y f ∈ Arrow ⁡ C
24 simprr ⊢ ∃! a a ∈ Arrow ⁡ C ∧ x ∈ Base C ∧ y ∈ Base C ∧ f ∈ x Hom ⁡ C y ∧ g ∈ x Hom ⁡ C y → g ∈ x Hom ⁡ C y
25 10 12 17 18 19 20 24 elhomai2 ⊢ ∃! a a ∈ Arrow ⁡ C ∧ x ∈ Base C ∧ y ∈ Base C ∧ f ∈ x Hom ⁡ C y ∧ g ∈ x Hom ⁡ C y → x y g ∈ x Hom a ⁡ C y
26 11 25 sselid ⊢ ∃! a a ∈ Arrow ⁡ C ∧ x ∈ Base C ∧ y ∈ Base C ∧ f ∈ x Hom ⁡ C y ∧ g ∈ x Hom ⁡ C y → x y g ∈ Arrow ⁡ C
27 3 4 8 23 26 rspc2dv ⊢ ∃! a a ∈ Arrow ⁡ C ∧ x ∈ Base C ∧ y ∈ Base C ∧ f ∈ x Hom ⁡ C y ∧ g ∈ x Hom ⁡ C y → x y f = x y g
28 vex ⊢ x ∈ V
29 vex ⊢ y ∈ V
30 vex ⊢ f ∈ V
31 28 29 30 otth ⊢ x y f = x y g ↔ x = x ∧ y = y ∧ f = g
32 31 simp3bi ⊢ x y f = x y g → f = g
33 27 32 syl ⊢ ∃! a a ∈ Arrow ⁡ C ∧ x ∈ Base C ∧ y ∈ Base C ∧ f ∈ x Hom ⁡ C y ∧ g ∈ x Hom ⁡ C y → f = g
34 33 ralrimivva ⊢ ∃! a a ∈ Arrow ⁡ C ∧ x ∈ Base C ∧ y ∈ Base C → ∀ f ∈ x Hom ⁡ C y ∀ g ∈ x Hom ⁡ C y f = g
35 moel ⊢ ∃* f f ∈ x Hom ⁡ C y ↔ ∀ f ∈ x Hom ⁡ C y ∀ g ∈ x Hom ⁡ C y f = g
36 34 35 sylibr ⊢ ∃! a a ∈ Arrow ⁡ C ∧ x ∈ Base C ∧ y ∈ Base C → ∃* f f ∈ x Hom ⁡ C y
37 1 2 36 16 isthincd ⊢ ∃! a a ∈ Arrow ⁡ C → C ∈ ThinCat