Theorem sopo 5558

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 5540	. 2 ⊢ (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)))
2	1	simplbi 497	1 ⊢ (𝑅 Or 𝐴 → 𝑅 Po 𝐴)

Syntax hints:   → wi 4   ∨ w3o 1085  ∀wral 3044   class class class wbr 5102   Po wpo 5537   Or wor 5538

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 5540

This theorem is referenced by:  sonr  5563  sotr  5564  so2nr  5567  so3nr  5568  soltmin  6097  predso  6285  tz6.26  6308  wfi  6310  wfisg  6312  wfis2fg  6314  soxp  8085  soseq  8115  wfrfun  8279  wfrresex  8280  wfr2a  8281  wfr1  8282  on2recsfn  8608  on2recsov  8609  on2ind  8610  on3ind  8611  fimax2g  9209  wofi  9212  fimin2g  9426  ordtypelem8  9454  wemaplem2  9476  wemapsolem  9479  cantnf  9622  fin23lem27  10257  iccpnfhmeo  24819  xrhmeo  24820  logccv  26548  ex-po  30337  xrge0iifiso  33898  weiunso  36427  incsequz2  37716  epirron  43216  oneptr  43217  prproropf1olem1  47477