MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-poset Structured version   Visualization version   GIF version

Definition df-poset 17546
Description: Define the class of partially ordered sets (posets). A poset is a set equipped with a partial order, that is, a binary relation which is reflexive, antisymmetric, and transitive. Unlike a total order, in a partial order there may be pairs of elements where neither precedes the other. Definition of poset in [Crawley] p. 1. Note that Crawley-Dilworth require that a poset base set be nonempty, but we follow the convention of most authors who don't make this a requirement.

In our formalism of extensible structures, the base set of a poset 𝑓 is denoted by (Base‘𝑓) and its partial order by (le‘𝑓) (for "less than or equal to"). The quantifiers 𝑏𝑟 provide a notational shorthand to allow us to refer to the base and ordering relation as 𝑏 and 𝑟 in the definition rather than having to repeat (Base‘𝑓) and (le‘𝑓) throughout. These quantifiers can be eliminated with ceqsex2v 3545 and related theorems. (Contributed by NM, 18-Oct-2012.)

Assertion
Ref Expression
df-poset Poset = {𝑓 ∣ ∃𝑏𝑟(𝑏 = (Base‘𝑓) ∧ 𝑟 = (le‘𝑓) ∧ ∀𝑥𝑏𝑦𝑏𝑧𝑏 (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦𝑦𝑟𝑥) → 𝑥 = 𝑦) ∧ ((𝑥𝑟𝑦𝑦𝑟𝑧) → 𝑥𝑟𝑧)))}
Distinct variable group:   𝑓,𝑏,𝑟,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-poset
StepHypRef Expression
1 cpo 17540 . 2 class Poset
2 vb . . . . . . . 8 setvar 𝑏
32cv 1527 . . . . . . 7 class 𝑏
4 vf . . . . . . . . 9 setvar 𝑓
54cv 1527 . . . . . . . 8 class 𝑓
6 cbs 16473 . . . . . . . 8 class Base
75, 6cfv 6349 . . . . . . 7 class (Base‘𝑓)
83, 7wceq 1528 . . . . . 6 wff 𝑏 = (Base‘𝑓)
9 vr . . . . . . . 8 setvar 𝑟
109cv 1527 . . . . . . 7 class 𝑟
11 cple 16562 . . . . . . . 8 class le
125, 11cfv 6349 . . . . . . 7 class (le‘𝑓)
1310, 12wceq 1528 . . . . . 6 wff 𝑟 = (le‘𝑓)
14 vx . . . . . . . . . . . 12 setvar 𝑥
1514cv 1527 . . . . . . . . . . 11 class 𝑥
1615, 15, 10wbr 5058 . . . . . . . . . 10 wff 𝑥𝑟𝑥
17 vy . . . . . . . . . . . . . 14 setvar 𝑦
1817cv 1527 . . . . . . . . . . . . 13 class 𝑦
1915, 18, 10wbr 5058 . . . . . . . . . . . 12 wff 𝑥𝑟𝑦
2018, 15, 10wbr 5058 . . . . . . . . . . . 12 wff 𝑦𝑟𝑥
2119, 20wa 396 . . . . . . . . . . 11 wff (𝑥𝑟𝑦𝑦𝑟𝑥)
2214, 17weq 1955 . . . . . . . . . . 11 wff 𝑥 = 𝑦
2321, 22wi 4 . . . . . . . . . 10 wff ((𝑥𝑟𝑦𝑦𝑟𝑥) → 𝑥 = 𝑦)
24 vz . . . . . . . . . . . . . 14 setvar 𝑧
2524cv 1527 . . . . . . . . . . . . 13 class 𝑧
2618, 25, 10wbr 5058 . . . . . . . . . . . 12 wff 𝑦𝑟𝑧
2719, 26wa 396 . . . . . . . . . . 11 wff (𝑥𝑟𝑦𝑦𝑟𝑧)
2815, 25, 10wbr 5058 . . . . . . . . . . 11 wff 𝑥𝑟𝑧
2927, 28wi 4 . . . . . . . . . 10 wff ((𝑥𝑟𝑦𝑦𝑟𝑧) → 𝑥𝑟𝑧)
3016, 23, 29w3a 1079 . . . . . . . . 9 wff (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦𝑦𝑟𝑥) → 𝑥 = 𝑦) ∧ ((𝑥𝑟𝑦𝑦𝑟𝑧) → 𝑥𝑟𝑧))
3130, 24, 3wral 3138 . . . . . . . 8 wff 𝑧𝑏 (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦𝑦𝑟𝑥) → 𝑥 = 𝑦) ∧ ((𝑥𝑟𝑦𝑦𝑟𝑧) → 𝑥𝑟𝑧))
3231, 17, 3wral 3138 . . . . . . 7 wff 𝑦𝑏𝑧𝑏 (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦𝑦𝑟𝑥) → 𝑥 = 𝑦) ∧ ((𝑥𝑟𝑦𝑦𝑟𝑧) → 𝑥𝑟𝑧))
3332, 14, 3wral 3138 . . . . . 6 wff 𝑥𝑏𝑦𝑏𝑧𝑏 (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦𝑦𝑟𝑥) → 𝑥 = 𝑦) ∧ ((𝑥𝑟𝑦𝑦𝑟𝑧) → 𝑥𝑟𝑧))
348, 13, 33w3a 1079 . . . . 5 wff (𝑏 = (Base‘𝑓) ∧ 𝑟 = (le‘𝑓) ∧ ∀𝑥𝑏𝑦𝑏𝑧𝑏 (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦𝑦𝑟𝑥) → 𝑥 = 𝑦) ∧ ((𝑥𝑟𝑦𝑦𝑟𝑧) → 𝑥𝑟𝑧)))
3534, 9wex 1771 . . . 4 wff 𝑟(𝑏 = (Base‘𝑓) ∧ 𝑟 = (le‘𝑓) ∧ ∀𝑥𝑏𝑦𝑏𝑧𝑏 (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦𝑦𝑟𝑥) → 𝑥 = 𝑦) ∧ ((𝑥𝑟𝑦𝑦𝑟𝑧) → 𝑥𝑟𝑧)))
3635, 2wex 1771 . . 3 wff 𝑏𝑟(𝑏 = (Base‘𝑓) ∧ 𝑟 = (le‘𝑓) ∧ ∀𝑥𝑏𝑦𝑏𝑧𝑏 (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦𝑦𝑟𝑥) → 𝑥 = 𝑦) ∧ ((𝑥𝑟𝑦𝑦𝑟𝑧) → 𝑥𝑟𝑧)))
3736, 4cab 2799 . 2 class {𝑓 ∣ ∃𝑏𝑟(𝑏 = (Base‘𝑓) ∧ 𝑟 = (le‘𝑓) ∧ ∀𝑥𝑏𝑦𝑏𝑧𝑏 (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦𝑦𝑟𝑥) → 𝑥 = 𝑦) ∧ ((𝑥𝑟𝑦𝑦𝑟𝑧) → 𝑥𝑟𝑧)))}
381, 37wceq 1528 1 wff Poset = {𝑓 ∣ ∃𝑏𝑟(𝑏 = (Base‘𝑓) ∧ 𝑟 = (le‘𝑓) ∧ ∀𝑥𝑏𝑦𝑏𝑧𝑏 (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦𝑦𝑟𝑥) → 𝑥 = 𝑦) ∧ ((𝑥𝑟𝑦𝑦𝑟𝑧) → 𝑥𝑟𝑧)))}
Colors of variables: wff setvar class
This definition is referenced by:  ispos  17547
  Copyright terms: Public domain W3C validator