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	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐶 ) )
	prsthinc.h	⊢ ( 𝜑 → ( ≤ × { 1_o } ) = ( Hom ‘ 𝐶 ) )
	prsthinc.o	⊢ ( 𝜑 → ∅ = ( comp ‘ 𝐶 ) )
	prsthinc.l	⊢ ( 𝜑 → ≤ = ( le ‘ 𝐶 ) )
	prsthinc.p	⊢ ( 𝜑 → 𝐶 ∈ Proset )
Assertion	prsthinc	⊢ ( 𝜑 → ( 𝐶 ∈ ThinCat ∧ ( Id ‘ 𝐶 ) = ( 𝑦 ∈ 𝐵 ↦ ∅ ) ) )

Proof

Step	Hyp	Ref	Expression
1		indthinc.b	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐶 ) )
2		prsthinc.h	⊢ ( 𝜑 → ( ≤ × { 1_o } ) = ( Hom ‘ 𝐶 ) )
3		prsthinc.o	⊢ ( 𝜑 → ∅ = ( comp ‘ 𝐶 ) )
4		prsthinc.l	⊢ ( 𝜑 → ≤ = ( le ‘ 𝐶 ) )
5		prsthinc.p	⊢ ( 𝜑 → 𝐶 ∈ Proset )
6		eqidd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ≤ × { 1_o } ) = ( ≤ × { 1_o } ) )
7	6	f1omo	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ∃* 𝑓 𝑓 ∈ ( ( ≤ × { 1_o } ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
8		df-ov	⊢ ( 𝑥 ( ≤ × { 1_o } ) 𝑦 ) = ( ( ≤ × { 1_o } ) ‘ ⟨ 𝑥 , 𝑦 ⟩ )
9	8	eleq2i	⊢ ( 𝑓 ∈ ( 𝑥 ( ≤ × { 1_o } ) 𝑦 ) ↔ 𝑓 ∈ ( ( ≤ × { 1_o } ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
10	9	mobii	⊢ ( ∃* 𝑓 𝑓 ∈ ( 𝑥 ( ≤ × { 1_o } ) 𝑦 ) ↔ ∃* 𝑓 𝑓 ∈ ( ( ≤ × { 1_o } ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
11	7 10	sylibr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ∃* 𝑓 𝑓 ∈ ( 𝑥 ( ≤ × { 1_o } ) 𝑦 ) )
12		biid	⊢ ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 ( ≤ × { 1_o } ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( ≤ × { 1_o } ) 𝑧 ) ) ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 ( ≤ × { 1_o } ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( ≤ × { 1_o } ) 𝑧 ) ) ) )
13		0lt1o	⊢ ∅ ∈ 1_o
14	1	eleq2d	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐵 ↔ 𝑦 ∈ ( Base ‘ 𝐶 ) ) )
15		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
16		eqid	⊢ ( le ‘ 𝐶 ) = ( le ‘ 𝐶 )
17	15 16	prsref	⊢ ( ( 𝐶 ∈ Proset ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → 𝑦 ( le ‘ 𝐶 ) 𝑦 )
18	5 17	sylan	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → 𝑦 ( le ‘ 𝐶 ) 𝑦 )
19	14 18	sylbida	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ( le ‘ 𝐶 ) 𝑦 )
20	4	breqd	⊢ ( 𝜑 → ( 𝑦 ≤ 𝑦 ↔ 𝑦 ( le ‘ 𝐶 ) 𝑦 ) )
21	20	biimpar	⊢ ( ( 𝜑 ∧ 𝑦 ( le ‘ 𝐶 ) 𝑦 ) → 𝑦 ≤ 𝑦 )
22	19 21	syldan	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ≤ 𝑦 )
23		eqidd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( ≤ × { 1_o } ) = ( ≤ × { 1_o } ) )
24		1oex	⊢ 1_o ∈ V
25	24	a1i	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → 1_o ∈ V )
26		1n0	⊢ 1_o ≠ ∅
27	26	a1i	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → 1_o ≠ ∅ )
28	23 25 27	fvconstr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑦 ≤ 𝑦 ↔ ( 𝑦 ( ≤ × { 1_o } ) 𝑦 ) = 1_o ) )
29	22 28	mpbid	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑦 ( ≤ × { 1_o } ) 𝑦 ) = 1_o )
30	13 29	eleqtrrid	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ∅ ∈ ( 𝑦 ( ≤ × { 1_o } ) 𝑦 ) )
31		0ov	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∅ 𝑧 ) = ∅
32	31	oveqi	⊢ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ∅ 𝑧 ) 𝑓 ) = ( 𝑔 ∅ 𝑓 )
33		0ov	⊢ ( 𝑔 ∅ 𝑓 ) = ∅
34	32 33	eqtri	⊢ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ∅ 𝑧 ) 𝑓 ) = ∅
35	34 13	eqeltri	⊢ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ∅ 𝑧 ) 𝑓 ) ∈ 1_o
36		simpl	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 ( ≤ × { 1_o } ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( ≤ × { 1_o } ) 𝑧 ) ) ) ) → 𝜑 )
37	5	adantr	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 ( ≤ × { 1_o } ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( ≤ × { 1_o } ) 𝑧 ) ) ) ) → 𝐶 ∈ Proset )
38	1	eleq2d	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↔ 𝑥 ∈ ( Base ‘ 𝐶 ) ) )
39	1	eleq2d	⊢ ( 𝜑 → ( 𝑧 ∈ 𝐵 ↔ 𝑧 ∈ ( Base ‘ 𝐶 ) ) )
40	38 14 39	3anbi123d	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ↔ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ) )
41	40	biimpa	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) )
42	41	adantrr	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 ( ≤ × { 1_o } ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( ≤ × { 1_o } ) 𝑧 ) ) ) ) → ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) )
43		eqidd	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 ( ≤ × { 1_o } ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( ≤ × { 1_o } ) 𝑧 ) ) ) ) → ( ≤ × { 1_o } ) = ( ≤ × { 1_o } ) )
44		simprrl	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 ( ≤ × { 1_o } ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( ≤ × { 1_o } ) 𝑧 ) ) ) ) → 𝑓 ∈ ( 𝑥 ( ≤ × { 1_o } ) 𝑦 ) )
45	43 44	fvconstr2	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 ( ≤ × { 1_o } ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( ≤ × { 1_o } ) 𝑧 ) ) ) ) → 𝑥 ≤ 𝑦 )
46	4	breqd	⊢ ( 𝜑 → ( 𝑥 ≤ 𝑦 ↔ 𝑥 ( le ‘ 𝐶 ) 𝑦 ) )
47	46	biimpd	⊢ ( 𝜑 → ( 𝑥 ≤ 𝑦 → 𝑥 ( le ‘ 𝐶 ) 𝑦 ) )
48	36 45 47	sylc	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 ( ≤ × { 1_o } ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( ≤ × { 1_o } ) 𝑧 ) ) ) ) → 𝑥 ( le ‘ 𝐶 ) 𝑦 )
49		simprrr	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 ( ≤ × { 1_o } ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( ≤ × { 1_o } ) 𝑧 ) ) ) ) → 𝑔 ∈ ( 𝑦 ( ≤ × { 1_o } ) 𝑧 ) )
50	43 49	fvconstr2	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 ( ≤ × { 1_o } ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( ≤ × { 1_o } ) 𝑧 ) ) ) ) → 𝑦 ≤ 𝑧 )
51	4	breqd	⊢ ( 𝜑 → ( 𝑦 ≤ 𝑧 ↔ 𝑦 ( le ‘ 𝐶 ) 𝑧 ) )
52	51	biimpd	⊢ ( 𝜑 → ( 𝑦 ≤ 𝑧 → 𝑦 ( le ‘ 𝐶 ) 𝑧 ) )
53	36 50 52	sylc	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 ( ≤ × { 1_o } ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( ≤ × { 1_o } ) 𝑧 ) ) ) ) → 𝑦 ( le ‘ 𝐶 ) 𝑧 )
54	15 16	prstr	⊢ ( ( 𝐶 ∈ Proset ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑥 ( le ‘ 𝐶 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐶 ) 𝑧 ) ) → 𝑥 ( le ‘ 𝐶 ) 𝑧 )
55	37 42 48 53 54	syl112anc	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 ( ≤ × { 1_o } ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( ≤ × { 1_o } ) 𝑧 ) ) ) ) → 𝑥 ( le ‘ 𝐶 ) 𝑧 )
56	4	breqd	⊢ ( 𝜑 → ( 𝑥 ≤ 𝑧 ↔ 𝑥 ( le ‘ 𝐶 ) 𝑧 ) )
57	56	biimprd	⊢ ( 𝜑 → ( 𝑥 ( le ‘ 𝐶 ) 𝑧 → 𝑥 ≤ 𝑧 ) )
58	36 55 57	sylc	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 ( ≤ × { 1_o } ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( ≤ × { 1_o } ) 𝑧 ) ) ) ) → 𝑥 ≤ 𝑧 )
59	24	a1i	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 ( ≤ × { 1_o } ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( ≤ × { 1_o } ) 𝑧 ) ) ) ) → 1_o ∈ V )
60	26	a1i	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 ( ≤ × { 1_o } ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( ≤ × { 1_o } ) 𝑧 ) ) ) ) → 1_o ≠ ∅ )
61	43 59 60	fvconstr	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 ( ≤ × { 1_o } ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( ≤ × { 1_o } ) 𝑧 ) ) ) ) → ( 𝑥 ≤ 𝑧 ↔ ( 𝑥 ( ≤ × { 1_o } ) 𝑧 ) = 1_o ) )
62	58 61	mpbid	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 ( ≤ × { 1_o } ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( ≤ × { 1_o } ) 𝑧 ) ) ) ) → ( 𝑥 ( ≤ × { 1_o } ) 𝑧 ) = 1_o )
63	35 62	eleqtrrid	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 ( ≤ × { 1_o } ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( ≤ × { 1_o } ) 𝑧 ) ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ∅ 𝑧 ) 𝑓 ) ∈ ( 𝑥 ( ≤ × { 1_o } ) 𝑧 ) )
64	1 2 11 3 5 12 30 63	isthincd2	⊢ ( 𝜑 → ( 𝐶 ∈ ThinCat ∧ ( Id ‘ 𝐶 ) = ( 𝑦 ∈ 𝐵 ↦ ∅ ) ) )

Metamath Proof Explorer

Theorem prsthinc

Proof