Theorem sopo 5541

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

Syntax hints:   → wi 4   ∨ w3o 1085  ∀wral 3047   class class class wbr 5089   Po wpo 5520   Or wor 5521

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 5523

This theorem is referenced by:  sonr  5546  sotr  5547  so2nr  5550  so3nr  5551  soltmin  6082  predso  6271  tz6.26  6294  wfi  6296  wfisg  6298  wfis2fg  6300  soxp  8059  soseq  8089  wfrfun  8253  wfrresex  8254  wfr2a  8255  wfr1  8256  on2recsfn  8582  on2recsov  8583  on2ind  8584  on3ind  8585  fimax2g  9170  wofi  9173  fimin2g  9383  ordtypelem8  9411  wemaplem2  9433  wemapsolem  9436  cantnf  9583  fin23lem27  10219  iccpnfhmeo  24870  xrhmeo  24871  logccv  26599  ex-po  30415  xrge0iifiso  33948  weiunso  36510  incsequz2  37799  epirron  43357  oneptr  43358  chnsuslle  46989  prproropf1olem1  47613