Definition df-so 5564

Description: Define the strict complete (linear) order predicate. The expression 𝑅 Or 𝐴 is true if relationship 𝑅 orders 𝐴. For example, < Or ℝ is true (ltso 11414). 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 5562	. 2 wff 𝑅 Or 𝐴
4	1, 2	wpo 5561	. . 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 5106	. . . . . 6 wff 𝑥𝑅𝑦
10	5, 7	weq 1997	. . . . . 6 wff 𝑥 = 𝑦
11	8, 6, 2	wbr 5106	. . . . . 6 wff 𝑦𝑅𝑥
12	9, 10, 11	w3o 1102	. . . . 5 wff (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)
13	12, 7, 1	wral 3080	. . . 4 wff ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)
14	13, 5, 1	wral 3080	. . 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  5570  sopo  5582  soss  5583  soeq1  5584  solin  5590  issod  5598  so0  5601  soinxp  5738  sosn  5743  cnvso  6306  isosolem  7375  sorpss  7765  dfwe2  7809  epweon  7810  soxp  8165  soseq  8200  sornom  10379  zorn2lem6  10603  tosso  18617  dfso3  36662  dfso2  36697