Theorem sopo 5549

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

Syntax hints:   → wi 4   ∨ w3o 1085  ∀wral 3049   class class class wbr 5096   Po wpo 5528   Or wor 5529

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 5531

This theorem is referenced by:  sonr  5554  sotr  5555  so2nr  5558  so3nr  5559  soltmin  6091  predso  6280  tz6.26  6303  wfi  6305  wfisg  6307  wfis2fg  6309  soxp  8069  soseq  8099  wfrfun  8263  wfrresex  8264  wfr2a  8265  wfr1  8266  on2recsfn  8593  on2recsov  8594  on2ind  8595  on3ind  8596  fimax2g  9184  wofi  9187  fimin2g  9400  ordtypelem8  9428  wemaplem2  9450  wemapsolem  9453  cantnf  9600  fin23lem27  10236  iccpnfhmeo  24897  xrhmeo  24898  logccv  26626  ex-po  30459  xrge0iifiso  34041  weiunso  36609  incsequz2  37889  epirron  43438  oneptr  43439  chnsuslle  47067  prproropf1olem1  47691