Definition df-so 5556

Description: Define the strict complete (linear) order predicate. The expression 𝑅 Or 𝐴 is true if relationship 𝑅 orders 𝐴. For example, < Or ℝ is true (ltso 11361). 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 5554	. 2 wff 𝑅 Or 𝐴
4	1, 2	wpo 5553	. . 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 5102	. . . . . 6 wff 𝑥𝑅𝑦
10	5, 7	weq 1995	. . . . . 6 wff 𝑥 = 𝑦
11	8, 6, 2	wbr 5102	. . . . . 6 wff 𝑦𝑅𝑥
12	9, 10, 11	w3o 1102	. . . . 5 wff (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)
13	12, 7, 1	wral 3076	. . . 4 wff ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)
14	13, 5, 1	wral 3076	. . 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  5562  sopo  5574  soss  5575  soeq1  5576  solin  5582  issod  5590  so0  5593  soinxp  5729  sosn  5734  cnvso  6280  isosolem  7343  sorpss  7727  dfwe2  7771  epweon  7772  soxp  8124  soseq  8154  sornom  10326  zorn2lem6  10550  tosso  18552  dfso3  36406  dfso2  36441