Theorem sopo 5545

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

Syntax hints:   → wi 4   ∨ w3o 1091  ∀wral 3053   class class class wbr 5072   Po wpo 5524   Or wor 5525

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 208  df-an 397  df-so 5527

This theorem is referenced by:  sonr  5550  sotr  5551  so2nr  5554  so3nr  5555  soltmin  6086  predso  6275  tz6.26  6298  wfi  6300  wfisg  6302  wfis2fg  6304  soxp  8069  soseq  8099  wfrfun  8263  wfrresex  8264  wfr2a  8265  wfr1  8266  on2recsfn  8593  on2recsov  8594  on2ind  8595  on3ind  8596  fimax2g  9186  wofi  9189  fimin2g  9402  ordtypelem8  9430  wemaplem2  9452  wemapsolem  9455  cantnf  9605  fin23lem27  10241  iccpnfhmeo  24930  xrhmeo  24931  logccv  26645  ons2ind  28285  ex-po  30523  xrge0iifiso  34119  weiunso  36694  incsequz2  38116  epirron  43699  oneptr  43700  chnsuslle  47326  prproropf1olem1  47978