Definition df-so 3764

Description: Define the strict complete (linear) order predicate.

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 3751	. 2 wff R Or A
4	1, 2	wpo 3750	. . 3 wff R Po A
5		vx	. . . . . . . 8 set x
6	5	cv 1585	. . . . . . 7 class x
7		vy	. . . . . . . 8 set y
8	7	cv 1585	. . . . . . 7 class y
9	6, 8, 2	wbr 3507	. . . . . 6 wff xRy
10	6, 8	wceq 1586	. . . . . 6 wff x = y
11	8, 6, 2	wbr 3507	. . . . . 6 wff yRx
12	9, 10, 11	w3o 1101	. . . . 5 wff (xRy \/ x = y \/ yRx)
13	12, 7, 1	wral 2355	. . . 4 wff A.y e. A (xRy \/ x = y \/ yRx)
14	13, 5, 1	wral 2355	. . 3 wff A.x e. A A.y e. A (xRy \/ x = y \/ yRx)
15	4, 14	wa 337	. 2 wff (R Po A /\ A.x e. A A.y e. A (xRy \/ x = y \/ yRx))
16	3, 15	wb 219	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 3765  soss 3766  soeq1 3767  solin 3771  itlso 3777  so0 3779  dfwe2 4007  cnvso 4532  soxp 5213  zorn2lem6 6366  zorn 6370  dfso2 14464  soxpOLD 14603  soseq 14608

Copyright terms: Public domain