Definition df-so 5568

Description: Define the strict complete (linear) order predicate. The expression 𝑅 Or 𝐴 is true if relationship 𝑅 orders 𝐴. For example, < Or ℝ is true (ltso 11317). 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 5566	. 2 wff 𝑅 Or 𝐴
4	1, 2	wpo 5565	. . 3 wff 𝑅 Po 𝐴
5		vx	. . . . . . . 8 setvar 𝑥
6	5	cv 1569	. . . . . . 7 class 𝑥
7		vy	. . . . . . . 8 setvar 𝑦
8	7	cv 1569	. . . . . . 7 class 𝑦
9	6, 8, 2	wbr 5107	. . . . . 6 wff 𝑥𝑅𝑦
10	5, 7	weq 1995	. . . . . 6 wff 𝑥 = 𝑦
11	8, 6, 2	wbr 5107	. . . . . 6 wff 𝑦𝑅𝑥
12	9, 10, 11	w3o 1102	. . . . 5 wff (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)
13	12, 7, 1	wral 3078	. . . 4 wff ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)
14	13, 5, 1	wral 3078	. . 3 wff ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)
15	4, 14	wa 401	. 2 wff (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))
16	3, 15	wb 209	1 wff (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)))

This definition is used by:  nfso  5574  sopo  5586  soss  5587  soeq1  5588  solin  5594  issod  5602  so0  5605  soinxp  5741  sosn  5746  cnvso  6290  isosolem  7351  sorpss  7732  dfwe2  7776  epweon  7777  soxp  8130  soseq  8160  sornom  10282  zorn2lem6  10506  tosso  18509  dfso3  36286  dfso2  36321