Theorem sopo 5608

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

Syntax hints:   → wi 4   ∨ w3o 1087  ∀wral 3062   class class class wbr 5149   Po wpo 5587   Or wor 5588

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 206  df-an 398  df-so 5590

This theorem is referenced by:  sonr  5612  sotr  5613  so2nr  5615  so3nr  5616  soltmin  6138  predso  6326  tz6.26  6349  wfi  6352  wfisg  6355  wfis2fg  6358  soxp  8115  soseq  8145  wfrfun  8332  wfrresex  8333  wfr2a  8334  wfr1  8335  on2recsfn  8666  on2recsov  8667  on2ind  8668  on3ind  8669  fimax2g  9289  wofi  9292  fimin2g  9492  ordtypelem8  9520  wemaplem2  9542  wemapsolem  9545  cantnf  9688  fin23lem27  10323  iccpnfhmeo  24461  xrhmeo  24462  logccv  26171  ex-po  29688  xrge0iifiso  32915  incsequz2  36617  epirron  42003  oneptr  42004  prproropf1olem1  46171