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 5597
Description: Define the strict complete (linear) order predicate. The expression 𝑅 Or 𝐴 is true if relationship 𝑅 orders 𝐴. For example, < Or ℝ is true (ltso 11338). 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 5595 . 2 wff 𝑅 Or 𝐴
41, 2wpo 5594 . . 3 wff 𝑅 Po 𝐴
5 vx . . . . . . . 8 setvar 𝑥
65cv 1535 . . . . . . 7 class 𝑥
7 vy . . . . . . . 8 setvar 𝑦
87cv 1535 . . . . . . 7 class 𝑦
96, 8, 2wbr 5147 . . . . . 6 wff 𝑥𝑅𝑦
105, 7weq 1959 . . . . . 6 wff 𝑥 = 𝑦
118, 6, 2wbr 5147 . . . . . 6 wff 𝑦𝑅𝑥
129, 10, 11w3o 1085 . . . . 5 wff (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)
1312, 7, 1wral 3058 . . . 4 wff 𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)
1413, 5, 1wral 3058 . . 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  5603  sopo  5615  soss  5616  soeq1  5617  solin  5622  issod  5630  so0  5633  soinxp  5769  sosn  5774  cnvso  6309  isosolem  7366  sorpss  7746  dfwe2  7792  epweon  7793  soxp  8152  soseq  8182  sornom  10314  zorn2lem6  10538  tosso  18476  dfso3  35699  dfso2  35734
  Copyright terms: Public domain W3C validator