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 us 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 | E. b E. r ( b = ( Base ` f ) /\ r = ( le ` f ) /\ A. x e. b A. y e. b A. z e. 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	|- Poset
1		vf	|- f
2		vb	|- b
3		vr	|- r
4	2	cv	|- b
5		cbs	|- Base
6	1	cv	|- f
7	6 5	cfv	|- ( Base ` f )
8	4 7	wceq	|- b = ( Base ` f )
9	3	cv	|- r
10		cple	|- le
11	6 10	cfv	|- ( le ` f )
12	9 11	wceq	|- r = ( le ` f )
13		vx	|- x
14		vy	|- y
15		vz	|- z
16	13	cv	|- x
17	16 16 9	wbr	|- x r x
18	14	cv	|- y
19	16 18 9	wbr	|- x r y
20	18 16 9	wbr	|- y r x
21	19 20	wa	|- ( x r y /\ y r x )
22	16 18	wceq	|- x = y
23	21 22	wi	|- ( ( x r y /\ y r x ) -> x = y )
24	15	cv	|- z
25	18 24 9	wbr	|- y r z
26	19 25	wa	|- ( x r y /\ y r z )
27	16 24 9	wbr	|- x r z
28	26 27	wi	|- ( ( x r y /\ y r z ) -> x r z )
29	17 23 28	w3a	|- ( 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	|- A. z e. 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	|- A. y e. b A. z e. 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	|- A. x e. b A. y e. b A. z e. 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	|- ( b = ( Base ` f ) /\ r = ( le ` f ) /\ A. x e. b A. y e. b A. z e. 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	|- E. r ( b = ( Base ` f ) /\ r = ( le ` f ) /\ A. x e. b A. y e. b A. z e. 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	|- E. b E. r ( b = ( Base ` f ) /\ r = ( le ` f ) /\ A. x e. b A. y e. b A. z e. 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	|- { f | E. b E. r ( b = ( Base ` f ) /\ r = ( le ` f ) /\ A. x e. b A. y e. b A. z e. 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	|- Poset = { f | E. b E. r ( b = ( Base ` f ) /\ r = ( le ` f ) /\ A. x e. b A. y e. b A. z e. b ( x r x /\ ( ( x r y /\ y r x ) -> x = y ) /\ ( ( x r y /\ y r z ) -> x r z ) ) ) }