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 3076   class class class wbr 5102   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  6132  predso  6330  tz6.26  6353  wfi  6355  wfisg  6357  wfis2fg  6359  soxp  8148  soseq  8183  wfrfun  8349  wfrresex  8350  wfr2a  8351  wfr1  8352  on2recsfn  8684  on2recsov  8685  on2ind  8686  on3ind  8687  fimax2g  9285  wofi  9288  fimin2g  9498  ordtypelem8  9526  wemaplem2  9548  wemapsolem  9551  cantnf  9701  fin23lem27  10413  iccpnfhmeo  25275  xrhmeo  25276  logccv  27000  ons2ind  28670  ex-po  31045  xrge0iifiso  34617  weiunso  37378  incsequz2  38820  epirron  44393  oneptr  44394  chnsuslle  48027  prproropf1olem1  48721