Definition df-so 5534

Description: Define the strict complete (linear) order predicate. The expression 𝑅 Or 𝐴 is true if relationship 𝑅 orders 𝐴. For example, < Or ℝ is true (ltso 11217). 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 5532	. 2 wff 𝑅 Or 𝐴
4	1, 2	wpo 5531	. . 3 wff 𝑅 Po 𝐴
5		vx	. . . . . . . 8 setvar 𝑥
6	5	cv 1541	. . . . . . 7 class 𝑥
7		vy	. . . . . . . 8 setvar 𝑦
8	7	cv 1541	. . . . . . 7 class 𝑦
9	6, 8, 2	wbr 5099	. . . . . 6 wff 𝑥𝑅𝑦
10	5, 7	weq 1964	. . . . . 6 wff 𝑥 = 𝑦
11	8, 6, 2	wbr 5099	. . . . . 6 wff 𝑦𝑅𝑥
12	9, 10, 11	w3o 1086	. . . . 5 wff (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)
13	12, 7, 1	wral 3052	. . . 4 wff ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)
14	13, 5, 1	wral 3052	. . 3 wff ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)
15	4, 14	wa 395	. 2 wff (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))
16	3, 15	wb 206	1 wff (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)))

This definition is referenced by:  nfso  5540  sopo  5552  soss  5553  soeq1  5554  solin  5560  issod  5568  so0  5571  soinxp  5707  sosn  5712  cnvso  6247  isosolem  7295  sorpss  7675  dfwe2  7721  epweon  7722  soxp  8073  soseq  8103  sornom  10191  zorn2lem6  10415  tosso  18344  dfso3  35916  dfso2  35951