Definition df-so 3604

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 3590	. 2 wff R Or A
4	1, 2	wpo 3589	. . 3 wff R Po A
5		vx	. . . . . . . 8 set x
6	5	cv 1297	. . . . . . 7 class x
7		vy	. . . . . . . 8 set y
8	7	cv 1297	. . . . . . 7 class y
9	6, 8, 2	wbr 3338	. . . . . 6 wff xRy
10	6, 8	wceq 1298	. . . . . 6 wff x = y
11	8, 6, 2	wbr 3338	. . . . . 6 wff yRx
12	9, 10, 11	w3o 857	. . . . 5 wff (xRy \/ x = y \/ yRx)
13	12, 7, 1	wral 2105	. . . 4 wff A.y e. A (xRy \/ x = y \/ yRx)
14	13, 5, 1	wral 2105	. . 3 wff A.x e. A A.y e. A (xRy \/ x = y \/ yRx)
15	4, 14	wa 240	. 2 wff (R Po A /\ A.x e. A A.y e. A (xRy \/ x = y \/ yRx))
16	3, 15	wb 163	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 3605  soss 3606  sossOLD 3607  soeq1 3608  solin 3612  itlso 3619  so0 3621  so0OLD 3622  dfwe2 3861  dfwe2OLD 3862  cnvso 4428  zorn2lem6 5955  zorn 5959  soxp 13950  soseq 13955

Copyright terms: Public domain