Theorem sopo 5627

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

Syntax hints:   → wi 4   ∨ w3o 1086  ∀wral 3067   class class class wbr 5166   Po wpo 5605   Or wor 5606

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 207  df-an 396  df-so 5608

This theorem is referenced by:  sonr  5632  sotr  5633  so2nr  5635  so3nr  5636  soltmin  6168  predso  6356  tz6.26  6379  wfi  6382  wfisg  6385  wfis2fg  6388  soxp  8170  soseq  8200  wfrfun  8388  wfrresex  8389  wfr2a  8390  wfr1  8391  on2recsfn  8723  on2recsov  8724  on2ind  8725  on3ind  8726  fimax2g  9350  wofi  9353  fimin2g  9566  ordtypelem8  9594  wemaplem2  9616  wemapsolem  9619  cantnf  9762  fin23lem27  10397  iccpnfhmeo  24995  xrhmeo  24996  logccv  26723  ex-po  30467  xrge0iifiso  33881  weiunso  36432  incsequz2  37709  epirron  43215  oneptr  43216  prproropf1olem1  47377