Theorem sopo 5580

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

Syntax hints:   → wi 4   ∨ w3o 1085  ∀wral 3051   class class class wbr 5119   Po wpo 5559   Or wor 5560

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 5562

This theorem is referenced by:  sonr  5585  sotr  5586  so2nr  5589  so3nr  5590  soltmin  6125  predso  6313  tz6.26  6336  wfi  6339  wfisg  6342  wfis2fg  6345  soxp  8128  soseq  8158  wfrfun  8346  wfrresex  8347  wfr2a  8348  wfr1  8349  on2recsfn  8679  on2recsov  8680  on2ind  8681  on3ind  8682  fimax2g  9294  wofi  9297  fimin2g  9511  ordtypelem8  9539  wemaplem2  9561  wemapsolem  9564  cantnf  9707  fin23lem27  10342  iccpnfhmeo  24894  xrhmeo  24895  logccv  26624  ex-po  30416  xrge0iifiso  33966  weiunso  36484  incsequz2  37773  epirron  43278  oneptr  43279  prproropf1olem1  47517