Theorem ltsopi

Description: Positive integer 'less than' is a strict ordering. (Contributed by NM, 8-Feb-1996) (Proof shortened by Mario Carneiro, 10-Jul-2014) (New usage is discouraged.)

	Ref	Expression
Assertion	ltsopi	|-

Proof

Step	Hyp	Ref	Expression
1		df-ni	|- N. = ( _om \ { (/) } )
2		difss	|- ( _om \ { (/) } ) C_ _om
3		omsson	|- _om C_ On
4	2 3	sstri	|- ( _om \ { (/) } ) C_ On
5	1 4	eqsstri	|- N. C_ On
6		epweon	|- _E We On
7		weso	|- ( _E We On -> _E Or On )
8	6 7	ax-mp	|- _E Or On
9		soss	|- ( N. C_ On -> ( _E Or On -> _E Or N. ) )
10	5 8 9	mp2	|- _E Or N.
11		df-lti	|-
12		soeq1	|- ( ( ( _E i^i ( N. X. N. ) ) Or N. ) )
13	11 12	ax-mp	|- ( ( _E i^i ( N. X. N. ) ) Or N. )
14		soinxp	|- ( _E Or N. <-> ( _E i^i ( N. X. N. ) ) Or N. )
15	13 14	bitr4i	|- ( _E Or N. )
16	10 15	mpbir	|-