Theorem issod 4835

Description: An irreflexive, transitive, linear relation is a strict ordering. (Contributed by NM, 21-Jan-1996.) (Revised by Mario Carneiro, 9-Jul-2014.)

Hypotheses

Ref	Expression
issod.1
issod.2

Assertion

Ref	Expression
issod

Distinct variable groups:   ,,   ,,   ,,

Proof of Theorem issod

Step	Hyp	Ref	Expression
1		issod.1	. 2
2		issod.2	. . 3
3	2	ralrimivva 2878	. 2
4		df-so 4806	. 2
5	1, 3, 4	sylanbrc 664	1

Syntax hints:  ->wi 4  /\wa 369  \/w3o 972  e.wcel 1818  A.wral 2807   class class class wbr 4452  Powpo 4803  Orwor 4804

This theorem is referenced by:  issoi  4836  swoso  7361  wemapsolem  7996  legso  23985  socnv  29194  fin2so  30040

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704

This theorem depends on definitions:  df-bi 185  df-an 371  df-ral 2812  df-so 4806