Theorem sopo 5585

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

This proof depends on syntax axioms:   → wi 4   ∨ w3o 1102  ∀wral 3080   class class class wbr 5108   Po wpo 5564   Or wor 5565

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-so 5567

This theorem is used by:  sonr  5590  sotr  5591  so2nr  5594  so3nr  5595  soltmin  6148  predso  6353  tz6.26  6376  wfi  6378  wfisg  6380  wfis2fg  6382  soxp  8178  soseq  8213  wfrfun  8379  wfrresex  8380  wfr2a  8381  wfr1  8382  on2recsfn  8714  on2recsov  8715  on2ind  8716  on3ind  8717  fimax2g  9315  wofi  9318  fimin2g  9528  ordtypelem8  9556  wemaplem2  9578  wemapsolem  9581  cantnf  9731  fin23lem27  10445  iccpnfhmeo  25321  xrhmeo  25322  logccv  27048  ons2ind  28718  ex-po  31093  xrge0iifiso  34678  weiunso  37469  incsequz2  38949  epirron  44517  oneptr  44518  chnsuslle  48164  prproropf1olem1  48858