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 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 = { 𝑓 ∣ ∃ 𝑏 ∃ 𝑟 ( 𝑏 = ( Base ‘ 𝑓 ) ∧ 𝑟 = ( le ‘ 𝑓 ) ∧ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑥 ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ) ) } |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cpo | ⊢ Poset | |
| 1 | vf | ⊢ 𝑓 | |
| 2 | vb | ⊢ 𝑏 | |
| 3 | vr | ⊢ 𝑟 | |
| 4 | 2 | cv | ⊢ 𝑏 |
| 5 | cbs | ⊢ Base | |
| 6 | 1 | cv | ⊢ 𝑓 |
| 7 | 6 5 | cfv | ⊢ ( Base ‘ 𝑓 ) |
| 8 | 4 7 | wceq | ⊢ 𝑏 = ( Base ‘ 𝑓 ) |
| 9 | 3 | cv | ⊢ 𝑟 |
| 10 | cple | ⊢ le | |
| 11 | 6 10 | cfv | ⊢ ( le ‘ 𝑓 ) |
| 12 | 9 11 | wceq | ⊢ 𝑟 = ( le ‘ 𝑓 ) |
| 13 | vx | ⊢ 𝑥 | |
| 14 | vy | ⊢ 𝑦 | |
| 15 | vz | ⊢ 𝑧 | |
| 16 | 13 | cv | ⊢ 𝑥 |
| 17 | 16 16 9 | wbr | ⊢ 𝑥 𝑟 𝑥 |
| 18 | 14 | cv | ⊢ 𝑦 |
| 19 | 16 18 9 | wbr | ⊢ 𝑥 𝑟 𝑦 |
| 20 | 18 16 9 | wbr | ⊢ 𝑦 𝑟 𝑥 |
| 21 | 19 20 | wa | ⊢ ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑥 ) |
| 22 | 16 18 | wceq | ⊢ 𝑥 = 𝑦 |
| 23 | 21 22 | wi | ⊢ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑥 ) → 𝑥 = 𝑦 ) |
| 24 | 15 | cv | ⊢ 𝑧 |
| 25 | 18 24 9 | wbr | ⊢ 𝑦 𝑟 𝑧 |
| 26 | 19 25 | wa | ⊢ ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) |
| 27 | 16 24 9 | wbr | ⊢ 𝑥 𝑟 𝑧 |
| 28 | 26 27 | wi | ⊢ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) |
| 29 | 17 23 28 | w3a | ⊢ ( 𝑥 𝑟 𝑥 ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ) |
| 30 | 29 15 4 | wral | ⊢ ∀ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑥 ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ) |
| 31 | 30 14 4 | wral | ⊢ ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑥 ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ) |
| 32 | 31 13 4 | wral | ⊢ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑥 ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ) |
| 33 | 8 12 32 | w3a | ⊢ ( 𝑏 = ( Base ‘ 𝑓 ) ∧ 𝑟 = ( le ‘ 𝑓 ) ∧ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑥 ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ) ) |
| 34 | 33 3 | wex | ⊢ ∃ 𝑟 ( 𝑏 = ( Base ‘ 𝑓 ) ∧ 𝑟 = ( le ‘ 𝑓 ) ∧ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑥 ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ) ) |
| 35 | 34 2 | wex | ⊢ ∃ 𝑏 ∃ 𝑟 ( 𝑏 = ( Base ‘ 𝑓 ) ∧ 𝑟 = ( le ‘ 𝑓 ) ∧ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑥 ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ) ) |
| 36 | 35 1 | cab | ⊢ { 𝑓 ∣ ∃ 𝑏 ∃ 𝑟 ( 𝑏 = ( Base ‘ 𝑓 ) ∧ 𝑟 = ( le ‘ 𝑓 ) ∧ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑥 ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ) ) } |
| 37 | 0 36 | wceq | ⊢ Poset = { 𝑓 ∣ ∃ 𝑏 ∃ 𝑟 ( 𝑏 = ( Base ‘ 𝑓 ) ∧ 𝑟 = ( le ‘ 𝑓 ) ∧ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑥 ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ) ) } |