Metamath Proof Explorer

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

Proof

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