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	⊢ <N Or N

Proof

Step	Hyp	Ref	Expression
1		df-ni	⊢ N = ( ω ∖ { ∅ } )
2		difss	⊢ ( ω ∖ { ∅ } ) ⊆ ω
3		omsson	⊢ ω ⊆ On
4	2 3	sstri	⊢ ( ω ∖ { ∅ } ) ⊆ On
5	1 4	eqsstri	⊢ N ⊆ 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 ⊆ On → ( E Or On → E Or N ) )
10	5 8 9	mp2	⊢ E Or N
11		df-lti	⊢ <N = ( E ∩ ( N × N ) )
12		soeq1	⊢ ( <N = ( E ∩ ( N × N ) ) → ( <N Or N ↔ ( E ∩ ( N × N ) ) Or N ) )
13	11 12	ax-mp	⊢ ( <N Or N ↔ ( E ∩ ( N × N ) ) Or N )
14		soinxp	⊢ ( E Or N ↔ ( E ∩ ( N × N ) ) Or N )
15	13 14	bitr4i	⊢ ( <N Or N ↔ E Or N )
16	10 15	mpbir	⊢ <N Or N