Theorem sopo 5052

Description: A strict linear order is a strict partial order. (Contributed by NM, 28-Mar-1997.)

Assertion

Ref	Expression
sopo	|- ( R Or A -> R Po A )

Proof of Theorem sopo

Dummy variables x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-so 5036	. 2 |- ( R Or A <-> ( R Po A /\ A. x e. A A. y e. A ( x R y \/ x = y \/ y R x ) ) )
2	1	simplbi 476	1 |- ( R Or A -> R Po A )

Syntax hints:   -> wi 4   \/ w3o 1036   A.wral 2912   class class class wbr 4653   Po wpo 5033   Or wor 5034

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 386  df-so 5036

This theorem is referenced by:  sonr  5056  sotr  5057  so2nr  5059  so3nr  5060  soltmin  5532  predso  5699  soxp  7290  fimax2g  8206  wofi  8209  fimin2g  8403  ordtypelem8  8430  wemaplem2  8452  wemapsolem  8455  cantnf  8590  fin23lem27  9150  iccpnfhmeo  22744  xrhmeo  22745  logccv  24409  ex-po  27292  xrge0iifiso  29981  soseq  31751  incsequz2  33545