Theorem sopo 5588

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

Syntax hints:   → wi 4   ∨ w3o 1102  ∀wral 3079   class class class wbr 5109   Po wpo 5567   Or wor 5568

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 210  df-an 401  df-so 5570

This theorem is referenced by:  sonr  5593  sotr  5594  so2nr  5597  so3nr  5598  soltmin  6136  predso  6325  tz6.26  6348  wfi  6350  wfisg  6352  wfis2fg  6354  soxp  8121  soseq  8151  wfrfun  8316  wfrresex  8317  wfr2a  8318  wfr1  8319  on2recsfn  8649  on2recsov  8650  on2ind  8651  on3ind  8652  fimax2g  9242  wofi  9245  fimin2g  9455  ordtypelem8  9483  wemaplem2  9505  wemapsolem  9508  cantnf  9658  fin23lem27  10307  iccpnfhmeo  25104  xrhmeo  25105  logccv  26828  ons2ind  28468  ex-po  30786  xrge0iifiso  34325  weiunso  36977  incsequz2  38400  epirron  43981  oneptr  43982  chnsuslle  47597  prproropf1olem1  48252