Definition df-po 2918

Description: Define a strict partial order relation. Definition of [Enderton] p. 168.

Assertion

Ref	Expression
df-po	⊢ (R Po A ↔ ∀x ∈ A ∀y ∈ A ∀z ∈ A (¬ xRx ⋀ ((xRy ⋀ yRz) → xRz)))

Distinct variable groups:   x,y,z,R   x,A,y,z

Detailed syntax breakdown of Definition df-po

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cR	. . 3 class R
3	1, 2	wpo 2916	. 2 wff R Po A
4		vx	. . . . . . . . 9 set x
5	4	cv 991	. . . . . . . 8 class x
6	5, 5, 2	wbr 2692	. . . . . . 7 wff xRx
7	6	wn 2	. . . . . 6 wff ¬ xRx
8		vy	. . . . . . . . . 10 set y
9	8	cv 991	. . . . . . . . 9 class y
10	5, 9, 2	wbr 2692	. . . . . . . 8 wff xRy
11		vz	. . . . . . . . . 10 set z
12	11	cv 991	. . . . . . . . 9 class z
13	9, 12, 2	wbr 2692	. . . . . . . 8 wff yRz
14	10, 13	wa 221	. . . . . . 7 wff (xRy ⋀ yRz)
15	5, 12, 2	wbr 2692	. . . . . . 7 wff xRz
16	14, 15	wi 3	. . . . . 6 wff ((xRy ⋀ yRz) → xRz)
17	7, 16	wa 221	. . . . 5 wff (¬ xRx ⋀ ((xRy ⋀ yRz) → xRz))
18	17, 11, 1	wral 1691	. . . 4 wff ∀z ∈ A (¬ xRx ⋀ ((xRy ⋀ yRz) → xRz))
19	18, 8, 1	wral 1691	. . 3 wff ∀y ∈ A ∀z ∈ A (¬ xRx ⋀ ((xRy ⋀ yRz) → xRz))
20	19, 4, 1	wral 1691	. 2 wff ∀x ∈ A ∀y ∈ A ∀z ∈ A (¬ xRx ⋀ ((xRy ⋀ yRz) → xRz))
21	3, 20	wb 144	1 wff (R Po A ↔ ∀x ∈ A ∀y ∈ A ∀z ∈ A (¬ xRx ⋀ ((xRy ⋀ yRz) → xRz)))

This definition is referenced by:  poss 2919  poeq1 2920  pocl 2922  po0 2927  posn 2928  itlso 2942  dfwe2 3140  cnvpo 3627  zorn 4943

Copyright terms: Public domain