Users' Mathboxes Mathbox for Zhi Wang < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  prsthinc Structured version   Visualization version   GIF version

Theorem prsthinc 45783
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 45757 and catprs2 45758 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.)
Hypotheses
Ref Expression
indthinc.b (𝜑𝐵 = (Base‘𝐶))
prsthinc.h (𝜑 → ( × {1o}) = (Hom ‘𝐶))
prsthinc.o (𝜑 → ∅ = (comp‘𝐶))
prsthinc.l (𝜑 = (le‘𝐶))
prsthinc.p (𝜑𝐶 ∈ Proset )
Assertion
Ref Expression
prsthinc (𝜑 → (𝐶 ∈ ThinCat ∧ (Id‘𝐶) = (𝑦𝐵 ↦ ∅)))
Distinct variable groups:   𝑦,   𝑦,𝐵   𝑦,𝐶   𝜑,𝑦

Proof of Theorem prsthinc
Dummy variables 𝑓 𝑔 𝑥 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 indthinc.b . 2 (𝜑𝐵 = (Base‘𝐶))
2 prsthinc.h . 2 (𝜑 → ( × {1o}) = (Hom ‘𝐶))
3 eqidd 2739 . . . 4 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → ( × {1o}) = ( × {1o}))
43f1omo 45695 . . 3 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → ∃*𝑓 𝑓 ∈ (( × {1o})‘⟨𝑥, 𝑦⟩))
5 df-ov 7167 . . . . 5 (𝑥( × {1o})𝑦) = (( × {1o})‘⟨𝑥, 𝑦⟩)
65eleq2i 2824 . . . 4 (𝑓 ∈ (𝑥( × {1o})𝑦) ↔ 𝑓 ∈ (( × {1o})‘⟨𝑥, 𝑦⟩))
76mobii 2548 . . 3 (∃*𝑓 𝑓 ∈ (𝑥( × {1o})𝑦) ↔ ∃*𝑓 𝑓 ∈ (( × {1o})‘⟨𝑥, 𝑦⟩))
84, 7sylibr 237 . 2 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → ∃*𝑓 𝑓 ∈ (𝑥( × {1o})𝑦))
9 prsthinc.o . 2 (𝜑 → ∅ = (comp‘𝐶))
10 prsthinc.p . 2 (𝜑𝐶 ∈ Proset )
11 biid 264 . 2 (((𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑓 ∈ (𝑥( × {1o})𝑦) ∧ 𝑔 ∈ (𝑦( × {1o})𝑧))) ↔ ((𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑓 ∈ (𝑥( × {1o})𝑦) ∧ 𝑔 ∈ (𝑦( × {1o})𝑧))))
12 0lt1o 8153 . . 3 ∅ ∈ 1o
131eleq2d 2818 . . . . . 6 (𝜑 → (𝑦𝐵𝑦 ∈ (Base‘𝐶)))
14 eqid 2738 . . . . . . . 8 (Base‘𝐶) = (Base‘𝐶)
15 eqid 2738 . . . . . . . 8 (le‘𝐶) = (le‘𝐶)
1614, 15prsref 17651 . . . . . . 7 ((𝐶 ∈ Proset ∧ 𝑦 ∈ (Base‘𝐶)) → 𝑦(le‘𝐶)𝑦)
1710, 16sylan 583 . . . . . 6 ((𝜑𝑦 ∈ (Base‘𝐶)) → 𝑦(le‘𝐶)𝑦)
1813, 17sylbida 595 . . . . 5 ((𝜑𝑦𝐵) → 𝑦(le‘𝐶)𝑦)
19 prsthinc.l . . . . . . 7 (𝜑 = (le‘𝐶))
2019breqd 5038 . . . . . 6 (𝜑 → (𝑦 𝑦𝑦(le‘𝐶)𝑦))
2120biimpar 481 . . . . 5 ((𝜑𝑦(le‘𝐶)𝑦) → 𝑦 𝑦)
2218, 21syldan 594 . . . 4 ((𝜑𝑦𝐵) → 𝑦 𝑦)
23 eqidd 2739 . . . . 5 ((𝜑𝑦𝐵) → ( × {1o}) = ( × {1o}))
24 1oex 8137 . . . . . 6 1o ∈ V
2524a1i 11 . . . . 5 ((𝜑𝑦𝐵) → 1o ∈ V)
26 1n0 8143 . . . . . 6 1o ≠ ∅
2726a1i 11 . . . . 5 ((𝜑𝑦𝐵) → 1o ≠ ∅)
2823, 25, 27fvconstr 45690 . . . 4 ((𝜑𝑦𝐵) → (𝑦 𝑦 ↔ (𝑦( × {1o})𝑦) = 1o))
2922, 28mpbid 235 . . 3 ((𝜑𝑦𝐵) → (𝑦( × {1o})𝑦) = 1o)
3012, 29eleqtrrid 2840 . 2 ((𝜑𝑦𝐵) → ∅ ∈ (𝑦( × {1o})𝑦))
31 0ov 7201 . . . . . 6 (⟨𝑥, 𝑦⟩∅𝑧) = ∅
3231oveqi 7177 . . . . 5 (𝑔(⟨𝑥, 𝑦⟩∅𝑧)𝑓) = (𝑔𝑓)
33 0ov 7201 . . . . 5 (𝑔𝑓) = ∅
3432, 33eqtri 2761 . . . 4 (𝑔(⟨𝑥, 𝑦⟩∅𝑧)𝑓) = ∅
3534, 12eqeltri 2829 . . 3 (𝑔(⟨𝑥, 𝑦⟩∅𝑧)𝑓) ∈ 1o
36 simpl 486 . . . . 5 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑓 ∈ (𝑥( × {1o})𝑦) ∧ 𝑔 ∈ (𝑦( × {1o})𝑧)))) → 𝜑)
3710adantr 484 . . . . . 6 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑓 ∈ (𝑥( × {1o})𝑦) ∧ 𝑔 ∈ (𝑦( × {1o})𝑧)))) → 𝐶 ∈ Proset )
381eleq2d 2818 . . . . . . . . 9 (𝜑 → (𝑥𝐵𝑥 ∈ (Base‘𝐶)))
391eleq2d 2818 . . . . . . . . 9 (𝜑 → (𝑧𝐵𝑧 ∈ (Base‘𝐶)))
4038, 13, 393anbi123d 1437 . . . . . . . 8 (𝜑 → ((𝑥𝐵𝑦𝐵𝑧𝐵) ↔ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))))
4140biimpa 480 . . . . . . 7 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵)) → (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)))
4241adantrr 717 . . . . . 6 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑓 ∈ (𝑥( × {1o})𝑦) ∧ 𝑔 ∈ (𝑦( × {1o})𝑧)))) → (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)))
43 eqidd 2739 . . . . . . . 8 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑓 ∈ (𝑥( × {1o})𝑦) ∧ 𝑔 ∈ (𝑦( × {1o})𝑧)))) → ( × {1o}) = ( × {1o}))
44 simprrl 781 . . . . . . . 8 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑓 ∈ (𝑥( × {1o})𝑦) ∧ 𝑔 ∈ (𝑦( × {1o})𝑧)))) → 𝑓 ∈ (𝑥( × {1o})𝑦))
4543, 44fvconstr2 45692 . . . . . . 7 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑓 ∈ (𝑥( × {1o})𝑦) ∧ 𝑔 ∈ (𝑦( × {1o})𝑧)))) → 𝑥 𝑦)
4619breqd 5038 . . . . . . . 8 (𝜑 → (𝑥 𝑦𝑥(le‘𝐶)𝑦))
4746biimpd 232 . . . . . . 7 (𝜑 → (𝑥 𝑦𝑥(le‘𝐶)𝑦))
4836, 45, 47sylc 65 . . . . . 6 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑓 ∈ (𝑥( × {1o})𝑦) ∧ 𝑔 ∈ (𝑦( × {1o})𝑧)))) → 𝑥(le‘𝐶)𝑦)
49 simprrr 782 . . . . . . . 8 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑓 ∈ (𝑥( × {1o})𝑦) ∧ 𝑔 ∈ (𝑦( × {1o})𝑧)))) → 𝑔 ∈ (𝑦( × {1o})𝑧))
5043, 49fvconstr2 45692 . . . . . . 7 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑓 ∈ (𝑥( × {1o})𝑦) ∧ 𝑔 ∈ (𝑦( × {1o})𝑧)))) → 𝑦 𝑧)
5119breqd 5038 . . . . . . . 8 (𝜑 → (𝑦 𝑧𝑦(le‘𝐶)𝑧))
5251biimpd 232 . . . . . . 7 (𝜑 → (𝑦 𝑧𝑦(le‘𝐶)𝑧))
5336, 50, 52sylc 65 . . . . . 6 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑓 ∈ (𝑥( × {1o})𝑦) ∧ 𝑔 ∈ (𝑦( × {1o})𝑧)))) → 𝑦(le‘𝐶)𝑧)
5414, 15prstr 17652 . . . . . 6 ((𝐶 ∈ Proset ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑥(le‘𝐶)𝑦𝑦(le‘𝐶)𝑧)) → 𝑥(le‘𝐶)𝑧)
5537, 42, 48, 53, 54syl112anc 1375 . . . . 5 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑓 ∈ (𝑥( × {1o})𝑦) ∧ 𝑔 ∈ (𝑦( × {1o})𝑧)))) → 𝑥(le‘𝐶)𝑧)
5619breqd 5038 . . . . . 6 (𝜑 → (𝑥 𝑧𝑥(le‘𝐶)𝑧))
5756biimprd 251 . . . . 5 (𝜑 → (𝑥(le‘𝐶)𝑧𝑥 𝑧))
5836, 55, 57sylc 65 . . . 4 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑓 ∈ (𝑥( × {1o})𝑦) ∧ 𝑔 ∈ (𝑦( × {1o})𝑧)))) → 𝑥 𝑧)
5924a1i 11 . . . . 5 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑓 ∈ (𝑥( × {1o})𝑦) ∧ 𝑔 ∈ (𝑦( × {1o})𝑧)))) → 1o ∈ V)
6026a1i 11 . . . . 5 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑓 ∈ (𝑥( × {1o})𝑦) ∧ 𝑔 ∈ (𝑦( × {1o})𝑧)))) → 1o ≠ ∅)
6143, 59, 60fvconstr 45690 . . . 4 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑓 ∈ (𝑥( × {1o})𝑦) ∧ 𝑔 ∈ (𝑦( × {1o})𝑧)))) → (𝑥 𝑧 ↔ (𝑥( × {1o})𝑧) = 1o))
6258, 61mpbid 235 . . 3 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑓 ∈ (𝑥( × {1o})𝑦) ∧ 𝑔 ∈ (𝑦( × {1o})𝑧)))) → (𝑥( × {1o})𝑧) = 1o)
6335, 62eleqtrrid 2840 . 2 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑓 ∈ (𝑥( × {1o})𝑦) ∧ 𝑔 ∈ (𝑦( × {1o})𝑧)))) → (𝑔(⟨𝑥, 𝑦⟩∅𝑧)𝑓) ∈ (𝑥( × {1o})𝑧))
641, 2, 8, 9, 10, 11, 30, 63isthincd2 45776 1 (𝜑 → (𝐶 ∈ ThinCat ∧ (Id‘𝐶) = (𝑦𝐵 ↦ ∅)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  w3a 1088   = wceq 1542  wcel 2113  ∃*wmo 2538  wne 2934  Vcvv 3397  c0 4209  {csn 4513  cop 4519   class class class wbr 5027  cmpt 5107   × cxp 5517  cfv 6333  (class class class)co 7164  1oc1o 8117  Basecbs 16579  lecple 16668  Hom chom 16672  compcco 16673  Idccid 17032   Proset cproset 17645  ThinCatcthinc 45763
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2161  ax-12 2178  ax-ext 2710  ax-rep 5151  ax-sep 5164  ax-nul 5171  ax-pr 5293
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ne 2935  df-ral 3058  df-rex 3059  df-reu 3060  df-rmo 3061  df-rab 3062  df-v 3399  df-sbc 3680  df-csb 3789  df-dif 3844  df-un 3846  df-in 3848  df-ss 3858  df-nul 4210  df-if 4412  df-sn 4514  df-pr 4516  df-op 4520  df-uni 4794  df-iun 4880  df-br 5028  df-opab 5090  df-mpt 5108  df-id 5425  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-suc 6172  df-iota 6291  df-fun 6335  df-fn 6336  df-f 6337  df-f1 6338  df-fo 6339  df-f1o 6340  df-fv 6341  df-riota 7121  df-ov 7167  df-1o 8124  df-cat 17035  df-cid 17036  df-proset 17647  df-thinc 45764
This theorem is referenced by:  prstcthin  45798
  Copyright terms: Public domain W3C validator