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

Definition df-poset 14358
 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 2953 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 14352 . 2
2 vb . . . . . . . 8
32cv 1648 . . . . . . 7
4 vf . . . . . . . . 9
54cv 1648 . . . . . . . 8
6 cbs 13424 . . . . . . . 8
75, 6cfv 5413 . . . . . . 7
83, 7wceq 1649 . . . . . 6
9 vr . . . . . . . 8
109cv 1648 . . . . . . 7
11 cple 13491 . . . . . . . 8
125, 11cfv 5413 . . . . . . 7
1310, 12wceq 1649 . . . . . 6
14 vx . . . . . . . . . . . 12
1514cv 1648 . . . . . . . . . . 11
1615, 15, 10wbr 4172 . . . . . . . . . 10
17 vy . . . . . . . . . . . . . 14
1817cv 1648 . . . . . . . . . . . . 13
1915, 18, 10wbr 4172 . . . . . . . . . . . 12
2018, 15, 10wbr 4172 . . . . . . . . . . . 12
2119, 20wa 359 . . . . . . . . . . 11
2214, 17weq 1650 . . . . . . . . . . 11
2321, 22wi 4 . . . . . . . . . 10
24 vz . . . . . . . . . . . . . 14
2524cv 1648 . . . . . . . . . . . . 13
2618, 25, 10wbr 4172 . . . . . . . . . . . 12
2719, 26wa 359 . . . . . . . . . . 11
2815, 25, 10wbr 4172 . . . . . . . . . . 11
2927, 28wi 4 . . . . . . . . . 10
3016, 23, 29w3a 936 . . . . . . . . 9
3130, 24, 3wral 2666 . . . . . . . 8
3231, 17, 3wral 2666 . . . . . . 7
3332, 14, 3wral 2666 . . . . . 6
348, 13, 33w3a 936 . . . . 5
3534, 9wex 1547 . . . 4
3635, 2wex 1547 . . 3
3736, 4cab 2390 . 2
381, 37wceq 1649 1
 Colors of variables: wff set class This definition is referenced by:  ispos  14359
 Copyright terms: Public domain W3C validator