Definition df-poset 16946

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 ( Base ` f ) and its partial order by ( le ` f ) (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 ( Base ` f ) and ( le ` f ) throughout. These quantifiers can be eliminated with ceqsex2v 3245 and related theorems. (Contributed by NM, 18-Oct-2012.)

Assertion

Ref	Expression
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 ) ) ) }

Distinct variable group:   f, b, r, x, y, z

Detailed syntax breakdown of Definition df-poset

Step	Hyp	Ref	Expression
1		cpo 16940	. 2 class Poset
2		vb	. . . . . . . 8 setvar b
3	2	cv 1482	. . . . . . 7 class b
4		vf	. . . . . . . . 9 setvar f
5	4	cv 1482	. . . . . . . 8 class f
6		cbs 15857	. . . . . . . 8 class Base
7	5, 6	cfv 5888	. . . . . . 7 class ( Base ` f )
8	3, 7	wceq 1483	. . . . . 6 wff b = ( Base ` f )
9		vr	. . . . . . . 8 setvar r
10	9	cv 1482	. . . . . . 7 class r
11		cple 15948	. . . . . . . 8 class le
12	5, 11	cfv 5888	. . . . . . 7 class ( le ` f )
13	10, 12	wceq 1483	. . . . . 6 wff r = ( le ` f )
14		vx	. . . . . . . . . . . 12 setvar x
15	14	cv 1482	. . . . . . . . . . 11 class x
16	15, 15, 10	wbr 4653	. . . . . . . . . 10 wff x r x
17		vy	. . . . . . . . . . . . . 14 setvar y
18	17	cv 1482	. . . . . . . . . . . . 13 class y
19	15, 18, 10	wbr 4653	. . . . . . . . . . . 12 wff x r y
20	18, 15, 10	wbr 4653	. . . . . . . . . . . 12 wff y r x
21	19, 20	wa 384	. . . . . . . . . . 11 wff ( x r y /\ y r x )
22	14, 17	weq 1874	. . . . . . . . . . 11 wff x = y
23	21, 22	wi 4	. . . . . . . . . 10 wff ( ( x r y /\ y r x ) -> x = y )
24		vz	. . . . . . . . . . . . . 14 setvar z
25	24	cv 1482	. . . . . . . . . . . . 13 class z
26	18, 25, 10	wbr 4653	. . . . . . . . . . . 12 wff y r z
27	19, 26	wa 384	. . . . . . . . . . 11 wff ( x r y /\ y r z )
28	15, 25, 10	wbr 4653	. . . . . . . . . . 11 wff x r z
29	27, 28	wi 4	. . . . . . . . . 10 wff ( ( x r y /\ y r z ) -> x r z )
30	16, 23, 29	w3a 1037	. . . . . . . . 9 wff ( x r x /\ ( ( x r y /\ y r x ) -> x = y ) /\ ( ( x r y /\ y r z ) -> x r z ) )
31	30, 24, 3	wral 2912	. . . . . . . 8 wff 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, 17, 3	wral 2912	. . . . . . 7 wff 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	32, 14, 3	wral 2912	. . . . . 6 wff 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	8, 13, 33	w3a 1037	. . . . 5 wff ( 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, 9	wex 1704	. . . 4 wff 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, 2	wex 1704	. . 3 wff 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	36, 4	cab 2608	. 2 class { 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 ) ) ) }
38	1, 37	wceq 1483	1 wff 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 ) ) ) }

This definition is referenced by:  ispos  16947