Theorem sopo 5574

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.

Step	Hyp	Ref	Expression
1		df-so 5556	. 2 ⊢ (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)))
2	1	simplbi 500	1 ⊢ (𝑅 Or 𝐴 → 𝑅 Po 𝐴)

Syntax hints:   → wi 4   ∨ w3o 1097  ∀wral 3076   class class class wbr 5100   Po wpo 5553   Or wor 5554

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 209  df-an 400  df-so 5556

This theorem is referenced by:  sonr  5579  sotr  5580  so2nr  5583  so3nr  5584  soltmin  6123  predso  6311  tz6.26  6334  wfi  6336  wfisg  6338  wfis2fg  6340  soxp  8109  soseq  8139  wfrfun  8304  wfrresex  8305  wfr2a  8306  wfr1  8307  on2recsfn  8637  on2recsov  8638  on2ind  8639  on3ind  8640  fimax2g  9230  wofi  9233  fimin2g  9445  ordtypelem8  9473  wemaplem2  9495  wemapsolem  9498  cantnf  9648  fin23lem27  10285  iccpnfhmeo  25007  xrhmeo  25008  logccv  26728  ons2ind  28368  ex-po  30637  xrge0iifiso  34232  weiunso  36826  incsequz2  38248  epirron  43831  oneptr  43832  chnsuslle  47457  prproropf1olem1  48109