Metamath Proof Explorer

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 ⊢ R Po A ↔ ∀ x ∈ A ∀ y ∈ A ∀ z ∈ A ¬ x R x ∧ x R y ∧ y R z → x R z

Detailed syntax breakdown

Step Hyp Ref Expression
0 cR class R
1 cA class A
2 1 0 wpo wff R Po A
3 vx setvar x
4 vy setvar y
5 vz setvar z
6 3 cv setvar x
7 6 6 0 wbr wff x R x
8 7 wn wff ¬ x R x
9 4 cv setvar y
10 6 9 0 wbr wff x R y
11 5 cv setvar z
12 9 11 0 wbr wff y R z
13 10 12 wa wff x R y ∧ y R z
14 6 11 0 wbr wff x R z
15 13 14 wi wff x R y ∧ y R z → x R z
16 8 15 wa wff ¬ x R x ∧ x R y ∧ y R z → x R z
17 16 5 1 wral wff ∀ z ∈ A ¬ x R x ∧ x R y ∧ y R z → x R z
18 17 4 1 wral wff ∀ y ∈ A ∀ z ∈ A ¬ x R x ∧ x R y ∧ y R z → x R z
19 18 3 1 wral wff ∀ x ∈ A ∀ y ∈ A ∀ z ∈ A ¬ x R x ∧ x R y ∧ y R z → x R z
20 2 19 wb wff R Po A ↔ ∀ x ∈ A ∀ y ∈ A ∀ z ∈ A ¬ x R x ∧ x R y ∧ y R z → x R z