Theorem sopo 5523

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

Syntax hints:   → wi 4   ∨ w3o 1085  ∀wral 3065   class class class wbr 5075   Po wpo 5502   Or wor 5503

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 206  df-an 397  df-so 5505

This theorem is referenced by:  sonr  5527  sotr  5528  so2nr  5530  so3nr  5531  soltmin  6046  predso  6231  tz6.26  6254  wfi  6257  wfisg  6260  wfis2fg  6263  soxp  7979  wfrfun  8172  wfrresex  8173  wfr2a  8174  wfr1  8175  fimax2g  9069  wofi  9072  fimin2g  9265  ordtypelem8  9293  wemaplem2  9315  wemapsolem  9318  cantnf  9460  fin23lem27  10093  iccpnfhmeo  24117  xrhmeo  24118  logccv  25827  ex-po  28808  xrge0iifiso  31894  soseq  33812  on2recsfn  33835  on2recsov  33836  on2ind  33837  on3ind  33838  incsequz2  35916  prproropf1olem1  44966