Theorem ltsopi 7152

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

Assertion

Ref	Expression
ltsopi	⊢ <N Or N

Proof of Theorem ltsopi

Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elirrv 4471	. . . . . 6 ⊢ ¬ 𝑥 ∈ 𝑥
2		ltpiord 7151	. . . . . . 7 ⊢ ((𝑥 ∈ N ∧ 𝑥 ∈ N) → (𝑥 <N 𝑥 ↔ 𝑥 ∈ 𝑥))
3	2	anidms 395	. . . . . 6 ⊢ (𝑥 ∈ N → (𝑥 <N 𝑥 ↔ 𝑥 ∈ 𝑥))
4	1, 3	mtbiri 665	. . . . 5 ⊢ (𝑥 ∈ N → ¬ 𝑥 <N 𝑥)
5	4	adantl 275	. . . 4 ⊢ ((⊤ ∧ 𝑥 ∈ N) → ¬ 𝑥 <N 𝑥)
6		pion 7142	. . . . . . . 8 ⊢ (𝑧 ∈ N → 𝑧 ∈ On)
7		ontr1 4319	. . . . . . . 8 ⊢ (𝑧 ∈ On → ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑧) → 𝑥 ∈ 𝑧))
8	6, 7	syl 14	. . . . . . 7 ⊢ (𝑧 ∈ N → ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑧) → 𝑥 ∈ 𝑧))
9	8	3ad2ant3 1005	. . . . . 6 ⊢ ((𝑥 ∈ N ∧ 𝑦 ∈ N ∧ 𝑧 ∈ N) → ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑧) → 𝑥 ∈ 𝑧))
10		ltpiord 7151	. . . . . . . 8 ⊢ ((𝑥 ∈ N ∧ 𝑦 ∈ N) → (𝑥 <N 𝑦 ↔ 𝑥 ∈ 𝑦))
11	10	3adant3 1002	. . . . . . 7 ⊢ ((𝑥 ∈ N ∧ 𝑦 ∈ N ∧ 𝑧 ∈ N) → (𝑥 <N 𝑦 ↔ 𝑥 ∈ 𝑦))
12		ltpiord 7151	. . . . . . . 8 ⊢ ((𝑦 ∈ N ∧ 𝑧 ∈ N) → (𝑦 <N 𝑧 ↔ 𝑦 ∈ 𝑧))
13	12	3adant1 1000	. . . . . . 7 ⊢ ((𝑥 ∈ N ∧ 𝑦 ∈ N ∧ 𝑧 ∈ N) → (𝑦 <N 𝑧 ↔ 𝑦 ∈ 𝑧))
14	11, 13	anbi12d 465	. . . . . 6 ⊢ ((𝑥 ∈ N ∧ 𝑦 ∈ N ∧ 𝑧 ∈ N) → ((𝑥 <N 𝑦 ∧ 𝑦 <N 𝑧) ↔ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑧)))
15		ltpiord 7151	. . . . . . 7 ⊢ ((𝑥 ∈ N ∧ 𝑧 ∈ N) → (𝑥 <N 𝑧 ↔ 𝑥 ∈ 𝑧))
16	15	3adant2 1001	. . . . . 6 ⊢ ((𝑥 ∈ N ∧ 𝑦 ∈ N ∧ 𝑧 ∈ N) → (𝑥 <N 𝑧 ↔ 𝑥 ∈ 𝑧))
17	9, 14, 16	3imtr4d 202	. . . . 5 ⊢ ((𝑥 ∈ N ∧ 𝑦 ∈ N ∧ 𝑧 ∈ N) → ((𝑥 <N 𝑦 ∧ 𝑦 <N 𝑧) → 𝑥 <N 𝑧))
18	17	adantl 275	. . . 4 ⊢ ((⊤ ∧ (𝑥 ∈ N ∧ 𝑦 ∈ N ∧ 𝑧 ∈ N)) → ((𝑥 <N 𝑦 ∧ 𝑦 <N 𝑧) → 𝑥 <N 𝑧))
19	5, 18	ispod 4234	. . 3 ⊢ (⊤ → <N Po N)
20		pinn 7141	. . . . . 6 ⊢ (𝑥 ∈ N → 𝑥 ∈ ω)
21		pinn 7141	. . . . . 6 ⊢ (𝑦 ∈ N → 𝑦 ∈ ω)
22		nntri3or 6397	. . . . . 6 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥))
23	20, 21, 22	syl2an 287	. . . . 5 ⊢ ((𝑥 ∈ N ∧ 𝑦 ∈ N) → (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥))
24		biidd 171	. . . . . 6 ⊢ ((𝑥 ∈ N ∧ 𝑦 ∈ N) → (𝑥 = 𝑦 ↔ 𝑥 = 𝑦))
25		ltpiord 7151	. . . . . . 7 ⊢ ((𝑦 ∈ N ∧ 𝑥 ∈ N) → (𝑦 <N 𝑥 ↔ 𝑦 ∈ 𝑥))
26	25	ancoms 266	. . . . . 6 ⊢ ((𝑥 ∈ N ∧ 𝑦 ∈ N) → (𝑦 <N 𝑥 ↔ 𝑦 ∈ 𝑥))
27	10, 24, 26	3orbi123d 1290	. . . . 5 ⊢ ((𝑥 ∈ N ∧ 𝑦 ∈ N) → ((𝑥 <N 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 <N 𝑥) ↔ (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥)))
28	23, 27	mpbird 166	. . . 4 ⊢ ((𝑥 ∈ N ∧ 𝑦 ∈ N) → (𝑥 <N 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 <N 𝑥))
29	28	adantl 275	. . 3 ⊢ ((⊤ ∧ (𝑥 ∈ N ∧ 𝑦 ∈ N)) → (𝑥 <N 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 <N 𝑥))
30	19, 29	issod 4249	. 2 ⊢ (⊤ → <N Or N)
31	30	mptru 1341	1 ⊢ <N Or N

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103   ↔ wb 104   ∨ w3o 962   ∧ w3a 963  ⊤wtru 1333   ∈ wcel 1481   class class class wbr 3937   Or wor 4225  Oncon0 4293  ωcom 4512  Ncnpi 7104   <_N clti 7107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-13 1492  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-sep 4054  ax-nul 4062  ax-pow 4106  ax-pr 4139  ax-un 4363  ax-setind 4460  ax-iinf 4510

This theorem depends on definitions:  df-bi 116  df-3or 964  df-3an 965  df-tru 1335  df-nf 1438  df-sb 1737  df-eu 2003  df-mo 2004  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ne 2310  df-ral 2422  df-rex 2423  df-v 2691  df-dif 3078  df-un 3080  df-in 3082  df-ss 3089  df-nul 3369  df-pw 3517  df-sn 3538  df-pr 3539  df-op 3541  df-uni 3745  df-int 3780  df-br 3938  df-opab 3998  df-tr 4035  df-eprel 4219  df-po 4226  df-iso 4227  df-iord 4296  df-on 4298  df-suc 4301  df-iom 4513  df-xp 4553  df-ni 7136  df-lti 7139

This theorem is referenced by:  ltsonq  7230