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

Theorem sopo 5565
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 5547 . 2 (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)))
21simplbi 499 1 (𝑅 Or 𝐴𝑅 Po 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3o 1087  wral 3065   class class class wbr 5106   Po wpo 5544   Or wor 5545
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 206  df-an 398  df-so 5547
This theorem is referenced by:  sonr  5569  sotr  5570  so2nr  5572  so3nr  5573  soltmin  6091  predso  6279  tz6.26  6302  wfi  6305  wfisg  6308  wfis2fg  6311  soxp  8062  soseq  8092  wfrfun  8279  wfrresex  8280  wfr2a  8281  wfr1  8282  on2recsfn  8614  on2recsov  8615  on2ind  8616  on3ind  8617  fimax2g  9234  wofi  9237  fimin2g  9434  ordtypelem8  9462  wemaplem2  9484  wemapsolem  9487  cantnf  9630  fin23lem27  10265  iccpnfhmeo  24311  xrhmeo  24312  logccv  26021  ex-po  29382  xrge0iifiso  32519  incsequz2  36211  epirron  41591  oneptr  41592  prproropf1olem1  45702
  Copyright terms: Public domain W3C validator