Definition df-so 5180

Description: Define the strict complete (linear) order predicate. The expression 𝑅 Or 𝐴 is true if relationship 𝑅 orders 𝐴. For example, < Or ℝ is true (ltso 10302). Equivalent to Definition 6.19(1) of [TakeutiZaring] p. 29. (Contributed by NM, 21-Jan-1996.)

Assertion

Ref	Expression
df-so	⊢ (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)))

Distinct variable groups:   𝑥,𝑦,𝑅   𝑥,𝐴,𝑦

Detailed syntax breakdown of Definition df-so

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cR	. . 3 class 𝑅
3	1, 2	wor 5178	. 2 wff 𝑅 Or 𝐴
4	1, 2	wpo 5177	. . 3 wff 𝑅 Po 𝐴
5		vx	. . . . . . . 8 setvar 𝑥
6	5	cv 1623	. . . . . . 7 class 𝑥
7		vy	. . . . . . . 8 setvar 𝑦
8	7	cv 1623	. . . . . . 7 class 𝑦
9	6, 8, 2	wbr 4796	. . . . . 6 wff 𝑥𝑅𝑦
10	5, 7	weq 2032	. . . . . 6 wff 𝑥 = 𝑦
11	8, 6, 2	wbr 4796	. . . . . 6 wff 𝑦𝑅𝑥
12	9, 10, 11	w3o 1071	. . . . 5 wff (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)
13	12, 7, 1	wral 3042	. . . 4 wff ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)
14	13, 5, 1	wral 3042	. . 3 wff ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)
15	4, 14	wa 383	. 2 wff (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))
16	3, 15	wb 196	1 wff (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)))

This definition is referenced by:  nfso  5185  sopo  5196  soss  5197  soeq1  5198  solin  5202  issod  5209  so0  5212  soinxp  5332  sosn  5337  cnvso  5827  isosolem  6752  sorpss  7099  dfwe2  7138  soxp  7450  sornom  9283  zorn2lem6  9507  tosso  17229  dfso3  31900  dfso2  31943  soseq  32052