Theorem sopo 5568

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

Syntax hints:   → wi 4   ∨ w3o 1085  ∀wral 3045   class class class wbr 5110   Po wpo 5547   Or wor 5548

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 5550

This theorem is referenced by:  sonr  5573  sotr  5574  so2nr  5577  so3nr  5578  soltmin  6112  predso  6300  tz6.26  6323  wfi  6325  wfisg  6327  wfis2fg  6329  soxp  8111  soseq  8141  wfrfun  8305  wfrresex  8306  wfr2a  8307  wfr1  8308  on2recsfn  8634  on2recsov  8635  on2ind  8636  on3ind  8637  fimax2g  9240  wofi  9243  fimin2g  9457  ordtypelem8  9485  wemaplem2  9507  wemapsolem  9510  cantnf  9653  fin23lem27  10288  iccpnfhmeo  24850  xrhmeo  24851  logccv  26579  ex-po  30371  xrge0iifiso  33932  weiunso  36461  incsequz2  37750  epirron  43250  oneptr  43251  prproropf1olem1  47508