Description: Define the class of preordered sets, or prosets. A proset is a set equipped with a preorder, that is, a transitive and reflexive relation.
Preorders are a natural generalization of partial orders which need not be antisymmetric: there may be pairs of elements such that each is "less than or equal to" the other, so that both elements have the same order-theoretic properties (in some sense, there is a "tie" among them).
If a preorder is required to be antisymmetric, that is, there is no such "tie", then one obtains a partial order. If a preorder is required to be symmetric, that is, all comparable elements are tied, then one obtains an equivalence relation.
Every preorder naturally factors into these two notions: the "tie" relation on a proset is an equivalence relation, and the quotient under that equivalence relation is a partial order. (Contributed by FL, 17-Nov-2014) (Revised by Stefan O'Rear, 31-Jan-2015)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-proset | ⊢ Proset = { 𝑓 ∣ [ ( Base ‘ 𝑓 ) / 𝑏 ] [ ( le ‘ 𝑓 ) / 𝑟 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑥 ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ) } |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cproset | ⊢ Proset | |
| 1 | vf | ⊢ 𝑓 | |
| 2 | cbs | ⊢ Base | |
| 3 | 1 | cv | ⊢ 𝑓 |
| 4 | 3 2 | cfv | ⊢ ( Base ‘ 𝑓 ) |
| 5 | vb | ⊢ 𝑏 | |
| 6 | cple | ⊢ le | |
| 7 | 3 6 | cfv | ⊢ ( le ‘ 𝑓 ) |
| 8 | vr | ⊢ 𝑟 | |
| 9 | vx | ⊢ 𝑥 | |
| 10 | 5 | cv | ⊢ 𝑏 |
| 11 | vy | ⊢ 𝑦 | |
| 12 | vz | ⊢ 𝑧 | |
| 13 | 9 | cv | ⊢ 𝑥 |
| 14 | 8 | cv | ⊢ 𝑟 |
| 15 | 13 13 14 | wbr | ⊢ 𝑥 𝑟 𝑥 |
| 16 | 11 | cv | ⊢ 𝑦 |
| 17 | 13 16 14 | wbr | ⊢ 𝑥 𝑟 𝑦 |
| 18 | 12 | cv | ⊢ 𝑧 |
| 19 | 16 18 14 | wbr | ⊢ 𝑦 𝑟 𝑧 |
| 20 | 17 19 | wa | ⊢ ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) |
| 21 | 13 18 14 | wbr | ⊢ 𝑥 𝑟 𝑧 |
| 22 | 20 21 | wi | ⊢ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) |
| 23 | 15 22 | wa | ⊢ ( 𝑥 𝑟 𝑥 ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ) |
| 24 | 23 12 10 | wral | ⊢ ∀ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑥 ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ) |
| 25 | 24 11 10 | wral | ⊢ ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑥 ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ) |
| 26 | 25 9 10 | wral | ⊢ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑥 ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ) |
| 27 | 26 8 7 | wsbc | ⊢ [ ( le ‘ 𝑓 ) / 𝑟 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑥 ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ) |
| 28 | 27 5 4 | wsbc | ⊢ [ ( Base ‘ 𝑓 ) / 𝑏 ] [ ( le ‘ 𝑓 ) / 𝑟 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑥 ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ) |
| 29 | 28 1 | cab | ⊢ { 𝑓 ∣ [ ( Base ‘ 𝑓 ) / 𝑏 ] [ ( le ‘ 𝑓 ) / 𝑟 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑥 ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ) } |
| 30 | 0 29 | wceq | ⊢ Proset = { 𝑓 ∣ [ ( Base ‘ 𝑓 ) / 𝑏 ] [ ( le ‘ 𝑓 ) / 𝑟 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑥 ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ) } |