Definition df-po 2831

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

Assertion

Ref	Expression
df-po	|- (R Po A <-> A.x e. A A.y e. A A.z e. 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 2829	. 2 wff R Po A
4		vx	. . . . . . . . 9 set x
5	4	cv 952	. . . . . . . 8 class x
6	5, 5, 2	wbr 2609	. . . . . . 7 wff xRx
7	6	wn 2	. . . . . 6 wff -. xRx
8		vy	. . . . . . . . . 10 set y
9	8	cv 952	. . . . . . . . 9 class y
10	5, 9, 2	wbr 2609	. . . . . . . 8 wff xRy
11		vz	. . . . . . . . . 10 set z
12	11	cv 952	. . . . . . . . 9 class z
13	9, 12, 2	wbr 2609	. . . . . . . 8 wff yRz
14	10, 13	wa 223	. . . . . . 7 wff (xRy /\ yRz)
15	5, 12, 2	wbr 2609	. . . . . . 7 wff xRz
16	14, 15	wi 3	. . . . . 6 wff ((xRy /\ yRz) -> xRz)
17	7, 16	wa 223	. . . . 5 wff (-. xRx /\ ((xRy /\ yRz) -> xRz))
18	17, 11, 1	wral 1637	. . . 4 wff A.z e. A (-. xRx /\ ((xRy /\ yRz) -> xRz))
19	18, 8, 1	wral 1637	. . 3 wff A.y e. A A.z e. A (-. xRx /\ ((xRy /\ yRz) -> xRz))
20	19, 4, 1	wral 1637	. 2 wff A.x e. A A.y e. A A.z e. A (-. xRx /\ ((xRy /\ yRz) -> xRz))
21	3, 20	wb 146	1 wff (R Po A <-> A.x e. A A.y e. A A.z e. A (-. xRx /\ ((xRy /\ yRz) -> xRz)))

This definition is referenced by:  poss 2832  poeq1 2833  pocl 2835  po0 2840  itlso 2854  dfwe2 2925  cnvpo 3508  zorn 4769

Copyright terms: Public domain