Theorem sopo 5486

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

Syntax hints:   → wi 4   ∨ w3o 1082  ∀wral 3138   class class class wbr 5058   Po wpo 5466   Or wor 5467

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 209  df-an 399  df-so 5469

This theorem is referenced by:  sonr  5490  sotr  5491  so2nr  5493  so3nr  5494  soltmin  5990  predso  6161  soxp  7817  fimax2g  8758  wofi  8761  fimin2g  8955  ordtypelem8  8983  wemaplem2  9005  wemapsolem  9008  cantnf  9150  fin23lem27  9744  iccpnfhmeo  23543  xrhmeo  23544  logccv  25240  ex-po  28208  xrge0iifiso  31173  soseq  33091  incsequz2  35018  prproropf1olem1  43659