This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 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 ⊢ ( 𝜑 → ( ≤ × { 1o } ) = ( 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 ⊢ ( 𝜑 → ( ≤ × { 1o } ) = ( Hom ‘ 𝐶 ) )
3 prsthinc.o ⊢ ( 𝜑 → ∅ = ( comp ‘ 𝐶 ) )
4 prsthinc.l ⊢ ( 𝜑 → ≤ = ( le ‘ 𝐶 ) )
5 prsthinc.p ⊢ ( 𝜑 → 𝐶 ∈ Proset )
6 eqidd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ≤ × { 1o } ) = ( ≤ × { 1o } ) )
7 6 f1omo ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ∃* 𝑓 𝑓 ∈ ( ( ≤ × { 1o } ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
8 df-ov ⊢ ( 𝑥 ( ≤ × { 1o } ) 𝑦 ) = ( ( ≤ × { 1o } ) ‘ ⟨ 𝑥 , 𝑦 ⟩ )
9 8 eleq2i ⊢ ( 𝑓 ∈ ( 𝑥 ( ≤ × { 1o } ) 𝑦 ) ↔ 𝑓 ∈ ( ( ≤ × { 1o } ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
10 9 mobii ⊢ ( ∃* 𝑓 𝑓 ∈ ( 𝑥 ( ≤ × { 1o } ) 𝑦 ) ↔ ∃* 𝑓 𝑓 ∈ ( ( ≤ × { 1o } ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
11 7 10 sylibr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ∃* 𝑓 𝑓 ∈ ( 𝑥 ( ≤ × { 1o } ) 𝑦 ) )
12 biid ⊢ ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 ( ≤ × { 1o } ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( ≤ × { 1o } ) 𝑧 ) ) ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 ( ≤ × { 1o } ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( ≤ × { 1o } ) 𝑧 ) ) ) )
13 0lt1o ⊢ ∅ ∈ 1o
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 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( ≤ × { 1o } ) = ( ≤ × { 1o } ) )
24 1oex ⊢ 1o ∈ V
25 24 a1i ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → 1o ∈ V )
26 1n0 ⊢ 1o ≠ ∅
27 26 a1i ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → 1o ≠ ∅ )
28 23 25 27 fvconstr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑦 ≤ 𝑦 ↔ ( 𝑦 ( ≤ × { 1o } ) 𝑦 ) = 1o ) )
29 22 28 mpbid ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑦 ( ≤ × { 1o } ) 𝑦 ) = 1o )
30 13 29 eleqtrrid ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ∅ ∈ ( 𝑦 ( ≤ × { 1o } ) 𝑦 ) )
31 0ov ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∅ 𝑧 ) = ∅
32 31 oveqi ⊢ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ∅ 𝑧 ) 𝑓 ) = ( 𝑔 ∅ 𝑓 )
33 0ov ⊢ ( 𝑔 ∅ 𝑓 ) = ∅
34 32 33 eqtri ⊢ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ∅ 𝑧 ) 𝑓 ) = ∅
35 34 13 eqeltri ⊢ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ∅ 𝑧 ) 𝑓 ) ∈ 1o
36 simpl ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 ( ≤ × { 1o } ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( ≤ × { 1o } ) 𝑧 ) ) ) ) → 𝜑 )
37 5 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 ( ≤ × { 1o } ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( ≤ × { 1o } ) 𝑧 ) ) ) ) → 𝐶 ∈ 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 ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 ( ≤ × { 1o } ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( ≤ × { 1o } ) 𝑧 ) ) ) ) → ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) )
43 eqidd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 ( ≤ × { 1o } ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( ≤ × { 1o } ) 𝑧 ) ) ) ) → ( ≤ × { 1o } ) = ( ≤ × { 1o } ) )
44 simprrl ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 ( ≤ × { 1o } ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( ≤ × { 1o } ) 𝑧 ) ) ) ) → 𝑓 ∈ ( 𝑥 ( ≤ × { 1o } ) 𝑦 ) )
45 43 44 fvconstr2 ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 ( ≤ × { 1o } ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( ≤ × { 1o } ) 𝑧 ) ) ) ) → 𝑥 ≤ 𝑦 )
46 4 breqd ⊢ ( 𝜑 → ( 𝑥 ≤ 𝑦 ↔ 𝑥 ( le ‘ 𝐶 ) 𝑦 ) )
47 46 biimpd ⊢ ( 𝜑 → ( 𝑥 ≤ 𝑦 → 𝑥 ( le ‘ 𝐶 ) 𝑦 ) )
48 36 45 47 sylc ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 ( ≤ × { 1o } ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( ≤ × { 1o } ) 𝑧 ) ) ) ) → 𝑥 ( le ‘ 𝐶 ) 𝑦 )
49 simprrr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 ( ≤ × { 1o } ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( ≤ × { 1o } ) 𝑧 ) ) ) ) → 𝑔 ∈ ( 𝑦 ( ≤ × { 1o } ) 𝑧 ) )
50 43 49 fvconstr2 ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 ( ≤ × { 1o } ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( ≤ × { 1o } ) 𝑧 ) ) ) ) → 𝑦 ≤ 𝑧 )
51 4 breqd ⊢ ( 𝜑 → ( 𝑦 ≤ 𝑧 ↔ 𝑦 ( le ‘ 𝐶 ) 𝑧 ) )
52 51 biimpd ⊢ ( 𝜑 → ( 𝑦 ≤ 𝑧 → 𝑦 ( le ‘ 𝐶 ) 𝑧 ) )
53 36 50 52 sylc ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 ( ≤ × { 1o } ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( ≤ × { 1o } ) 𝑧 ) ) ) ) → 𝑦 ( le ‘ 𝐶 ) 𝑧 )
54 15 16 prstr ⊢ ( ( 𝐶 ∈ Proset ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑥 ( le ‘ 𝐶 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐶 ) 𝑧 ) ) → 𝑥 ( le ‘ 𝐶 ) 𝑧 )
55 37 42 48 53 54 syl112anc ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 ( ≤ × { 1o } ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( ≤ × { 1o } ) 𝑧 ) ) ) ) → 𝑥 ( le ‘ 𝐶 ) 𝑧 )
56 4 breqd ⊢ ( 𝜑 → ( 𝑥 ≤ 𝑧 ↔ 𝑥 ( le ‘ 𝐶 ) 𝑧 ) )
57 56 biimprd ⊢ ( 𝜑 → ( 𝑥 ( le ‘ 𝐶 ) 𝑧 → 𝑥 ≤ 𝑧 ) )
58 36 55 57 sylc ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 ( ≤ × { 1o } ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( ≤ × { 1o } ) 𝑧 ) ) ) ) → 𝑥 ≤ 𝑧 )
59 24 a1i ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 ( ≤ × { 1o } ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( ≤ × { 1o } ) 𝑧 ) ) ) ) → 1o ∈ V )
60 26 a1i ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 ( ≤ × { 1o } ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( ≤ × { 1o } ) 𝑧 ) ) ) ) → 1o ≠ ∅ )
61 43 59 60 fvconstr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 ( ≤ × { 1o } ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( ≤ × { 1o } ) 𝑧 ) ) ) ) → ( 𝑥 ≤ 𝑧 ↔ ( 𝑥 ( ≤ × { 1o } ) 𝑧 ) = 1o ) )
62 58 61 mpbid ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 ( ≤ × { 1o } ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( ≤ × { 1o } ) 𝑧 ) ) ) ) → ( 𝑥 ( ≤ × { 1o } ) 𝑧 ) = 1o )
63 35 62 eleqtrrid ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 ( ≤ × { 1o } ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( ≤ × { 1o } ) 𝑧 ) ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ∅ 𝑧 ) 𝑓 ) ∈ ( 𝑥 ( ≤ × { 1o } ) 𝑧 ) )
64 1 2 11 3 5 12 30 63 isthincd2 ⊢ ( 𝜑 → ( 𝐶 ∈ ThinCat ∧ ( Id ‘ 𝐶 ) = ( 𝑦 ∈ 𝐵 ↦ ∅ ) ) )