Definition df-so 2138

Description: Define a strict or linear order relation.

Assertion

Ref	Expression
df-so	⊢ (R Or A ↔ (R Po A ∧ ∀x ∈ A ∀y ∈ A (xRy ∨ x = y ∨ yRx)))

Distinct variable group(s):   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 2059	. 2 wff R Or A
4	1, 2	wpo 2058	. . 3 wff R Po A
5		vx	. . . . . . . 8 set x
6	5	cv 1089	. . . . . . 7 class x
7		vy	. . . . . . . 8 set y
8	7	cv 1089	. . . . . . 7 class y
9	6, 8, 2	wbr 2054	. . . . . 6 wff xRy
10	5, 7	weq 797	. . . . . 6 wff x = y
11	8, 6, 2	wbr 2054	. . . . . 6 wff yRx
12	9, 10, 11	w3o 580	. . . . 5 wff (xRy ∨ x = y ∨ yRx)
13	12, 7, 1	wral 1201	. . . 4 wff ∀y ∈ A (xRy ∨ x = y ∨ yRx)
14	13, 5, 1	wral 1201	. . 3 wff ∀x ∈ A ∀y ∈ A (xRy ∨ x = y ∨ yRx)
15	4, 14	wa 196	. 2 wff (R Po A ∧ ∀x ∈ A ∀y ∈ A (xRy ∨ x = y ∨ yRx))
16	3, 15	wb 127	1 wff (R Or A ↔ (R Po A ∧ ∀x ∈ A ∀y ∈ A (xRy ∨ x = y ∨ yRx)))

This definition is referenced by:  sopo 2139  soss 2140  soeq1 2141  solin 2145  itlso 2151  so0 2153  dfwe2 2187  zornlem6 3608  zorn2 3612

metamath.org