Theorem sopo 5551

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

Syntax hints:   → wi 4   ∨ w3o 1085  ∀wral 3051   class class class wbr 5098   Po wpo 5530   Or wor 5531

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 5533

This theorem is referenced by:  sonr  5556  sotr  5557  so2nr  5560  so3nr  5561  soltmin  6093  predso  6282  tz6.26  6305  wfi  6307  wfisg  6309  wfis2fg  6311  soxp  8071  soseq  8101  wfrfun  8265  wfrresex  8266  wfr2a  8267  wfr1  8268  on2recsfn  8595  on2recsov  8596  on2ind  8597  on3ind  8598  fimax2g  9186  wofi  9189  fimin2g  9402  ordtypelem8  9430  wemaplem2  9452  wemapsolem  9455  cantnf  9602  fin23lem27  10238  iccpnfhmeo  24899  xrhmeo  24900  logccv  26628  ons2ind  28271  ex-po  30510  xrge0iifiso  34092  weiunso  36660  incsequz2  37950  epirron  43496  oneptr  43497  chnsuslle  47125  prproropf1olem1  47749