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 49111
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 48900 and catprs2 48901 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 2738 . . . 4 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → ( × {1o}) = ( × {1o}))
43f1omo 48792 . . 3 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → ∃*𝑓 𝑓 ∈ (( × {1o})‘⟨𝑥, 𝑦⟩))
5 df-ov 7434 . . . . 5 (𝑥( × {1o})𝑦) = (( × {1o})‘⟨𝑥, 𝑦⟩)
65eleq2i 2833 . . . 4 (𝑓 ∈ (𝑥( × {1o})𝑦) ↔ 𝑓 ∈ (( × {1o})‘⟨𝑥, 𝑦⟩))
76mobii 2548 . . 3 (∃*𝑓 𝑓 ∈ (𝑥( × {1o})𝑦) ↔ ∃*𝑓 𝑓 ∈ (( × {1o})‘⟨𝑥, 𝑦⟩))
84, 7sylibr 234 . 2 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → ∃*𝑓 𝑓 ∈ (𝑥( × {1o})𝑦))
9 prsthinc.o . 2 (𝜑 → ∅ = (comp‘𝐶))
10 prsthinc.p . 2 (𝜑𝐶 ∈ Proset )
11 biid 261 . 2 (((𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑓 ∈ (𝑥( × {1o})𝑦) ∧ 𝑔 ∈ (𝑦( × {1o})𝑧))) ↔ ((𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑓 ∈ (𝑥( × {1o})𝑦) ∧ 𝑔 ∈ (𝑦( × {1o})𝑧))))
12 0lt1o 8542 . . 3 ∅ ∈ 1o
131eleq2d 2827 . . . . . 6 (𝜑 → (𝑦𝐵𝑦 ∈ (Base‘𝐶)))
14 eqid 2737 . . . . . . . 8 (Base‘𝐶) = (Base‘𝐶)
15 eqid 2737 . . . . . . . 8 (le‘𝐶) = (le‘𝐶)
1614, 15prsref 18344 . . . . . . 7 ((𝐶 ∈ Proset ∧ 𝑦 ∈ (Base‘𝐶)) → 𝑦(le‘𝐶)𝑦)
1710, 16sylan 580 . . . . . 6 ((𝜑𝑦 ∈ (Base‘𝐶)) → 𝑦(le‘𝐶)𝑦)
1813, 17sylbida 592 . . . . 5 ((𝜑𝑦𝐵) → 𝑦(le‘𝐶)𝑦)
19 prsthinc.l . . . . . . 7 (𝜑 = (le‘𝐶))
2019breqd 5154 . . . . . 6 (𝜑 → (𝑦 𝑦𝑦(le‘𝐶)𝑦))
2120biimpar 477 . . . . 5 ((𝜑𝑦(le‘𝐶)𝑦) → 𝑦 𝑦)
2218, 21syldan 591 . . . 4 ((𝜑𝑦𝐵) → 𝑦 𝑦)
23 eqidd 2738 . . . . 5 ((𝜑𝑦𝐵) → ( × {1o}) = ( × {1o}))
24 1oex 8516 . . . . . 6 1o ∈ V
2524a1i 11 . . . . 5 ((𝜑𝑦𝐵) → 1o ∈ V)
26 1n0 8526 . . . . . 6 1o ≠ ∅
2726a1i 11 . . . . 5 ((𝜑𝑦𝐵) → 1o ≠ ∅)
2823, 25, 27fvconstr 48765 . . . 4 ((𝜑𝑦𝐵) → (𝑦 𝑦 ↔ (𝑦( × {1o})𝑦) = 1o))
2922, 28mpbid 232 . . 3 ((𝜑𝑦𝐵) → (𝑦( × {1o})𝑦) = 1o)
3012, 29eleqtrrid 2848 . 2 ((𝜑𝑦𝐵) → ∅ ∈ (𝑦( × {1o})𝑦))
31 0ov 7468 . . . . . 6 (⟨𝑥, 𝑦⟩∅𝑧) = ∅
3231oveqi 7444 . . . . 5 (𝑔(⟨𝑥, 𝑦⟩∅𝑧)𝑓) = (𝑔𝑓)
33 0ov 7468 . . . . 5 (𝑔𝑓) = ∅
3432, 33eqtri 2765 . . . 4 (𝑔(⟨𝑥, 𝑦⟩∅𝑧)𝑓) = ∅
3534, 12eqeltri 2837 . . 3 (𝑔(⟨𝑥, 𝑦⟩∅𝑧)𝑓) ∈ 1o
36 simpl 482 . . . . 5 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑓 ∈ (𝑥( × {1o})𝑦) ∧ 𝑔 ∈ (𝑦( × {1o})𝑧)))) → 𝜑)
3710adantr 480 . . . . . 6 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑓 ∈ (𝑥( × {1o})𝑦) ∧ 𝑔 ∈ (𝑦( × {1o})𝑧)))) → 𝐶 ∈ Proset )
381eleq2d 2827 . . . . . . . . 9 (𝜑 → (𝑥𝐵𝑥 ∈ (Base‘𝐶)))
391eleq2d 2827 . . . . . . . . 9 (𝜑 → (𝑧𝐵𝑧 ∈ (Base‘𝐶)))
4038, 13, 393anbi123d 1438 . . . . . . . 8 (𝜑 → ((𝑥𝐵𝑦𝐵𝑧𝐵) ↔ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))))
4140biimpa 476 . . . . . . 7 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵)) → (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)))
4241adantrr 717 . . . . . 6 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑓 ∈ (𝑥( × {1o})𝑦) ∧ 𝑔 ∈ (𝑦( × {1o})𝑧)))) → (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)))
43 eqidd 2738 . . . . . . . 8 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑓 ∈ (𝑥( × {1o})𝑦) ∧ 𝑔 ∈ (𝑦( × {1o})𝑧)))) → ( × {1o}) = ( × {1o}))
44 simprrl 781 . . . . . . . 8 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑓 ∈ (𝑥( × {1o})𝑦) ∧ 𝑔 ∈ (𝑦( × {1o})𝑧)))) → 𝑓 ∈ (𝑥( × {1o})𝑦))
4543, 44fvconstr2 48767 . . . . . . 7 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑓 ∈ (𝑥( × {1o})𝑦) ∧ 𝑔 ∈ (𝑦( × {1o})𝑧)))) → 𝑥 𝑦)
4619breqd 5154 . . . . . . . 8 (𝜑 → (𝑥 𝑦𝑥(le‘𝐶)𝑦))
4746biimpd 229 . . . . . . 7 (𝜑 → (𝑥 𝑦𝑥(le‘𝐶)𝑦))
4836, 45, 47sylc 65 . . . . . 6 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑓 ∈ (𝑥( × {1o})𝑦) ∧ 𝑔 ∈ (𝑦( × {1o})𝑧)))) → 𝑥(le‘𝐶)𝑦)
49 simprrr 782 . . . . . . . 8 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑓 ∈ (𝑥( × {1o})𝑦) ∧ 𝑔 ∈ (𝑦( × {1o})𝑧)))) → 𝑔 ∈ (𝑦( × {1o})𝑧))
5043, 49fvconstr2 48767 . . . . . . 7 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑓 ∈ (𝑥( × {1o})𝑦) ∧ 𝑔 ∈ (𝑦( × {1o})𝑧)))) → 𝑦 𝑧)
5119breqd 5154 . . . . . . . 8 (𝜑 → (𝑦 𝑧𝑦(le‘𝐶)𝑧))
5251biimpd 229 . . . . . . 7 (𝜑 → (𝑦 𝑧𝑦(le‘𝐶)𝑧))
5336, 50, 52sylc 65 . . . . . 6 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑓 ∈ (𝑥( × {1o})𝑦) ∧ 𝑔 ∈ (𝑦( × {1o})𝑧)))) → 𝑦(le‘𝐶)𝑧)
5414, 15prstr 18345 . . . . . 6 ((𝐶 ∈ Proset ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑥(le‘𝐶)𝑦𝑦(le‘𝐶)𝑧)) → 𝑥(le‘𝐶)𝑧)
5537, 42, 48, 53, 54syl112anc 1376 . . . . 5 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑓 ∈ (𝑥( × {1o})𝑦) ∧ 𝑔 ∈ (𝑦( × {1o})𝑧)))) → 𝑥(le‘𝐶)𝑧)
5619breqd 5154 . . . . . 6 (𝜑 → (𝑥 𝑧𝑥(le‘𝐶)𝑧))
5756biimprd 248 . . . . 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 48765 . . . 4 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑓 ∈ (𝑥( × {1o})𝑦) ∧ 𝑔 ∈ (𝑦( × {1o})𝑧)))) → (𝑥 𝑧 ↔ (𝑥( × {1o})𝑧) = 1o))
6258, 61mpbid 232 . . 3 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑓 ∈ (𝑥( × {1o})𝑦) ∧ 𝑔 ∈ (𝑦( × {1o})𝑧)))) → (𝑥( × {1o})𝑧) = 1o)
6335, 62eleqtrrid 2848 . 2 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑓 ∈ (𝑥( × {1o})𝑦) ∧ 𝑔 ∈ (𝑦( × {1o})𝑧)))) → (𝑔(⟨𝑥, 𝑦⟩∅𝑧)𝑓) ∈ (𝑥( × {1o})𝑧))
641, 2, 8, 9, 10, 11, 30, 63isthincd2 49086 1 (𝜑 → (𝐶 ∈ ThinCat ∧ (Id‘𝐶) = (𝑦𝐵 ↦ ∅)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3a 1087   = wceq 1540  wcel 2108  ∃*wmo 2538  wne 2940  Vcvv 3480  c0 4333  {csn 4626  cop 4632   class class class wbr 5143  cmpt 5225   × cxp 5683  cfv 6561  (class class class)co 7431  1oc1o 8499  Basecbs 17247  lecple 17304  Hom chom 17308  compcco 17309  Idccid 17708   Proset cproset 18338  ThinCatcthinc 49067
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pr 5432
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-riota 7388  df-ov 7434  df-1o 8506  df-cat 17711  df-cid 17712  df-proset 18340  df-thinc 49068
This theorem is referenced by:  prstcthin  49165
  Copyright terms: Public domain W3C validator