Theorem sopo 5589

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

Syntax hints:   → wi 4   ∨ w3o 1100  ∀wral 3085   class class class wbr 5113   Po wpo 5568   Or wor 5569

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 210  df-an 401  df-so 5571

This theorem is referenced by:  sonr  5594  sotr  5595  so2nr  5598  so3nr  5599  soltmin  6137  predso  6326  tz6.26  6349  wfi  6351  wfisg  6353  wfis2fg  6355  soxp  8124  soseq  8154  wfrfun  8319  wfrresex  8320  wfr2a  8321  wfr1  8322  on2recsfn  8652  on2recsov  8653  on2ind  8654  on3ind  8655  fimax2g  9245  wofi  9248  fimin2g  9458  ordtypelem8  9486  wemaplem2  9508  wemapsolem  9511  cantnf  9661  fin23lem27  10311  iccpnfhmeo  25072  xrhmeo  25073  logccv  26793  ons2ind  28433  ex-po  30726  xrge0iifiso  34269  weiunso  36865  incsequz2  38287  epirron  43872  oneptr  43873  chnsuslle  47488  prproropf1olem1  48140