Definition df-po 5560

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

This definition is referenced by:  poss  5562  poeq1  5563  nfpo  5566  pocl  5568  ispod  5569  po0  5577  poinxp  5733  posn  5738  cnvpo  6278  dfpo2  6287  isopolem  7333  porpss  7714  dfwe2  7761  epweon  7762  poxp  8112  poseq  8142  dfso3  36083  elpotr  36142  weiunpo  36838