Theorem sopo 5513

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

Syntax hints:   → wi 4   ∨ w3o 1084  ∀wral 3063   class class class wbr 5070   Po wpo 5492   Or wor 5493

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 5495

This theorem is referenced by:  sonr  5517  sotr  5518  so2nr  5520  so3nr  5521  soltmin  6030  predso  6216  tz6.26  6235  wfi  6238  wfisg  6241  wfis2fg  6244  soxp  7941  wfrfun  8134  wfrresex  8135  wfr2a  8136  wfr1  8137  fimax2g  8990  wofi  8993  fimin2g  9186  ordtypelem8  9214  wemaplem2  9236  wemapsolem  9239  cantnf  9381  fin23lem27  10015  iccpnfhmeo  24014  xrhmeo  24015  logccv  25723  ex-po  28700  xrge0iifiso  31787  soseq  33730  on2recsfn  33753  on2recsov  33754  on2ind  33755  on3ind  33756  incsequz2  35834  prproropf1olem1  44843