prsthinc

Description: Preordered sets as categories. Similar to example 3.3(4.d) of Adamek p. 24, but the hom-sets are not pairwise disjoint. One can define a functor from the category of prosets to the category of small thin categories. See catprs and catprs2 for inducing a preorder from a category. Example 3.26(2) of Adamek p. 33 indicates that it induces a bijection from the equivalence class of isomorphic small thin categories to the equivalence class of order-isomorphic preordered sets. (Contributed by Zhi Wang, 18-Sep-2024)

	Ref	Expression
Hypotheses	indthinc.b	$⊢ φ \to B = {Base}_{C}$
	prsthinc.h	$⊢ φ \to \underset{˙}{\leq} \times \{1_{𝑜}\} = Hom (C)$
	prsthinc.o	$⊢ φ \to \emptyset = comp (C)$
	prsthinc.l	$⊢ φ \to \underset{˙}{\leq} = \leq_{C}$
	prsthinc.p	$⊢ φ \to C \in Proset$
Assertion	prsthinc	$⊢ φ \to (C \in ThinCat \land Id (C) = (y \in B ⟼ \emptyset))$

Proof

Step	Hyp	Ref	Expression
1		indthinc.b	$⊢ φ \to B = {Base}_{C}$
2		prsthinc.h	$⊢ φ \to \underset{˙}{\leq} \times \{1_{𝑜}\} = Hom (C)$
3		prsthinc.o	$⊢ φ \to \emptyset = comp (C)$
4		prsthinc.l	$⊢ φ \to \underset{˙}{\leq} = \leq_{C}$
5		prsthinc.p	$⊢ φ \to C \in Proset$
6		eqidd	$⊢ (φ \land (x \in B \land y \in B)) \to \underset{˙}{\leq} \times \{1_{𝑜}\} = \underset{˙}{\leq} \times \{1_{𝑜}\}$
7	6	f1omo	$⊢ (φ \land (x \in B \land y \in B)) \to \exists^{*} f f \in (\underset{˙}{\leq} \times \{1_{𝑜}\}) (⟨x, y⟩)$
8		df-ov	$⊢ x (\underset{˙}{\leq} \times \{1_{𝑜}\}) y = (\underset{˙}{\leq} \times \{1_{𝑜}\}) (⟨x, y⟩)$
9	8	eleq2i	$⊢ f \in (x (\underset{˙}{\leq} \times \{1_{𝑜}\}) y) \leftrightarrow f \in (\underset{˙}{\leq} \times \{1_{𝑜}\}) (⟨x, y⟩)$
10	9	mobii	$⊢ \exists^{} f f \in (x (\underset{˙}{\leq} \times \{1_{𝑜}\}) y) \leftrightarrow \exists^{} f f \in (\underset{˙}{\leq} \times \{1_{𝑜}\}) (⟨x, y⟩)$
11	7 10	sylibr	$⊢ (φ \land (x \in B \land y \in B)) \to \exists^{*} f f \in (x (\underset{˙}{\leq} \times \{1_{𝑜}\}) y)$
12		biid	$⊢ ((x \in B \land y \in B \land z \in B) \land (f \in (x (\underset{˙}{\leq} \times \{1_{𝑜}\}) y) \land g \in (y (\underset{˙}{\leq} \times \{1_{𝑜}\}) z))) \leftrightarrow ((x \in B \land y \in B \land z \in B) \land (f \in (x (\underset{˙}{\leq} \times \{1_{𝑜}\}) y) \land g \in (y (\underset{˙}{\leq} \times \{1_{𝑜}\}) z)))$
13		0lt1o	$⊢ \emptyset \in 1_{𝑜}$
14	1	eleq2d	$⊢ φ \to (y \in B \leftrightarrow y \in {Base}_{C})$
15		eqid	$⊢ {Base}_{C} = {Base}_{C}$
16		eqid	$⊢ \leq_{C} = \leq_{C}$
17	15 16	prsref	$⊢ (C \in Proset \land y \in {Base}_{C}) \to y \leq_{C} y$
18	5 17	sylan	$⊢ (φ \land y \in {Base}_{C}) \to y \leq_{C} y$
19	14 18	sylbida	$⊢ (φ \land y \in B) \to y \leq_{C} y$
20	4	breqd	$⊢ φ \to (y \underset{˙}{\leq} y \leftrightarrow y \leq_{C} y)$
21	20	biimpar	$⊢ (φ \land y \leq_{C} y) \to y \underset{˙}{\leq} y$
22	19 21	syldan	$⊢ (φ \land y \in B) \to y \underset{˙}{\leq} y$
23		eqidd	$⊢ (φ \land y \in B) \to \underset{˙}{\leq} \times \{1_{𝑜}\} = \underset{˙}{\leq} \times \{1_{𝑜}\}$
24		1oex	$⊢ 1_{𝑜} \in V$
25	24	a1i	$⊢ (φ \land y \in B) \to 1_{𝑜} \in V$
26		1n0	$⊢ 1_{𝑜} \neq \emptyset$
27	26	a1i	$⊢ (φ \land y \in B) \to 1_{𝑜} \neq \emptyset$
28	23 25 27	fvconstr	$⊢ (φ \land y \in B) \to (y \underset{˙}{\leq} y \leftrightarrow y (\underset{˙}{\leq} \times \{1_{𝑜}\}) y = 1_{𝑜})$
29	22 28	mpbid	$⊢ (φ \land y \in B) \to y (\underset{˙}{\leq} \times \{1_{𝑜}\}) y = 1_{𝑜}$
30	13 29	eleqtrrid	$⊢ (φ \land y \in B) \to \emptyset \in (y (\underset{˙}{\leq} \times \{1_{𝑜}\}) y)$
31		0ov	$⊢ ⟨x, y⟩ \emptyset z = \emptyset$
32	31	oveqi	$⊢ g (⟨x, y⟩ \emptyset z) f = g \emptyset f$
33		0ov	$⊢ g \emptyset f = \emptyset$
34	32 33	eqtri	$⊢ g (⟨x, y⟩ \emptyset z) f = \emptyset$
35	34 13	eqeltri	$⊢ g (⟨x, y⟩ \emptyset z) f \in 1_{𝑜}$
36		simpl	$⊢ (φ \land ((x \in B \land y \in B \land z \in B) \land (f \in (x (\underset{˙}{\leq} \times \{1_{𝑜}\}) y) \land g \in (y (\underset{˙}{\leq} \times \{1_{𝑜}\}) z)))) \to φ$
37	5	adantr	$⊢ (φ \land ((x \in B \land y \in B \land z \in B) \land (f \in (x (\underset{˙}{\leq} \times \{1_{𝑜}\}) y) \land g \in (y (\underset{˙}{\leq} \times \{1_{𝑜}\}) z)))) \to C \in Proset$
38	1	eleq2d	$⊢ φ \to (x \in B \leftrightarrow x \in {Base}_{C})$
39	1	eleq2d	$⊢ φ \to (z \in B \leftrightarrow z \in {Base}_{C})$
40	38 14 39	3anbi123d	$⊢ φ \to ((x \in B \land y \in B \land z \in B) \leftrightarrow (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C}))$
41	40	biimpa	$⊢ (φ \land (x \in B \land y \in B \land z \in B)) \to (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C})$
42	41	adantrr	$⊢ (φ \land ((x \in B \land y \in B \land z \in B) \land (f \in (x (\underset{˙}{\leq} \times \{1_{𝑜}\}) y) \land g \in (y (\underset{˙}{\leq} \times \{1_{𝑜}\}) z)))) \to (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C})$
43		eqidd	$⊢ (φ \land ((x \in B \land y \in B \land z \in B) \land (f \in (x (\underset{˙}{\leq} \times \{1_{𝑜}\}) y) \land g \in (y (\underset{˙}{\leq} \times \{1_{𝑜}\}) z)))) \to \underset{˙}{\leq} \times \{1_{𝑜}\} = \underset{˙}{\leq} \times \{1_{𝑜}\}$
44		simprrl	$⊢ (φ \land ((x \in B \land y \in B \land z \in B) \land (f \in (x (\underset{˙}{\leq} \times \{1_{𝑜}\}) y) \land g \in (y (\underset{˙}{\leq} \times \{1_{𝑜}\}) z)))) \to f \in (x (\underset{˙}{\leq} \times \{1_{𝑜}\}) y)$
45	43 44	fvconstr2	$⊢ (φ \land ((x \in B \land y \in B \land z \in B) \land (f \in (x (\underset{˙}{\leq} \times \{1_{𝑜}\}) y) \land g \in (y (\underset{˙}{\leq} \times \{1_{𝑜}\}) z)))) \to x \underset{˙}{\leq} y$
46	4	breqd	$⊢ φ \to (x \underset{˙}{\leq} y \leftrightarrow x \leq_{C} y)$
47	46	biimpd	$⊢ φ \to (x \underset{˙}{\leq} y \to x \leq_{C} y)$
48	36 45 47	sylc	$⊢ (φ \land ((x \in B \land y \in B \land z \in B) \land (f \in (x (\underset{˙}{\leq} \times \{1_{𝑜}\}) y) \land g \in (y (\underset{˙}{\leq} \times \{1_{𝑜}\}) z)))) \to x \leq_{C} y$
49		simprrr	$⊢ (φ \land ((x \in B \land y \in B \land z \in B) \land (f \in (x (\underset{˙}{\leq} \times \{1_{𝑜}\}) y) \land g \in (y (\underset{˙}{\leq} \times \{1_{𝑜}\}) z)))) \to g \in (y (\underset{˙}{\leq} \times \{1_{𝑜}\}) z)$
50	43 49	fvconstr2	$⊢ (φ \land ((x \in B \land y \in B \land z \in B) \land (f \in (x (\underset{˙}{\leq} \times \{1_{𝑜}\}) y) \land g \in (y (\underset{˙}{\leq} \times \{1_{𝑜}\}) z)))) \to y \underset{˙}{\leq} z$
51	4	breqd	$⊢ φ \to (y \underset{˙}{\leq} z \leftrightarrow y \leq_{C} z)$
52	51	biimpd	$⊢ φ \to (y \underset{˙}{\leq} z \to y \leq_{C} z)$
53	36 50 52	sylc	$⊢ (φ \land ((x \in B \land y \in B \land z \in B) \land (f \in (x (\underset{˙}{\leq} \times \{1_{𝑜}\}) y) \land g \in (y (\underset{˙}{\leq} \times \{1_{𝑜}\}) z)))) \to y \leq_{C} z$
54	15 16	prstr	$⊢ (C \in Proset \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C}) \land (x \leq_{C} y \land y \leq_{C} z)) \to x \leq_{C} z$
55	37 42 48 53 54	syl112anc	$⊢ (φ \land ((x \in B \land y \in B \land z \in B) \land (f \in (x (\underset{˙}{\leq} \times \{1_{𝑜}\}) y) \land g \in (y (\underset{˙}{\leq} \times \{1_{𝑜}\}) z)))) \to x \leq_{C} z$
56	4	breqd	$⊢ φ \to (x \underset{˙}{\leq} z \leftrightarrow x \leq_{C} z)$
57	56	biimprd	$⊢ φ \to (x \leq_{C} z \to x \underset{˙}{\leq} z)$
58	36 55 57	sylc	$⊢ (φ \land ((x \in B \land y \in B \land z \in B) \land (f \in (x (\underset{˙}{\leq} \times \{1_{𝑜}\}) y) \land g \in (y (\underset{˙}{\leq} \times \{1_{𝑜}\}) z)))) \to x \underset{˙}{\leq} z$
59	24	a1i	$⊢ (φ \land ((x \in B \land y \in B \land z \in B) \land (f \in (x (\underset{˙}{\leq} \times \{1_{𝑜}\}) y) \land g \in (y (\underset{˙}{\leq} \times \{1_{𝑜}\}) z)))) \to 1_{𝑜} \in V$
60	26	a1i	$⊢ (φ \land ((x \in B \land y \in B \land z \in B) \land (f \in (x (\underset{˙}{\leq} \times \{1_{𝑜}\}) y) \land g \in (y (\underset{˙}{\leq} \times \{1_{𝑜}\}) z)))) \to 1_{𝑜} \neq \emptyset$
61	43 59 60	fvconstr	$⊢ (φ \land ((x \in B \land y \in B \land z \in B) \land (f \in (x (\underset{˙}{\leq} \times \{1_{𝑜}\}) y) \land g \in (y (\underset{˙}{\leq} \times \{1_{𝑜}\}) z)))) \to (x \underset{˙}{\leq} z \leftrightarrow x (\underset{˙}{\leq} \times \{1_{𝑜}\}) z = 1_{𝑜})$
62	58 61	mpbid	$⊢ (φ \land ((x \in B \land y \in B \land z \in B) \land (f \in (x (\underset{˙}{\leq} \times \{1_{𝑜}\}) y) \land g \in (y (\underset{˙}{\leq} \times \{1_{𝑜}\}) z)))) \to x (\underset{˙}{\leq} \times \{1_{𝑜}\}) z = 1_{𝑜}$
63	35 62	eleqtrrid	$⊢ (φ \land ((x \in B \land y \in B \land z \in B) \land (f \in (x (\underset{˙}{\leq} \times \{1_{𝑜}\}) y) \land g \in (y (\underset{˙}{\leq} \times \{1_{𝑜}\}) z)))) \to g (⟨x, y⟩ \emptyset z) f \in (x (\underset{˙}{\leq} \times \{1_{𝑜}\}) z)$
64	1 2 11 3 5 12 30 63	isthincd2	$⊢ φ \to (C \in ThinCat \land Id (C) = (y \in B ⟼ \emptyset))$

Metamath Proof Explorer

Theorem prsthinc

Proof