Theorem sopo 5188

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

Syntax hints:   → wi 4   ∨ w3o 1070  ∀wral 3061   class class class wbr 4787   Po wpo 5169   Or wor 5170

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 197  df-an 383  df-so 5172

This theorem is referenced by:  sonr  5192  sotr  5193  so2nr  5195  so3nr  5196  soltmin  5672  predso  5841  soxp  7445  fimax2g  8366  wofi  8369  fimin2g  8563  ordtypelem8  8590  wemaplem2  8612  wemapsolem  8615  cantnf  8758  fin23lem27  9356  iccpnfhmeo  22964  xrhmeo  22965  logccv  24630  ex-po  27634  xrge0iifiso  30321  soseq  32091  incsequz2  33877