Definition df-po 5596

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

This definition is referenced by:  poss  5598  poeq1  5599  nfpo  5602  pocl  5604  ispod  5605  po0  5613  poinxp  5768  posn  5773  cnvpo  6308  dfpo2  6317  isopolem  7364  porpss  7745  dfwe2  7792  epweon  7793  poxp  8151  poseq  8181  dfso3  35699  elpotr  35762  weiunpo  36447