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

Theorem sopo 5611
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 5593 . 2 (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)))
21simplbi 497 1 (𝑅 Or 𝐴𝑅 Po 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3o 1086  wral 3061   class class class wbr 5143   Po wpo 5590   Or wor 5591
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 207  df-an 396  df-so 5593
This theorem is referenced by:  sonr  5616  sotr  5617  so2nr  5620  so3nr  5621  soltmin  6156  predso  6345  tz6.26  6368  wfi  6371  wfisg  6374  wfis2fg  6377  soxp  8154  soseq  8184  wfrfun  8372  wfrresex  8373  wfr2a  8374  wfr1  8375  on2recsfn  8705  on2recsov  8706  on2ind  8707  on3ind  8708  fimax2g  9322  wofi  9325  fimin2g  9537  ordtypelem8  9565  wemaplem2  9587  wemapsolem  9590  cantnf  9733  fin23lem27  10368  iccpnfhmeo  24976  xrhmeo  24977  logccv  26705  ex-po  30454  xrge0iifiso  33934  weiunso  36467  incsequz2  37756  epirron  43266  oneptr  43267  prproropf1olem1  47490
  Copyright terms: Public domain W3C validator