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

Theorem sopo 5204
Description: A strict linear order is a strict partial order. (Contributed by NM, 28-Mar-1997.)
Assertion
Ref Expression
sopo (𝑅 Or 𝐴𝑅 Po 𝐴)

Proof of Theorem sopo
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-so 5188 . 2 (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)))
21simplbi 478 1 (𝑅 Or 𝐴𝑅 Po 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3o 1071  wral 3050   class class class wbr 4804   Po wpo 5185   Or wor 5186
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 197  df-an 385  df-so 5188
This theorem is referenced by:  sonr  5208  sotr  5209  so2nr  5211  so3nr  5212  soltmin  5690  predso  5860  soxp  7459  fimax2g  8373  wofi  8376  fimin2g  8570  ordtypelem8  8597  wemaplem2  8619  wemapsolem  8622  cantnf  8765  fin23lem27  9362  iccpnfhmeo  22965  xrhmeo  22966  logccv  24629  ex-po  27624  xrge0iifiso  30311  soseq  32081  incsequz2  33876
  Copyright terms: Public domain W3C validator