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 48855
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 48800 and catprs2 48801 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 2736 . . . 4 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → ( × {1o}) = ( × {1o}))
43f1omo 48691 . . 3 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → ∃*𝑓 𝑓 ∈ (( × {1o})‘⟨𝑥, 𝑦⟩))
5 df-ov 7434 . . . . 5 (𝑥( × {1o})𝑦) = (( × {1o})‘⟨𝑥, 𝑦⟩)
65eleq2i 2831 . . . 4 (𝑓 ∈ (𝑥( × {1o})𝑦) ↔ 𝑓 ∈ (( × {1o})‘⟨𝑥, 𝑦⟩))
76mobii 2546 . . 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 8541 . . 3 ∅ ∈ 1o
131eleq2d 2825 . . . . . 6 (𝜑 → (𝑦𝐵𝑦 ∈ (Base‘𝐶)))
14 eqid 2735 . . . . . . . 8 (Base‘𝐶) = (Base‘𝐶)
15 eqid 2735 . . . . . . . 8 (le‘𝐶) = (le‘𝐶)
1614, 15prsref 18356 . . . . . . 7 ((𝐶 ∈ Proset ∧ 𝑦 ∈ (Base‘𝐶)) → 𝑦(le‘𝐶)𝑦)
1710, 16sylan 580 . . . . . 6 ((𝜑𝑦 ∈ (Base‘𝐶)) → 𝑦(le‘𝐶)𝑦)
1813, 17sylbida 592 . . . . 5 ((𝜑𝑦𝐵) → 𝑦(le‘𝐶)𝑦)
19 prsthinc.l . . . . . . 7 (𝜑 = (le‘𝐶))
2019breqd 5159 . . . . . 6 (𝜑 → (𝑦 𝑦𝑦(le‘𝐶)𝑦))
2120biimpar 477 . . . . 5 ((𝜑𝑦(le‘𝐶)𝑦) → 𝑦 𝑦)
2218, 21syldan 591 . . . 4 ((𝜑𝑦𝐵) → 𝑦 𝑦)
23 eqidd 2736 . . . . 5 ((𝜑𝑦𝐵) → ( × {1o}) = ( × {1o}))
24 1oex 8515 . . . . . 6 1o ∈ V
2524a1i 11 . . . . 5 ((𝜑𝑦𝐵) → 1o ∈ V)
26 1n0 8525 . . . . . 6 1o ≠ ∅
2726a1i 11 . . . . 5 ((𝜑𝑦𝐵) → 1o ≠ ∅)
2823, 25, 27fvconstr 48686 . . . 4 ((𝜑𝑦𝐵) → (𝑦 𝑦 ↔ (𝑦( × {1o})𝑦) = 1o))
2922, 28mpbid 232 . . 3 ((𝜑𝑦𝐵) → (𝑦( × {1o})𝑦) = 1o)
3012, 29eleqtrrid 2846 . 2 ((𝜑𝑦𝐵) → ∅ ∈ (𝑦( × {1o})𝑦))
31 0ov 7468 . . . . . 6 (⟨𝑥, 𝑦⟩∅𝑧) = ∅
3231oveqi 7444 . . . . 5 (𝑔(⟨𝑥, 𝑦⟩∅𝑧)𝑓) = (𝑔𝑓)
33 0ov 7468 . . . . 5 (𝑔𝑓) = ∅
3432, 33eqtri 2763 . . . 4 (𝑔(⟨𝑥, 𝑦⟩∅𝑧)𝑓) = ∅
3534, 12eqeltri 2835 . . 3 (𝑔(⟨𝑥, 𝑦⟩∅𝑧)𝑓) ∈ 1o
36 simpl 482 . . . . 5 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑓 ∈ (𝑥( × {1o})𝑦) ∧ 𝑔 ∈ (𝑦( × {1o})𝑧)))) → 𝜑)
3710adantr 480 . . . . . 6 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑓 ∈ (𝑥( × {1o})𝑦) ∧ 𝑔 ∈ (𝑦( × {1o})𝑧)))) → 𝐶 ∈ Proset )
381eleq2d 2825 . . . . . . . . 9 (𝜑 → (𝑥𝐵𝑥 ∈ (Base‘𝐶)))
391eleq2d 2825 . . . . . . . . 9 (𝜑 → (𝑧𝐵𝑧 ∈ (Base‘𝐶)))
4038, 13, 393anbi123d 1435 . . . . . . . 8 (𝜑 → ((𝑥𝐵𝑦𝐵𝑧𝐵) ↔ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))))
4140biimpa 476 . . . . . . 7 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵)) → (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)))
4241adantrr 717 . . . . . 6 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑓 ∈ (𝑥( × {1o})𝑦) ∧ 𝑔 ∈ (𝑦( × {1o})𝑧)))) → (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)))
43 eqidd 2736 . . . . . . . 8 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑓 ∈ (𝑥( × {1o})𝑦) ∧ 𝑔 ∈ (𝑦( × {1o})𝑧)))) → ( × {1o}) = ( × {1o}))
44 simprrl 781 . . . . . . . 8 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑓 ∈ (𝑥( × {1o})𝑦) ∧ 𝑔 ∈ (𝑦( × {1o})𝑧)))) → 𝑓 ∈ (𝑥( × {1o})𝑦))
4543, 44fvconstr2 48688 . . . . . . 7 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑓 ∈ (𝑥( × {1o})𝑦) ∧ 𝑔 ∈ (𝑦( × {1o})𝑧)))) → 𝑥 𝑦)
4619breqd 5159 . . . . . . . 8 (𝜑 → (𝑥 𝑦𝑥(le‘𝐶)𝑦))
4746biimpd 229 . . . . . . 7 (𝜑 → (𝑥 𝑦𝑥(le‘𝐶)𝑦))
4836, 45, 47sylc 65 . . . . . 6 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑓 ∈ (𝑥( × {1o})𝑦) ∧ 𝑔 ∈ (𝑦( × {1o})𝑧)))) → 𝑥(le‘𝐶)𝑦)
49 simprrr 782 . . . . . . . 8 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑓 ∈ (𝑥( × {1o})𝑦) ∧ 𝑔 ∈ (𝑦( × {1o})𝑧)))) → 𝑔 ∈ (𝑦( × {1o})𝑧))
5043, 49fvconstr2 48688 . . . . . . 7 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑓 ∈ (𝑥( × {1o})𝑦) ∧ 𝑔 ∈ (𝑦( × {1o})𝑧)))) → 𝑦 𝑧)
5119breqd 5159 . . . . . . . 8 (𝜑 → (𝑦 𝑧𝑦(le‘𝐶)𝑧))
5251biimpd 229 . . . . . . 7 (𝜑 → (𝑦 𝑧𝑦(le‘𝐶)𝑧))
5336, 50, 52sylc 65 . . . . . 6 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑓 ∈ (𝑥( × {1o})𝑦) ∧ 𝑔 ∈ (𝑦( × {1o})𝑧)))) → 𝑦(le‘𝐶)𝑧)
5414, 15prstr 18357 . . . . . 6 ((𝐶 ∈ Proset ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑥(le‘𝐶)𝑦𝑦(le‘𝐶)𝑧)) → 𝑥(le‘𝐶)𝑧)
5537, 42, 48, 53, 54syl112anc 1373 . . . . 5 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑓 ∈ (𝑥( × {1o})𝑦) ∧ 𝑔 ∈ (𝑦( × {1o})𝑧)))) → 𝑥(le‘𝐶)𝑧)
5619breqd 5159 . . . . . 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 48686 . . . 4 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑓 ∈ (𝑥( × {1o})𝑦) ∧ 𝑔 ∈ (𝑦( × {1o})𝑧)))) → (𝑥 𝑧 ↔ (𝑥( × {1o})𝑧) = 1o))
6258, 61mpbid 232 . . 3 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑓 ∈ (𝑥( × {1o})𝑦) ∧ 𝑔 ∈ (𝑦( × {1o})𝑧)))) → (𝑥( × {1o})𝑧) = 1o)
6335, 62eleqtrrid 2846 . 2 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑓 ∈ (𝑥( × {1o})𝑦) ∧ 𝑔 ∈ (𝑦( × {1o})𝑧)))) → (𝑔(⟨𝑥, 𝑦⟩∅𝑧)𝑓) ∈ (𝑥( × {1o})𝑧))
641, 2, 8, 9, 10, 11, 30, 63isthincd2 48838 1 (𝜑 → (𝐶 ∈ ThinCat ∧ (Id‘𝐶) = (𝑦𝐵 ↦ ∅)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3a 1086   = wceq 1537  wcel 2106  ∃*wmo 2536  wne 2938  Vcvv 3478  c0 4339  {csn 4631  cop 4637   class class class wbr 5148  cmpt 5231   × cxp 5687  cfv 6563  (class class class)co 7431  1oc1o 8498  Basecbs 17245  lecple 17305  Hom chom 17309  compcco 17310  Idccid 17710   Proset cproset 18350  ThinCatcthinc 48819
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-rep 5285  ax-sep 5302  ax-nul 5312  ax-pr 5438
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-rmo 3378  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5583  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-suc 6392  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-riota 7388  df-ov 7434  df-1o 8505  df-cat 17713  df-cid 17714  df-proset 18352  df-thinc 48820
This theorem is referenced by:  prstcthin  48877
  Copyright terms: Public domain W3C validator