Theorem sopo 5552

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

Syntax hints:   → wi 4   ∨ w3o 1086  ∀wral 3052   class class class wbr 5086   Po wpo 5531   Or wor 5532

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 5534

This theorem is referenced by:  sonr  5557  sotr  5558  so2nr  5561  so3nr  5562  soltmin  6094  predso  6283  tz6.26  6306  wfi  6308  wfisg  6310  wfis2fg  6312  soxp  8073  soseq  8103  wfrfun  8267  wfrresex  8268  wfr2a  8269  wfr1  8270  on2recsfn  8597  on2recsov  8598  on2ind  8599  on3ind  8600  fimax2g  9190  wofi  9193  fimin2g  9406  ordtypelem8  9434  wemaplem2  9456  wemapsolem  9459  cantnf  9608  fin23lem27  10244  iccpnfhmeo  24925  xrhmeo  24926  logccv  26643  ons2ind  28284  ex-po  30523  xrge0iifiso  34098  weiunso  36667  incsequz2  38087  epirron  43703  oneptr  43704  chnsuslle  47330  prproropf1olem1  47978