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 496	1 ⊢ (𝑅 Or 𝐴 → 𝑅 Po 𝐴)

Syntax hints:   → wi 4   ∨ w3o 1086  ∀wral 3051   class class class wbr 5085   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  6099  predso  6288  tz6.26  6311  wfi  6313  wfisg  6315  wfis2fg  6317  soxp  8079  soseq  8109  wfrfun  8273  wfrresex  8274  wfr2a  8275  wfr1  8276  on2recsfn  8603  on2recsov  8604  on2ind  8605  on3ind  8606  fimax2g  9196  wofi  9199  fimin2g  9412  ordtypelem8  9440  wemaplem2  9462  wemapsolem  9465  cantnf  9614  fin23lem27  10250  iccpnfhmeo  24912  xrhmeo  24913  logccv  26627  ons2ind  28267  ex-po  30505  xrge0iifiso  34079  weiunso  36648  incsequz2  38070  epirron  43682  oneptr  43683  chnsuslle  47311  prproropf1olem1  47963