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

Theorem sopo 5012
 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 4996 . 2 (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)))
21simplbi 476 1 (𝑅 Or 𝐴𝑅 Po 𝐴)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∨ w3o 1035  ∀wral 2907   class class class wbr 4613   Po wpo 4993   Or wor 4994 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 386  df-so 4996 This theorem is referenced by:  sonr  5016  sotr  5017  so2nr  5019  so3nr  5020  soltmin  5491  predso  5658  soxp  7235  fimax2g  8150  wofi  8153  fimin2g  8347  ordtypelem8  8374  wemaplem2  8396  wemapsolem  8399  cantnf  8534  fin23lem27  9094  iccpnfhmeo  22652  xrhmeo  22653  logccv  24309  ex-po  27146  xrge0iifiso  29763  socnv  31363  soseq  31452  incsequz2  33177
 Copyright terms: Public domain W3C validator