Definition df-poset 18040

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 𝑓 is denoted by (Base‘𝑓) and its partial order by (le‘𝑓) (for "less than or equal to"). The quantifiers ∃𝑏∃𝑟 provide a notational shorthand to allow us to refer to the base and ordering relation as 𝑏 and 𝑟 in the definition rather than having to repeat (Base‘𝑓) and (le‘𝑓) throughout. These quantifiers can be eliminated with ceqsex2v 3484 and related theorems. (Contributed by NM, 18-Oct-2012.)

Assertion

Ref	Expression
df-poset	⊢ Poset = {𝑓 ∣ ∃𝑏∃𝑟(𝑏 = (Base‘𝑓) ∧ 𝑟 = (le‘𝑓) ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑥) → 𝑥 = 𝑦) ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧) → 𝑥𝑟𝑧)))}

Distinct variable group:   𝑓,𝑏,𝑟,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-poset

Step	Hyp	Ref	Expression
1		cpo 18034	. 2 class Poset
2		vb	. . . . . . . 8 setvar 𝑏
3	2	cv 1538	. . . . . . 7 class 𝑏
4		vf	. . . . . . . . 9 setvar 𝑓
5	4	cv 1538	. . . . . . . 8 class 𝑓
6		cbs 16921	. . . . . . . 8 class Base
7	5, 6	cfv 6437	. . . . . . 7 class (Base‘𝑓)
8	3, 7	wceq 1539	. . . . . 6 wff 𝑏 = (Base‘𝑓)
9		vr	. . . . . . . 8 setvar 𝑟
10	9	cv 1538	. . . . . . 7 class 𝑟
11		cple 16978	. . . . . . . 8 class le
12	5, 11	cfv 6437	. . . . . . 7 class (le‘𝑓)
13	10, 12	wceq 1539	. . . . . 6 wff 𝑟 = (le‘𝑓)
14		vx	. . . . . . . . . . . 12 setvar 𝑥
15	14	cv 1538	. . . . . . . . . . 11 class 𝑥
16	15, 15, 10	wbr 5075	. . . . . . . . . 10 wff 𝑥𝑟𝑥
17		vy	. . . . . . . . . . . . . 14 setvar 𝑦
18	17	cv 1538	. . . . . . . . . . . . 13 class 𝑦
19	15, 18, 10	wbr 5075	. . . . . . . . . . . 12 wff 𝑥𝑟𝑦
20	18, 15, 10	wbr 5075	. . . . . . . . . . . 12 wff 𝑦𝑟𝑥
21	19, 20	wa 396	. . . . . . . . . . 11 wff (𝑥𝑟𝑦 ∧ 𝑦𝑟𝑥)
22	14, 17	weq 1967	. . . . . . . . . . 11 wff 𝑥 = 𝑦
23	21, 22	wi 4	. . . . . . . . . 10 wff ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑥) → 𝑥 = 𝑦)
24		vz	. . . . . . . . . . . . . 14 setvar 𝑧
25	24	cv 1538	. . . . . . . . . . . . 13 class 𝑧
26	18, 25, 10	wbr 5075	. . . . . . . . . . . 12 wff 𝑦𝑟𝑧
27	19, 26	wa 396	. . . . . . . . . . 11 wff (𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧)
28	15, 25, 10	wbr 5075	. . . . . . . . . . 11 wff 𝑥𝑟𝑧
29	27, 28	wi 4	. . . . . . . . . 10 wff ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧) → 𝑥𝑟𝑧)
30	16, 23, 29	w3a 1086	. . . . . . . . 9 wff (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑥) → 𝑥 = 𝑦) ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧) → 𝑥𝑟𝑧))
31	30, 24, 3	wral 3065	. . . . . . . 8 wff ∀𝑧 ∈ 𝑏 (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑥) → 𝑥 = 𝑦) ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧) → 𝑥𝑟𝑧))
32	31, 17, 3	wral 3065	. . . . . . 7 wff ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑥) → 𝑥 = 𝑦) ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧) → 𝑥𝑟𝑧))
33	32, 14, 3	wral 3065	. . . . . 6 wff ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑥) → 𝑥 = 𝑦) ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧) → 𝑥𝑟𝑧))
34	8, 13, 33	w3a 1086	. . . . 5 wff (𝑏 = (Base‘𝑓) ∧ 𝑟 = (le‘𝑓) ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑥) → 𝑥 = 𝑦) ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧) → 𝑥𝑟𝑧)))
35	34, 9	wex 1782	. . . 4 wff ∃𝑟(𝑏 = (Base‘𝑓) ∧ 𝑟 = (le‘𝑓) ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑥) → 𝑥 = 𝑦) ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧) → 𝑥𝑟𝑧)))
36	35, 2	wex 1782	. . 3 wff ∃𝑏∃𝑟(𝑏 = (Base‘𝑓) ∧ 𝑟 = (le‘𝑓) ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑥) → 𝑥 = 𝑦) ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧) → 𝑥𝑟𝑧)))
37	36, 4	cab 2716	. 2 class {𝑓 ∣ ∃𝑏∃𝑟(𝑏 = (Base‘𝑓) ∧ 𝑟 = (le‘𝑓) ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑥) → 𝑥 = 𝑦) ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧) → 𝑥𝑟𝑧)))}
38	1, 37	wceq 1539	1 wff Poset = {𝑓 ∣ ∃𝑏∃𝑟(𝑏 = (Base‘𝑓) ∧ 𝑟 = (le‘𝑓) ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑥) → 𝑥 = 𝑦) ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧) → 𝑥𝑟𝑧)))}

This definition is referenced by:  ispos  18041