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 5233
Description: Define the strict complete (linear) order predicate. The expression 𝑅 Or 𝐴 is true if relationship 𝑅 orders 𝐴. For example, < Or ℝ is true (ltso 10399). 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 5231 . 2 wff 𝑅 Or 𝐴
41, 2wpo 5230 . . 3 wff 𝑅 Po 𝐴
5 vx . . . . . . . 8 setvar 𝑥
65cv 1636 . . . . . . 7 class 𝑥
7 vy . . . . . . . 8 setvar 𝑦
87cv 1636 . . . . . . 7 class 𝑦
96, 8, 2wbr 4844 . . . . . 6 wff 𝑥𝑅𝑦
105, 7weq 2054 . . . . . 6 wff 𝑥 = 𝑦
118, 6, 2wbr 4844 . . . . . 6 wff 𝑦𝑅𝑥
129, 10, 11w3o 1099 . . . . 5 wff (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)
1312, 7, 1wral 3096 . . . 4 wff 𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)
1413, 5, 1wral 3096 . . 3 wff 𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)
154, 14wa 384 . 2 wff (𝑅 Po 𝐴 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥))
163, 15wb 197 1 wff (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)))
Colors of variables: wff setvar class
This definition is referenced by:  nfso  5238  sopo  5249  soss  5250  soeq1  5251  solin  5255  issod  5262  so0  5265  soinxp  5385  sosn  5390  cnvso  5888  isosolem  6817  sorpss  7168  dfwe2  7207  soxp  7520  sornom  9380  zorn2lem6  9604  tosso  17237  dfso3  31918  dfso2  31961  soseq  32070
  Copyright terms: Public domain W3C validator