Theorem sopo 5609

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

Syntax hints:   → wi 4   ∨ w3o 1084  ∀wral 3058   class class class wbr 5148   Po wpo 5588   Or wor 5589

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 206  df-an 396  df-so 5591

This theorem is referenced by:  sonr  5613  sotr  5614  so2nr  5616  so3nr  5617  soltmin  6142  predso  6330  tz6.26  6353  wfi  6356  wfisg  6359  wfis2fg  6362  soxp  8134  soseq  8164  wfrfun  8353  wfrresex  8354  wfr2a  8355  wfr1  8356  on2recsfn  8688  on2recsov  8689  on2ind  8690  on3ind  8691  fimax2g  9314  wofi  9317  fimin2g  9521  ordtypelem8  9549  wemaplem2  9571  wemapsolem  9574  cantnf  9717  fin23lem27  10352  iccpnfhmeo  24883  xrhmeo  24884  logccv  26610  ex-po  30258  xrge0iifiso  33536  incsequz2  37222  epirron  42682  oneptr  42683  prproropf1olem1  46843