Definition df-po 5232

Description: Define the strict partial order predicate. Definition of [Enderton] p. 168. The expression 𝑅 Po 𝐴 means 𝑅 is a partial order on 𝐴. For example, < Po ℝ is true, while ≤ Po ℝ is false (ex-po 27619). (Contributed by NM, 16-Mar-1997.)

Assertion

Ref	Expression
df-po	⊢ (𝑅 Po 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)))

Distinct variable groups:   𝑥,𝑦,𝑧,𝑅   𝑥,𝐴,𝑦,𝑧

Detailed syntax breakdown of Definition df-po

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cR	. . 3 class 𝑅
3	1, 2	wpo 5230	. 2 wff 𝑅 Po 𝐴
4		vx	. . . . . . . . 9 setvar 𝑥
5	4	cv 1636	. . . . . . . 8 class 𝑥
6	5, 5, 2	wbr 4844	. . . . . . 7 wff 𝑥𝑅𝑥
7	6	wn 3	. . . . . 6 wff ¬ 𝑥𝑅𝑥
8		vy	. . . . . . . . . 10 setvar 𝑦
9	8	cv 1636	. . . . . . . . 9 class 𝑦
10	5, 9, 2	wbr 4844	. . . . . . . 8 wff 𝑥𝑅𝑦
11		vz	. . . . . . . . . 10 setvar 𝑧
12	11	cv 1636	. . . . . . . . 9 class 𝑧
13	9, 12, 2	wbr 4844	. . . . . . . 8 wff 𝑦𝑅𝑧
14	10, 13	wa 384	. . . . . . 7 wff (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)
15	5, 12, 2	wbr 4844	. . . . . . 7 wff 𝑥𝑅𝑧
16	14, 15	wi 4	. . . . . 6 wff ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)
17	7, 16	wa 384	. . . . 5 wff (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))
18	17, 11, 1	wral 3096	. . . 4 wff ∀𝑧 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))
19	18, 8, 1	wral 3096	. . 3 wff ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))
20	19, 4, 1	wral 3096	. 2 wff ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))
21	3, 20	wb 197	1 wff (𝑅 Po 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)))

This definition is referenced by:  poss  5234  poeq1  5235  nfpo  5237  pocl  5239  ispod  5240  po0  5247  poinxp  5384  posn  5389  cnvpo  5887  isopolem  6815  porpss  7167  dfwe2  7207  poxp  7519  dfso3  31918  dfpo2  31962  elpotr  32001  poseq  32069