Metamath Proof Explorer

Definition df-poset

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 f is denoted by ( Basef ) and its partial order by ( lef ) (for "less than or equal to"). The quantifiers E. b E. r provide a notational shorthand to allow to refer to the base and ordering relation as b and r in the definition rather than having to repeat ( Basef ) and ( lef ) throughout. These quantifiers can be eliminated with ceqsex2v and related theorems. (Contributed by NM, 18-Oct-2012)

Ref Expression
Assertion df-poset ⊢ Poset = f | ∃ b ∃ r b = Base f ∧ r = ≤ f ∧ ∀ x ∈ b ∀ y ∈ b ∀ z ∈ b x r x ∧ x r y ∧ y r x → x = y ∧ x r y ∧ y r z → x r z

Detailed syntax breakdown

Step Hyp Ref Expression
0 cpo class Poset
1 vf setvar f
2 vb setvar b
3 vr setvar r
4 2 cv setvar b
5 cbs class Base
6 1 cv setvar f
7 6 5 cfv class Base f
8 4 7 wceq wff b = Base f
9 3 cv setvar r
10 cple class le
11 6 10 cfv class ≤ f
12 9 11 wceq wff r = ≤ f
13 vx setvar x
14 vy setvar y
15 vz setvar z
16 13 cv setvar x
17 16 16 9 wbr wff x r x
18 14 cv setvar y
19 16 18 9 wbr wff x r y
20 18 16 9 wbr wff y r x
21 19 20 wa wff x r y ∧ y r x
22 16 18 wceq wff x = y
23 21 22 wi wff x r y ∧ y r x → x = y
24 15 cv setvar z
25 18 24 9 wbr wff y r z
26 19 25 wa wff x r y ∧ y r z
27 16 24 9 wbr wff x r z
28 26 27 wi wff x r y ∧ y r z → x r z
29 17 23 28 w3a wff x r x ∧ x r y ∧ y r x → x = y ∧ x r y ∧ y r z → x r z
30 29 15 4 wral wff ∀ z ∈ b x r x ∧ x r y ∧ y r x → x = y ∧ x r y ∧ y r z → x r z
31 30 14 4 wral wff ∀ y ∈ b ∀ z ∈ b x r x ∧ x r y ∧ y r x → x = y ∧ x r y ∧ y r z → x r z
32 31 13 4 wral wff ∀ x ∈ b ∀ y ∈ b ∀ z ∈ b x r x ∧ x r y ∧ y r x → x = y ∧ x r y ∧ y r z → x r z
33 8 12 32 w3a wff b = Base f ∧ r = ≤ f ∧ ∀ x ∈ b ∀ y ∈ b ∀ z ∈ b x r x ∧ x r y ∧ y r x → x = y ∧ x r y ∧ y r z → x r z
34 33 3 wex wff ∃ r b = Base f ∧ r = ≤ f ∧ ∀ x ∈ b ∀ y ∈ b ∀ z ∈ b x r x ∧ x r y ∧ y r x → x = y ∧ x r y ∧ y r z → x r z
35 34 2 wex wff ∃ b ∃ r b = Base f ∧ r = ≤ f ∧ ∀ x ∈ b ∀ y ∈ b ∀ z ∈ b x r x ∧ x r y ∧ y r x → x = y ∧ x r y ∧ y r z → x r z
36 35 1 cab class f | ∃ b ∃ r b = Base f ∧ r = ≤ f ∧ ∀ x ∈ b ∀ y ∈ b ∀ z ∈ b x r x ∧ x r y ∧ y r x → x = y ∧ x r y ∧ y r z → x r z
37 0 36 wceq wff Poset = f | ∃ b ∃ r b = Base f ∧ r = ≤ f ∧ ∀ x ∈ b ∀ y ∈ b ∀ z ∈ b x r x ∧ x r y ∧ y r x → x = y ∧ x r y ∧ y r z → x r z