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 \| \exists b \exists r (b = {Base}_{f} \land r = \leq_{f} \land \forall x \in b \forall y \in b \forall z \in b (x r x \land ((x r y \land y r x) \to x = y) \land ((x r y \land y r z) \to 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 \leq_{f}$
12	9 11	wceq	$wff r = \leq_{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 \land y r x)$
22	16 18	wceq	$wff x = y$
23	21 22	wi	$wff ((x r y \land y r x) \to x = y)$
24	15	cv	$setvar z$
25	18 24 9	wbr	$wff y r z$
26	19 25	wa	$wff (x r y \land y r z)$
27	16 24 9	wbr	$wff x r z$
28	26 27	wi	$wff ((x r y \land y r z) \to x r z)$
29	17 23 28	w3a	$wff (x r x \land ((x r y \land y r x) \to x = y) \land ((x r y \land y r z) \to x r z))$
30	29 15 4	wral	$wff \forall z \in b (x r x \land ((x r y \land y r x) \to x = y) \land ((x r y \land y r z) \to x r z))$
31	30 14 4	wral	$wff \forall y \in b \forall z \in b (x r x \land ((x r y \land y r x) \to x = y) \land ((x r y \land y r z) \to x r z))$
32	31 13 4	wral	$wff \forall x \in b \forall y \in b \forall z \in b (x r x \land ((x r y \land y r x) \to x = y) \land ((x r y \land y r z) \to x r z))$
33	8 12 32	w3a	$wff (b = {Base}_{f} \land r = \leq_{f} \land \forall x \in b \forall y \in b \forall z \in b (x r x \land ((x r y \land y r x) \to x = y) \land ((x r y \land y r z) \to x r z)))$
34	33 3	wex	$wff \exists r (b = {Base}_{f} \land r = \leq_{f} \land \forall x \in b \forall y \in b \forall z \in b (x r x \land ((x r y \land y r x) \to x = y) \land ((x r y \land y r z) \to x r z)))$
35	34 2	wex	$wff \exists b \exists r (b = {Base}_{f} \land r = \leq_{f} \land \forall x \in b \forall y \in b \forall z \in b (x r x \land ((x r y \land y r x) \to x = y) \land ((x r y \land y r z) \to x r z)))$
36	35 1	cab	$class \{f \| \exists b \exists r (b = {Base}_{f} \land r = \leq_{f} \land \forall x \in b \forall y \in b \forall z \in b (x r x \land ((x r y \land y r x) \to x = y) \land ((x r y \land y r z) \to x r z)))\}$
37	0 36	wceq	$wff Poset = \{f \| \exists b \exists r (b = {Base}_{f} \land r = \leq_{f} \land \forall x \in b \forall y \in b \forall z \in b (x r x \land ((x r y \land y r x) \to x = y) \land ((x r y \land y r z) \to x r z)))\}$

Metamath Proof Explorer

Definition df-poset

Detailed syntax breakdown