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	$$⊢{<}_{𝑵}\mathrm{Or}𝑵$$

Proof

Step	Hyp	Ref	Expression
1		df-ni	$$⊢𝑵=\mathrm{\omega }\setminus \left\{\varnothing \right\}$$
2		difss	$$⊢\mathrm{\omega }\setminus \left\{\varnothing \right\}\subseteq \mathrm{\omega }$$
3		omsson	$$⊢\mathrm{\omega }\subseteq \mathrm{On}$$
4	2 3	sstri	$$⊢\mathrm{\omega }\setminus \left\{\varnothing \right\}\subseteq \mathrm{On}$$
5	1 4	eqsstri	$$⊢𝑵\subseteq \mathrm{On}$$
6		epweon	$$⊢\mathrm{E}\mathrm{We}\mathrm{On}$$
7		weso	$$⊢\mathrm{E}\mathrm{We}\mathrm{On}\to \mathrm{E}\mathrm{Or}\mathrm{On}$$
8	6 7	ax-mp	$$⊢\mathrm{E}\mathrm{Or}\mathrm{On}$$
9		soss	$$⊢𝑵\subseteq \mathrm{On}\to \left(\mathrm{E}\mathrm{Or}\mathrm{On}\to \mathrm{E}\mathrm{Or}𝑵\right)$$
10	5 8 9	mp2	$$⊢\mathrm{E}\mathrm{Or}𝑵$$
11		df-lti	$$⊢{<}_{𝑵}=\mathrm{E}\cap \left(𝑵\times 𝑵\right)$$
12		soeq1	$$⊢{<}_{𝑵}=\mathrm{E}\cap \left(𝑵\times 𝑵\right)\to \left({<}_{𝑵}\mathrm{Or}𝑵\leftrightarrow \left(\mathrm{E}\cap \left(𝑵\times 𝑵\right)\right)\mathrm{Or}𝑵\right)$$
13	11 12	ax-mp	$$⊢{<}_{𝑵}\mathrm{Or}𝑵\leftrightarrow \left(\mathrm{E}\cap \left(𝑵\times 𝑵\right)\right)\mathrm{Or}𝑵$$
14		soinxp	$$⊢\mathrm{E}\mathrm{Or}𝑵\leftrightarrow \left(\mathrm{E}\cap \left(𝑵\times 𝑵\right)\right)\mathrm{Or}𝑵$$
15	13 14	bitr4i	$$⊢{<}_{𝑵}\mathrm{Or}𝑵\leftrightarrow \mathrm{E}\mathrm{Or}𝑵$$
16	10 15	mpbir	$$⊢{<}_{𝑵}\mathrm{Or}𝑵$$