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

Definition df-poset 13924
Description: Define the class of posets. 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.

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 the definition rather than having to repeat  (
Base `  f ) and  ( le `  f ) throughout. These quantifiers can be eliminated with ceqsex2v 2763 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
StepHypRef Expression
1 cpo 13918 . 2  class  Poset
2 vb . . . . . . . 8  set  b
32cv 1618 . . . . . . 7  class  b
4 vf . . . . . . . . 9  set  f
54cv 1618 . . . . . . . 8  class  f
6 cbs 13022 . . . . . . . 8  class  Base
75, 6cfv 4592 . . . . . . 7  class  ( Base `  f )
83, 7wceq 1619 . . . . . 6  wff  b  =  ( Base `  f
)
9 vr . . . . . . . 8  set  r
109cv 1618 . . . . . . 7  class  r
11 cple 13089 . . . . . . . 8  class  le
125, 11cfv 4592 . . . . . . 7  class  ( le
`  f )
1310, 12wceq 1619 . . . . . 6  wff  r  =  ( le `  f
)
14 vx . . . . . . . . . . . 12  set  x
1514cv 1618 . . . . . . . . . . 11  class  x
1615, 15, 10wbr 3920 . . . . . . . . . 10  wff  x r x
17 vy . . . . . . . . . . . . . 14  set  y
1817cv 1618 . . . . . . . . . . . . 13  class  y
1915, 18, 10wbr 3920 . . . . . . . . . . . 12  wff  x r y
2018, 15, 10wbr 3920 . . . . . . . . . . . 12  wff  y r x
2119, 20wa 360 . . . . . . . . . . 11  wff  ( x r y  /\  y
r x )
2214, 17weq 1620 . . . . . . . . . . 11  wff  x  =  y
2321, 22wi 6 . . . . . . . . . 10  wff  ( ( x r y  /\  y r x )  ->  x  =  y )
24 vz . . . . . . . . . . . . . 14  set  z
2524cv 1618 . . . . . . . . . . . . 13  class  z
2618, 25, 10wbr 3920 . . . . . . . . . . . 12  wff  y r z
2719, 26wa 360 . . . . . . . . . . 11  wff  ( x r y  /\  y
r z )
2815, 25, 10wbr 3920 . . . . . . . . . . 11  wff  x r z
2927, 28wi 6 . . . . . . . . . 10  wff  ( ( x r y  /\  y r z )  ->  x r z )
3016, 23, 29w3a 939 . . . . . . . . 9  wff  ( x r x  /\  (
( x r y  /\  y r x )  ->  x  =  y )  /\  (
( x r y  /\  y r z )  ->  x r
z ) )
3130, 24, 3wral 2509 . . . . . . . 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 ) )
3231, 17, 3wral 2509 . . . . . . 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 ) )
3332, 14, 3wral 2509 . . . . . 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 ) )
348, 13, 33w3a 939 . . . . 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 ) ) )
3534, 9wex 1537 . . . 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 ) ) )
3635, 2wex 1537 . . 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 ) ) )
3736, 4cab 2239 . 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 ) ) ) }
381, 37wceq 1619 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 ) ) ) }
Colors of variables: wff set class
This definition is referenced by:  ispos  13925
  Copyright terms: Public domain W3C validator