Theorem sopo 5578

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

This proof depends on syntax axioms:   → wi 4   ∨ w3o 1102  ∀wral 3077   class class class wbr 5103   Po wpo 5557   Or wor 5558

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-so 5560

This theorem is used by:  sonr  5583  sotr  5584  so2nr  5587  so3nr  5588  soltmin  6130  predso  6327  tz6.26  6350  wfi  6352  wfisg  6354  wfis2fg  6356  soxp  8141  soseq  8176  wfrfun  8341  wfrresex  8342  wfr2a  8343  wfr1  8344  on2recsfn  8676  on2recsov  8677  on2ind  8678  on3ind  8679  fimax2g  9277  wofi  9280  fimin2g  9491  ordtypelem8  9519  wemaplem2  9541  wemapsolem  9544  cantnf  9694  fin23lem27  10406  iccpnfhmeo  25266  xrhmeo  25267  logccv  26991  ons2ind  28661  ex-po  31036  xrge0iifiso  34567  weiunso  37254  incsequz2  38683  epirron  44255  oneptr  44256  chnsuslle  47890  prproropf1olem1  48584