Definition df-po 5558

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 31041). (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 5556	. 2 wff 𝑅 Po 𝐴
4		vx	. . . . . . . . 9 setvar 𝑥
5	4	cv 1568	. . . . . . . 8 class 𝑥
6	5, 5, 2	wbr 5102	. . . . . . 7 wff 𝑥𝑅𝑥
7	6	wn 3	. . . . . 6 wff ¬ 𝑥𝑅𝑥
8		vy	. . . . . . . . . 10 setvar 𝑦
9	8	cv 1568	. . . . . . . . 9 class 𝑦
10	5, 9, 2	wbr 5102	. . . . . . . 8 wff 𝑥𝑅𝑦
11		vz	. . . . . . . . . 10 setvar 𝑧
12	11	cv 1568	. . . . . . . . 9 class 𝑧
13	9, 12, 2	wbr 5102	. . . . . . . 8 wff 𝑦𝑅𝑧
14	10, 13	wa 401	. . . . . . 7 wff (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)
15	5, 12, 2	wbr 5102	. . . . . . 7 wff 𝑥𝑅𝑧
16	14, 15	wi 4	. . . . . 6 wff ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)
17	7, 16	wa 401	. . . . 5 wff (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))
18	17, 11, 1	wral 3076	. . . 4 wff ∀𝑧 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))
19	18, 8, 1	wral 3076	. . 3 wff ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))
20	19, 4, 1	wral 3076	. 2 wff ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))
21	3, 20	wb 209	1 wff (𝑅 Po 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)))

This definition is used by:  poss  5560  poeq1  5561  nfpo  5564  pocl  5566  ispod  5567  po0  5575  poinxp  5731  posn  5736  cnvpo  6290  dfpo2  6299  isopolem  7353  porpss  7743  dfwe2  7788  epweon  7789  poxp  8142  poseq  8177  dfso3  36577  elpotr  36635  weiunpo  37345