Definition df-so 2856

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 2845	. 2 wff R Or A
4	1, 2	wpo 2844	. . 3 wff R Po A
5		vx	. . . . . . . 8 set x
6	5	cv 957	. . . . . . 7 class x
7		vy	. . . . . . . 8 set y
8	7	cv 957	. . . . . . 7 class y
9	6, 8, 2	wbr 2624	. . . . . 6 wff xRy
10	6, 8	wceq 958	. . . . . 6 wff x = y
11	8, 6, 2	wbr 2624	. . . . . 6 wff yRx
12	9, 10, 11	w3o 776	. . . . 5 wff (xRy \/ x = y \/ yRx)
13	12, 7, 1	wral 1648	. . . 4 wff A.y e. A (xRy \/ x = y \/ yRx)
14	13, 5, 1	wral 1648	. . 3 wff A.x e. A A.y e. A (xRy \/ x = y \/ yRx)
15	4, 14	wa 223	. 2 wff (R Po A /\ A.x e. A A.y e. A (xRy \/ x = y \/ yRx))
16	3, 15	wb 146	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 2857  soss 2858  soeq1 2859  solin 2863  itlso 2869  so0 2871  dfwe2 2941  cnvso 3529  zorn2lem6 4803  zorn 4807

Copyright terms: Public domain