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	Could not format assertion : No typesetting found for \|- ( E! a a e. ( Arrow ` C ) -> C e. TermCat ) with typecode \|-

Proof

Step	Hyp	Ref	Expression
1		arweuthinc	$⊢ \exists! a a \in Arrow (C) \to C \in ThinCat$
2		euex	$⊢ \exists! a a \in Arrow (C) \to \exists a a \in Arrow (C)$
3		eqid	$⊢ Arrow (C) = Arrow (C)$
4		eqid	$⊢ {Base}_{C} = {Base}_{C}$
5	3 4	arwdm	$⊢ a \in Arrow (C) \to {dom}_{a} (a) \in {Base}_{C}$
6		eleq1	$⊢ x = {dom}_{a} (a) \to (x \in {Base}_{C} \leftrightarrow {dom}_{a} (a) \in {Base}_{C})$
7	5 5 6	spcedv	$⊢ a \in Arrow (C) \to \exists x x \in {Base}_{C}$
8	7	exlimiv	$⊢ \exists a a \in Arrow (C) \to \exists x x \in {Base}_{C}$
9	2 8	syl	$⊢ \exists! a a \in Arrow (C) \to \exists x x \in {Base}_{C}$
10		eqeq1	$⊢ a = ⟨x, x, Id (C) (x)⟩ \to (a = b \leftrightarrow ⟨x, x, Id (C) (x)⟩ = b)$
11		eqeq2	$⊢ b = ⟨y, y, Id (C) (y)⟩ \to (⟨x, x, Id (C) (x)⟩ = b \leftrightarrow ⟨x, x, Id (C) (x)⟩ = ⟨y, y, Id (C) (y)⟩)$
12		eumo	$⊢ \exists! a a \in Arrow (C) \to \exists^{*} a a \in Arrow (C)$
13	12	adantr	$⊢ (\exists! a a \in Arrow (C) \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to \exists^{*} a a \in Arrow (C)$
14		moel	$⊢ \exists^{*} a a \in Arrow (C) \leftrightarrow \forall a \in Arrow (C) \forall b \in Arrow (C) a = b$
15	13 14	sylib	$⊢ (\exists! a a \in Arrow (C) \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to \forall a \in Arrow (C) \forall b \in Arrow (C) a = b$
16		eqid	$⊢ {Hom}_{a} (C) = {Hom}_{a} (C)$
17	3 16	homarw	$⊢ x {Hom}_{a} (C) x \subseteq Arrow (C)$
18	1	adantr	$⊢ (\exists! a a \in Arrow (C) \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to C \in ThinCat$
19	18	thinccatd	$⊢ (\exists! a a \in Arrow (C) \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to C \in Cat$
20		eqid	$⊢ Hom (C) = Hom (C)$
21		simprl	$⊢ (\exists! a a \in Arrow (C) \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to x \in {Base}_{C}$
22		eqid	$⊢ Id (C) = Id (C)$
23	4 20 22 19 21	catidcl	$⊢ (\exists! a a \in Arrow (C) \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to Id (C) (x) \in (x Hom (C) x)$
24	16 4 19 20 21 21 23	elhomai2	$⊢ (\exists! a a \in Arrow (C) \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to ⟨x, x, Id (C) (x)⟩ \in (x {Hom}_{a} (C) x)$
25	17 24	sselid	$⊢ (\exists! a a \in Arrow (C) \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to ⟨x, x, Id (C) (x)⟩ \in Arrow (C)$
26	3 16	homarw	$⊢ y {Hom}_{a} (C) y \subseteq Arrow (C)$
27		simprr	$⊢ (\exists! a a \in Arrow (C) \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to y \in {Base}_{C}$
28	4 20 22 19 27	catidcl	$⊢ (\exists! a a \in Arrow (C) \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to Id (C) (y) \in (y Hom (C) y)$
29	16 4 19 20 27 27 28	elhomai2	$⊢ (\exists! a a \in Arrow (C) \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to ⟨y, y, Id (C) (y)⟩ \in (y {Hom}_{a} (C) y)$
30	26 29	sselid	$⊢ (\exists! a a \in Arrow (C) \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to ⟨y, y, Id (C) (y)⟩ \in Arrow (C)$
31	10 11 15 25 30	rspc2dv	$⊢ (\exists! a a \in Arrow (C) \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to ⟨x, x, Id (C) (x)⟩ = ⟨y, y, Id (C) (y)⟩$
32		vex	$⊢ x \in V$
33		fvex	$⊢ Id (C) (x) \in V$
34	32 32 33	otth	$⊢ ⟨x, x, Id (C) (x)⟩ = ⟨y, y, Id (C) (y)⟩ \leftrightarrow (x = y \land x = y \land Id (C) (x) = Id (C) (y))$
35	34	simp1bi	$⊢ ⟨x, x, Id (C) (x)⟩ = ⟨y, y, Id (C) (y)⟩ \to x = y$
36	31 35	syl	$⊢ (\exists! a a \in Arrow (C) \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to x = y$
37	36	ralrimivva	$⊢ \exists! a a \in Arrow (C) \to \forall x \in {Base}_{C} \forall y \in {Base}_{C} x = y$
38		moel	$⊢ \exists^{*} x x \in {Base}_{C} \leftrightarrow \forall x \in {Base}_{C} \forall y \in {Base}_{C} x = y$
39	37 38	sylibr	$⊢ \exists! a a \in Arrow (C) \to \exists^{*} x x \in {Base}_{C}$
40		df-eu	$⊢ \exists! x x \in {Base}_{C} \leftrightarrow (\exists x x \in {Base}_{C} \land \exists^{*} x x \in {Base}_{C})$
41	9 39 40	sylanbrc	$⊢ \exists! a a \in Arrow (C) \to \exists! x x \in {Base}_{C}$
42	4	istermc2	Could not format ( C e. TermCat <-> ( C e. ThinCat /\ E! x x e. ( Base ` C ) ) ) : No typesetting found for \|- ( C e. TermCat <-> ( C e. ThinCat /\ E! x x e. ( Base ` C ) ) ) with typecode \|-
43	1 41 42	sylanbrc	Could not format ( E! a a e. ( Arrow ` C ) -> C e. TermCat ) : No typesetting found for \|- ( E! a a e. ( Arrow ` C ) -> C e. TermCat ) with typecode \|-

Metamath Proof Explorer

Theorem arweutermc

Proof