Definition df-so 2929

Description: Define a strict complete (linear) order relation.

Assertion

Ref	Expression
df-so	|- (R Or A <-> (R Po A /\ A.x e. A A.y e. A (xRy \/ x = y \/ yRx)))

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

Detailed syntax breakdown of Definition df-so

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cR	. . 3 class R
3	1, 2	wor 2917	. 2 wff R Or A
4	1, 2	wpo 2916	. . 3 wff R Po A
5		vx	. . . . . . . 8 set x
6	5	cv 991	. . . . . . 7 class x
7		vy	. . . . . . . 8 set y
8	7	cv 991	. . . . . . 7 class y
9	6, 8, 2	wbr 2692	. . . . . 6 wff xRy
10	6, 8	wceq 992	. . . . . 6 wff x = y
11	8, 6, 2	wbr 2692	. . . . . 6 wff yRx
12	9, 10, 11	w3o 780	. . . . 5 wff (xRy \/ x = y \/ yRx)
13	12, 7, 1	wral 1691	. . . 4 wff A.y e. A (xRy \/ x = y \/ yRx)
14	13, 5, 1	wral 1691	. . 3 wff A.x e. A A.y e. A (xRy \/ x = y \/ yRx)
15	4, 14	wa 221	. 2 wff (R Po A /\ A.x e. A A.y e. A (xRy \/ x = y \/ yRx))
16	3, 15	wb 144	1 wff (R Or A <-> (R Po A /\ A.x e. A A.y e. A (xRy \/ x = y \/ yRx)))

This definition is referenced by:  sopo 2930  soss 2931  soeq1 2932  solin 2936  itlso 2942  so0 2944  dfwe2 3140  cnvso 3628  zorn2lem6 4939  zorn 4943

Copyright terms: Public domain