Theorem sopo 5611

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

Syntax hints:   → wi 4   ∨ w3o 1086  ∀wral 3061   class class class wbr 5143   Po wpo 5590   Or wor 5591

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 5593

This theorem is referenced by:  sonr  5616  sotr  5617  so2nr  5620  so3nr  5621  soltmin  6156  predso  6345  tz6.26  6368  wfi  6371  wfisg  6374  wfis2fg  6377  soxp  8154  soseq  8184  wfrfun  8372  wfrresex  8373  wfr2a  8374  wfr1  8375  on2recsfn  8705  on2recsov  8706  on2ind  8707  on3ind  8708  fimax2g  9322  wofi  9325  fimin2g  9537  ordtypelem8  9565  wemaplem2  9587  wemapsolem  9590  cantnf  9733  fin23lem27  10368  iccpnfhmeo  24976  xrhmeo  24977  logccv  26705  ex-po  30454  xrge0iifiso  33934  weiunso  36467  incsequz2  37756  epirron  43266  oneptr  43267  prproropf1olem1  47490