Definition df-so 2841

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 2830	. 2 wff R Or A
4	1, 2	wpo 2829	. . 3 wff R Po A
5		vx	. . . . . . . 8 set x
6	5	cv 952	. . . . . . 7 class x
7		vy	. . . . . . . 8 set y
8	7	cv 952	. . . . . . 7 class y
9	6, 8, 2	wbr 2609	. . . . . 6 wff xRy
10	6, 8	wceq 953	. . . . . 6 wff x = y
11	8, 6, 2	wbr 2609	. . . . . 6 wff yRx
12	9, 10, 11	w3o 772	. . . . 5 wff (xRy \/ x = y \/ yRx)
13	12, 7, 1	wral 1637	. . . 4 wff A.y e. A (xRy \/ x = y \/ yRx)
14	13, 5, 1	wral 1637	. . 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 2842  soss 2843  soeq1 2844  solin 2848  itlso 2854  so0 2856  dfwe2 2925  cnvso 3509  zorn2lem6 4765  zorn 4769

Copyright terms: Public domain