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 5006
Description: Define the strict complete (linear) order predicate. The expression 𝑅 Or 𝐴 is true if relationship 𝑅 orders 𝐴. For example, < Or ℝ is true (ltso 10078). 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 5004 . 2 wff 𝑅 Or 𝐴
41, 2wpo 5003 . . 3 wff 𝑅 Po 𝐴
5 vx . . . . . . . 8 setvar 𝑥
65cv 1479 . . . . . . 7 class 𝑥
7 vy . . . . . . . 8 setvar 𝑦
87cv 1479 . . . . . . 7 class 𝑦
96, 8, 2wbr 4623 . . . . . 6 wff 𝑥𝑅𝑦
105, 7weq 1871 . . . . . 6 wff 𝑥 = 𝑦
118, 6, 2wbr 4623 . . . . . 6 wff 𝑦𝑅𝑥
129, 10, 11w3o 1035 . . . . 5 wff (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)
1312, 7, 1wral 2908 . . . 4 wff 𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)
1413, 5, 1wral 2908 . . 3 wff 𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)
154, 14wa 384 . 2 wff (𝑅 Po 𝐴 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥))
163, 15wb 196 1 wff (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)))
Colors of variables: wff setvar class
This definition is referenced by:  nfso  5011  sopo  5022  soss  5023  soeq1  5024  solin  5028  issod  5035  so0  5038  soinxp  5154  sosn  5159  cnvso  5643  isosolem  6562  sorpss  6907  dfwe2  6943  soxp  7250  sornom  9059  zorn2lem6  9283  tosso  16976  dfso3  31363  dfso2  31405  soseq  31505
  Copyright terms: Public domain W3C validator