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

Definition df-poset 14405
 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 provide a notational shorthand to allow us to refer to the base and ordering relation as and the definition rather than having to repeat and throughout. These quantifiers can be eliminated with ceqsex2v 2995 and related theorems. (Contributed by NM, 18-Oct-2012.)
Assertion
Ref Expression
df-poset
Distinct variable group:   ,,,,,

Detailed syntax breakdown of Definition df-poset
StepHypRef Expression
1 cpo 14399 . 2
2 vb . . . . . . . 8
32cv 1652 . . . . . . 7
4 vf . . . . . . . . 9
54cv 1652 . . . . . . . 8
6 cbs 13471 . . . . . . . 8
75, 6cfv 5456 . . . . . . 7
83, 7wceq 1653 . . . . . 6
9 vr . . . . . . . 8
109cv 1652 . . . . . . 7
11 cple 13538 . . . . . . . 8
125, 11cfv 5456 . . . . . . 7
1310, 12wceq 1653 . . . . . 6
14 vx . . . . . . . . . . . 12
1514cv 1652 . . . . . . . . . . 11
1615, 15, 10wbr 4214 . . . . . . . . . 10
17 vy . . . . . . . . . . . . . 14
1817cv 1652 . . . . . . . . . . . . 13
1915, 18, 10wbr 4214 . . . . . . . . . . . 12
2018, 15, 10wbr 4214 . . . . . . . . . . . 12
2119, 20wa 360 . . . . . . . . . . 11
2214, 17weq 1654 . . . . . . . . . . 11
2321, 22wi 4 . . . . . . . . . 10
24 vz . . . . . . . . . . . . . 14
2524cv 1652 . . . . . . . . . . . . 13
2618, 25, 10wbr 4214 . . . . . . . . . . . 12
2719, 26wa 360 . . . . . . . . . . 11
2815, 25, 10wbr 4214 . . . . . . . . . . 11
2927, 28wi 4 . . . . . . . . . 10
3016, 23, 29w3a 937 . . . . . . . . 9
3130, 24, 3wral 2707 . . . . . . . 8
3231, 17, 3wral 2707 . . . . . . 7
3332, 14, 3wral 2707 . . . . . 6
348, 13, 33w3a 937 . . . . 5
3534, 9wex 1551 . . . 4
3635, 2wex 1551 . . 3
3736, 4cab 2424 . 2
381, 37wceq 1653 1
 Colors of variables: wff set class This definition is referenced by:  ispos  14406
 Copyright terms: Public domain W3C validator