MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-so Structured version   Visualization version   GIF version

Definition df-so 5593
Description: Define the strict complete (linear) order predicate. The expression 𝑅 Or 𝐴 is true if relationship 𝑅 orders 𝐴. For example, < Or ℝ is true (ltso 11341). 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
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cR . . 3 class 𝑅
31, 2wor 5591 . 2 wff 𝑅 Or 𝐴
41, 2wpo 5590 . . 3 wff 𝑅 Po 𝐴
5 vx . . . . . . . 8 setvar 𝑥
65cv 1539 . . . . . . 7 class 𝑥
7 vy . . . . . . . 8 setvar 𝑦
87cv 1539 . . . . . . 7 class 𝑦
96, 8, 2wbr 5143 . . . . . 6 wff 𝑥𝑅𝑦
105, 7weq 1962 . . . . . 6 wff 𝑥 = 𝑦
118, 6, 2wbr 5143 . . . . . 6 wff 𝑦𝑅𝑥
129, 10, 11w3o 1086 . . . . 5 wff (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)
1312, 7, 1wral 3061 . . . 4 wff 𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)
1413, 5, 1wral 3061 . . 3 wff 𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)
154, 14wa 395 . 2 wff (𝑅 Po 𝐴 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥))
163, 15wb 206 1 wff (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)))
Colors of variables: wff setvar class
This definition is referenced by:  nfso  5599  sopo  5611  soss  5612  soeq1  5613  solin  5619  issod  5627  so0  5630  soinxp  5767  sosn  5772  cnvso  6308  isosolem  7367  sorpss  7748  dfwe2  7794  epweon  7795  soxp  8154  soseq  8184  sornom  10317  zorn2lem6  10541  tosso  18464  dfso3  35720  dfso2  35755
  Copyright terms: Public domain W3C validator