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

Theorem sopo 5188
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 5172 . 2 (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)))
21simplbi 485 1 (𝑅 Or 𝐴𝑅 Po 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3o 1070  wral 3061   class class class wbr 4787   Po wpo 5169   Or wor 5170
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 383  df-so 5172
This theorem is referenced by:  sonr  5192  sotr  5193  so2nr  5195  so3nr  5196  soltmin  5672  predso  5841  soxp  7445  fimax2g  8366  wofi  8369  fimin2g  8563  ordtypelem8  8590  wemaplem2  8612  wemapsolem  8615  cantnf  8758  fin23lem27  9356  iccpnfhmeo  22964  xrhmeo  22965  logccv  24630  ex-po  27634  xrge0iifiso  30321  soseq  32091  incsequz2  33877
  Copyright terms: Public domain W3C validator