Theorem sopo 5569

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

Syntax hints:   → wi 4   ∨ w3o 1086  ∀wral 3060   class class class wbr 5110   Po wpo 5548   Or wor 5549

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 397  df-so 5551

This theorem is referenced by:  sonr  5573  sotr  5574  so2nr  5576  so3nr  5577  soltmin  6095  predso  6283  tz6.26  6306  wfi  6309  wfisg  6312  wfis2fg  6315  soxp  8066  soseq  8096  wfrfun  8283  wfrresex  8284  wfr2a  8285  wfr1  8286  on2recsfn  8618  on2recsov  8619  on2ind  8620  on3ind  8621  fimax2g  9240  wofi  9243  fimin2g  9442  ordtypelem8  9470  wemaplem2  9492  wemapsolem  9495  cantnf  9638  fin23lem27  10273  iccpnfhmeo  24345  xrhmeo  24346  logccv  26055  ex-po  29442  xrge0iifiso  32605  incsequz2  36281  epirron  41646  oneptr  41647  prproropf1olem1  45815