Definition df-po 2128

Description: Define a 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 group(s):   x,y,z,R   x,A,ï,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 2058	. 2 wff R Po A
4		vx	. . . . . . . . 9 set x
5	4	cv 1089	. . . . . . . 8 class x
6	5, 5, 2	wbr 2054	. . . . . . 7 wff xRx
7	6	wn 1	. . . . . 6 wff ¬ xRx
8		vy	. . . . . . . . . 10 set y
9	8	cv 1089	. . . . . . . . 9 class y
10	5, 9, 2	wbr 2054	. . . . . . . 8 wff xRy
11		vz	. . . . . . . . . 10 set z
12	11	cv 1089	. . . . . . . . 9 class z
13	9, 12, 2	wbr 2054	. . . . . . . 8 wff yRz
14	10, 13	wa 196	. . . . . . 7 wff (xRy ∧ yRz)
15	5, 12, 2	wbr 2054	. . . . . . 7 wff xRz
16	14, 15	wi 2	. . . . . 6 wff ((xRy ∧ yRz) → xRz)
17	7, 16	wa 196	. . . . 5 wff (¬ xRx ∧ ((xRy ∧ yRz) → xRz))
18	17, 11, 1	wral 1201	. . . 4 wff ∀z ∈ A (¬ xRx ∧ ((xRy ∧ yRz) → xRz))
19	18, 8, 1	wral 1201	. . 3 wff ∀y ∈ A ∀z ∈ A (¬ xRx ∧ ((xRy ∧ yRz) → xRz))
20	19, 4, 1	wral 1201	. 2 wff ∀x ∈ A ∀y ∈ A ∀z ∈ A (¬ xRx ∧ ((xRy ∧ yRz) → xRz))
21	3, 20	wb 127	1 wff (R Po A ↔ ∀x ∈ A ∀y ∈ A ∀z ∈ A (¬ xRx ∧ ((xRy ∧ yRz) → xRz)))

This definition is referenced by:  poss 2129  poeq1 2130  pocl 2132  po0 2137  itlso 2151  dfwe2 2187  zorn2 3612

metamath.org