Theorem sopo 2848

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 2847	. 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 773   = wceq 955  A.wral 1644   class class class wbr 2616   Po wpo 2835   Or wor 2836

This theorem is referenced by:  sonr 2852  sotr 2853  so2nr 2855  so3nr 2856

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 2847

Copyright terms: Public domain