Definition df-po 5561

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

This definition is referenced by:  poss  5563  poeq1  5564  nfpo  5567  pocl  5569  ispod  5570  po0  5578  poinxp  5735  posn  5740  cnvpo  6276  dfpo2  6285  isopolem  7337  porpss  7719  dfwe2  7766  epweon  7767  poxp  8125  poseq  8155  dfso3  35683  elpotr  35745  weiunpo  36429