Theorem sopo 5590

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

This proof depends on syntax axioms:   → wi 4   ∨ w3o 1102  ∀wral 3081   class class class wbr 5111   Po wpo 5569   Or wor 5570

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 5572

This theorem is used by:  sonr  5595  sotr  5596  so2nr  5599  so3nr  5600  soltmin  6138  predso  6329  tz6.26  6352  wfi  6354  wfisg  6356  wfis2fg  6358  soxp  8131  soseq  8161  wfrfun  8326  wfrresex  8327  wfr2a  8328  wfr1  8329  on2recsfn  8659  on2recsov  8660  on2ind  8661  on3ind  8662  fimax2g  9253  wofi  9256  fimin2g  9466  ordtypelem8  9494  wemaplem2  9516  wemapsolem  9519  cantnf  9669  fin23lem27  10327  iccpnfhmeo  25157  xrhmeo  25158  logccv  26881  ons2ind  28521  ex-po  30859  xrge0iifiso  34391  weiunso  37036  incsequz2  38460  epirron  44041  oneptr  44042  chnsuslle  47657  prproropf1olem1  48312