Theorem sopo 4976

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

Syntax hints:   → wi 4   ∨ w3o 1030  ∀wral 2896   class class class wbr 4583   Po wpo 4957   Or wor 4958

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 196  df-an 385  df-so 4960

This theorem is referenced by:  sonr  4980  sotr  4981  so2nr  4983  so3nr  4984  soltmin  5451  predso  5616  soxp  7177  fimax2g  8091  wofi  8094  fimin2g  8286  ordtypelem8  8313  wemaplem2  8335  wemapsolem  8338  cantnf  8473  fin23lem27  9033  iccpnfhmeo  22552  xrhmeo  22553  logccv  24209  ex-po  26684  xrge0iifiso  29309  socnv  30908  soseq  30995  incsequz2  32715