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 4949
Description: Define the strict complete (linear) order predicate. The expression 𝑅 Or 𝐴 is true if relationship 𝑅 orders 𝐴. For example, < Or ℝ is true (ltso 9969). 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 4947 . 2 wff 𝑅 Or 𝐴
41, 2wpo 4946 . . 3 wff 𝑅 Po 𝐴
5 vx . . . . . . . 8 setvar 𝑥
65cv 1473 . . . . . . 7 class 𝑥
7 vy . . . . . . . 8 setvar 𝑦
87cv 1473 . . . . . . 7 class 𝑦
96, 8, 2wbr 4577 . . . . . 6 wff 𝑥𝑅𝑦
105, 7weq 1860 . . . . . 6 wff 𝑥 = 𝑦
118, 6, 2wbr 4577 . . . . . 6 wff 𝑦𝑅𝑥
129, 10, 11w3o 1029 . . . . 5 wff (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)
1312, 7, 1wral 2895 . . . 4 wff 𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)
1413, 5, 1wral 2895 . . 3 wff 𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)
154, 14wa 382 . 2 wff (𝑅 Po 𝐴 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥))
163, 15wb 194 1 wff (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)))
Colors of variables: wff setvar class
This definition is referenced by:  nfso  4954  sopo  4965  soss  4966  soeq1  4967  solin  4971  issod  4978  so0  4981  soinxp  5095  sosn  5100  cnvso  5576  isosolem  6474  sorpss  6817  dfwe2  6850  soxp  7154  sornom  8959  zorn2lem6  9183  tosso  16807  dfso3  30649  dfso2  30690  soseq  30788
  Copyright terms: Public domain W3C validator