Theorem ltsopi 5016

Description: Positive integer 'less than' is a strict ordering.

Assertion

Ref	Expression
ltsopi	|- <N Or N.

Proof of Theorem ltsopi

Step	Hyp	Ref	Expression
1		ordtri2 2982	. . . . . 6 |- ((Ord x /\ Ord y) -> (x e. y <-> -. (x = y \/ y e. x)))
2		piord 5008	. . . . . 6 |- (x e. N. -> Ord x)
3		piord 5008	. . . . . 6 |- (y e. N. -> Ord y)
4	1, 2, 3	syl2an 454	. . . . 5 |- ((x e. N. /\ y e. N.) -> (x e. y <-> -. (x = y \/ y e. x)))
5		ltpiord 5015	. . . . 5 |- ((x e. N. /\ y e. N.) -> (x <N y <-> x e. y))
6		ltpiord 5015	. . . . . . . 8 |- ((y e. N. /\ x e. N.) -> (y <N x <-> y e. x))
7	6	ancoms 436	. . . . . . 7 |- ((x e. N. /\ y e. N.) -> (y <N x <-> y e. x))
8	7	orbi2d 614	. . . . . 6 |- ((x e. N. /\ y e. N.) -> ((x = y \/ y <N x) <-> (x = y \/ y e. x)))
9	8	negbid 611	. . . . 5 |- ((x e. N. /\ y e. N.) -> (-. (x = y \/ y <N x) <-> -. (x = y \/ y e. x)))
10	4, 5, 9	3bitr4d 550	. . . 4 |- ((x e. N. /\ y e. N.) -> (x <N y <-> -. (x = y \/ y <N x)))
11	10	3adant3 799	. . 3 |- ((x e. N. /\ y e. N. /\ z e. N.) -> (x <N y <-> -. (x = y \/ y <N x)))
12		3simp3 790	. . . . 5 |- ((x e. N. /\ y e. N. /\ z e. N.) -> z e. N.)
13		pion 5007	. . . . 5 |- (z e. N. -> z e. On)
14		ontr1 3003	. . . . 5 |- (z e. On -> ((x e. y /\ y e. z) -> x e. z))
15	12, 13, 14	3syl 20	. . . 4 |- ((x e. N. /\ y e. N. /\ z e. N.) -> ((x e. y /\ y e. z) -> x e. z))
16	5	3adant3 799	. . . . 5 |- ((x e. N. /\ y e. N. /\ z e. N.) -> (x <N y <-> x e. y))
17		ltpiord 5015	. . . . . 6 |- ((y e. N. /\ z e. N.) -> (y <N z <-> y e. z))
18	17	3adant1 797	. . . . 5 |- ((x e. N. /\ y e. N. /\ z e. N.) -> (y <N z <-> y e. z))
19	16, 18	anbi12d 628	. . . 4 |- ((x e. N. /\ y e. N. /\ z e. N.) -> ((x <N y /\ y <N z) <-> (x e. y /\ y e. z)))
20		ltpiord 5015	. . . . 5 |- ((x e. N. /\ z e. N.) -> (x <N z <-> x e. z))
21	20	3adant2 798	. . . 4 |- ((x e. N. /\ y e. N. /\ z e. N.) -> (x <N z <-> x e. z))
22	15, 19, 21	3imtr4d 543	. . 3 |- ((x e. N. /\ y e. N. /\ z e. N.) -> ((x <N y /\ y <N z) -> x <N z))
23	11, 22	jca 288	. 2 |- ((x e. N. /\ y e. N. /\ z e. N.) -> ((x <N y <-> -. (x = y \/ y <N x)) /\ ((x <N y /\ y <N z) -> x <N z)))
24	23	so 2864	1 |- <N Or N.

Syntax hints:  -. wn 2   -> wi 3   <-> wb 146   \/ wo 222   /\ wa 223   /\ w3a 775   = wceq 956   e. wcel 958   class class class wbr 2619   Or wor 2839  Ord word 2947  Oncon0 2948  N.cnpi 4972   <N clti 4975

This theorem is referenced by:  indpi 5034  ltsopq 5075  prlem934b 5138

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-11 967  ax-12 968  ax-13 969  ax-14 970  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459  ax-sep 2703  ax-pow 2742  ax-pr 2779

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 776  df-3an 777  df-ex 981  df-sb 1172  df-eu 1382  df-mo 1383  df-clab 1464  df-cleq 1469  df-clel 1472  df-ne 1587  df-ral 1649  df-rex 1650  df-v 1812  df-dif 2049  df-un 2050  df-in 2051  df-ss 2053  df-nul 2281  df-pw 2402  df-sn 2412  df-pr 2413  df-op 2416  df-uni 2504  df-br 2620  df-opab 2667  df-tr 2681  df-eprel 2832  df-po 2840  df-so 2850  df-fr 2917  df-we 2934  df-ord 2951  df-on 2952  df-om 3132  df-xp 3184  df-ni 5000  df-lti 5003

Copyright terms: Public domain