Theorem sopo 5559

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

Syntax hints:   → wi 4   ∨ w3o 1086  ∀wral 3052   class class class wbr 5100   Po wpo 5538   Or wor 5539

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 5541

This theorem is referenced by:  sonr  5564  sotr  5565  so2nr  5568  so3nr  5569  soltmin  6101  predso  6290  tz6.26  6313  wfi  6315  wfisg  6317  wfis2fg  6319  soxp  8081  soseq  8111  wfrfun  8275  wfrresex  8276  wfr2a  8277  wfr1  8278  on2recsfn  8605  on2recsov  8606  on2ind  8607  on3ind  8608  fimax2g  9198  wofi  9201  fimin2g  9414  ordtypelem8  9442  wemaplem2  9464  wemapsolem  9467  cantnf  9614  fin23lem27  10250  iccpnfhmeo  24911  xrhmeo  24912  logccv  26640  ons2ind  28283  ex-po  30522  xrge0iifiso  34113  weiunso  36682  incsequz2  38000  epirron  43611  oneptr  43612  chnsuslle  47239  prproropf1olem1  47863