Theorem sopo 5582

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

This proof depends on syntax axioms:   → wi 4   ∨ w3o 1102  ∀wral 3076   class class class wbr 5103   Po wpo 5561   Or wor 5562

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-so 5564

This theorem is used by:  sonr  5587  sotr  5588  so2nr  5591  so3nr  5592  soltmin  6130  predso  6322  tz6.26  6345  wfi  6347  wfisg  6349  wfis2fg  6351  soxp  8128  soseq  8158  wfrfun  8323  wfrresex  8324  wfr2a  8325  wfr1  8326  on2recsfn  8656  on2recsov  8657  on2ind  8658  on3ind  8659  fimax2g  9257  wofi  9260  fimin2g  9470  ordtypelem8  9498  wemaplem2  9520  wemapsolem  9523  cantnf  9673  fin23lem27  10331  iccpnfhmeo  25174  xrhmeo  25175  logccv  26901  ons2ind  28541  ex-po  30916  xrge0iifiso  34446  weiunso  37086  incsequz2  38500  epirron  44096  oneptr  44097  chnsuslle  47710  prproropf1olem1  48404