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 \leftrightarrow \forall x \in A \forall y \in A \forall z \in A (\neg x R x \land ((x R y \land y R z) \to 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 \neg 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 \land y R z)$
14	6 11 0	wbr	$wff x R z$
15	13 14	wi	$wff ((x R y \land y R z) \to x R z)$
16	8 15	wa	$wff (\neg x R x \land ((x R y \land y R z) \to x R z))$
17	16 5 1	wral	$wff \forall z \in A (\neg x R x \land ((x R y \land y R z) \to x R z))$
18	17 4 1	wral	$wff \forall y \in A \forall z \in A (\neg x R x \land ((x R y \land y R z) \to x R z))$
19	18 3 1	wral	$wff \forall x \in A \forall y \in A \forall z \in A (\neg x R x \land ((x R y \land y R z) \to x R z))$
20	2 19	wb	$wff (R Po A \leftrightarrow \forall x \in A \forall y \in A \forall z \in A (\neg x R x \land ((x R y \land y R z) \to x R z)))$

Metamath Proof Explorer

Definition df-po

Detailed syntax breakdown