Definition df-po

Description: Define the strict partial order predicate. Definition of Enderton p. 168. The expression R Po A means R is a partial order on A . For example, < Po RR is true, while <_ Po RR is false ( ex-po ). (Contributed by NM, 16-Mar-1997)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cR	⊢ 𝑅
1		cA	⊢ 𝐴
2	1 0	wpo	⊢ 𝑅 Po 𝐴
3		vx	⊢ 𝑥
4		vy	⊢ 𝑦
5		vz	⊢ 𝑧
6	3	cv	⊢ 𝑥
7	6 6 0	wbr	⊢ 𝑥 𝑅 𝑥
8	7	wn	⊢ ¬ 𝑥 𝑅 𝑥
9	4	cv	⊢ 𝑦
10	6 9 0	wbr	⊢ 𝑥 𝑅 𝑦
11	5	cv	⊢ 𝑧
12	9 11 0	wbr	⊢ 𝑦 𝑅 𝑧
13	10 12	wa	⊢ ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 )
14	6 11 0	wbr	⊢ 𝑥 𝑅 𝑧
15	13 14	wi	⊢ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 )
16	8 15	wa	⊢ ( ¬ 𝑥 𝑅 𝑥 ∧ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) )
17	16 5 1	wral	⊢ ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑥 𝑅 𝑥 ∧ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) )
18	17 4 1	wral	⊢ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑥 𝑅 𝑥 ∧ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) )
19	18 3 1	wral	⊢ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑥 𝑅 𝑥 ∧ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) )
20	2 19	wb	⊢ ( 𝑅 Po 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑥 𝑅 𝑥 ∧ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) )