Theorem sopo 2851

Description: A strict linear order is a strict partial order.

Assertion

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

Proof of Theorem sopo

Step	Hyp	Ref	Expression
1		df-so 2850	. 2 |- (R Or A <-> (R Po A /\ A.x e. A A.y e. A (xRy \/ x = y \/ yRx)))
2	1	pm3.26bi 322	1 |- (R Or A -> R Po A)

Syntax hints:   -> wi 3   \/ w3o 774   = wceq 956  A.wral 1645   class class class wbr 2619   Po wpo 2838   Or wor 2839

This theorem is referenced by:  sonr 2855  sotr 2856  so2nr 2858  so3nr 2859

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225  df-so 2850

Copyright terms: Public domain