Theorem sopo 5616

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

Syntax hints:   → wi 4   ∨ w3o 1085  ∀wral 3059   class class class wbr 5148   Po wpo 5595   Or wor 5596

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 5598

This theorem is referenced by:  sonr  5621  sotr  5622  so2nr  5624  so3nr  5625  soltmin  6159  predso  6347  tz6.26  6370  wfi  6373  wfisg  6376  wfis2fg  6379  soxp  8153  soseq  8183  wfrfun  8371  wfrresex  8372  wfr2a  8373  wfr1  8374  on2recsfn  8704  on2recsov  8705  on2ind  8706  on3ind  8707  fimax2g  9320  wofi  9323  fimin2g  9535  ordtypelem8  9563  wemaplem2  9585  wemapsolem  9588  cantnf  9731  fin23lem27  10366  iccpnfhmeo  24990  xrhmeo  24991  logccv  26720  ex-po  30464  xrge0iifiso  33896  weiunso  36449  incsequz2  37736  epirron  43243  oneptr  43244  prproropf1olem1  47428