Theorem sopo 5565

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

Syntax hints:   → wi 4   ∨ w3o 1085  ∀wral 3044   class class class wbr 5107   Po wpo 5544   Or wor 5545

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 5547

This theorem is referenced by:  sonr  5570  sotr  5571  so2nr  5574  so3nr  5575  soltmin  6109  predso  6297  tz6.26  6320  wfi  6322  wfisg  6324  wfis2fg  6326  soxp  8108  soseq  8138  wfrfun  8302  wfrresex  8303  wfr2a  8304  wfr1  8305  on2recsfn  8631  on2recsov  8632  on2ind  8633  on3ind  8634  fimax2g  9233  wofi  9236  fimin2g  9450  ordtypelem8  9478  wemaplem2  9500  wemapsolem  9503  cantnf  9646  fin23lem27  10281  iccpnfhmeo  24843  xrhmeo  24844  logccv  26572  ex-po  30364  xrge0iifiso  33925  weiunso  36454  incsequz2  37743  epirron  43243  oneptr  43244  prproropf1olem1  47504