ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  enq0tr Unicode version

Theorem enq0tr 6417
Description: The equivalence relation for non-negative fractions is transitive. Lemma for enq0er 6418. (Contributed by Jim Kingdon, 14-Nov-2019.)
Assertion
Ref Expression
enq0tr ~Q0 ~Q0  h ~Q0  h

Proof of Theorem enq0tr
Dummy variables  a  b  c  d  e  s  t are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 vex 2554 . . . . . . . . . 10 
_V
2 vex 2554 . . . . . . . . . 10 
_V
3 eleq1 2097 . . . . . . . . . . . 12  om  X.  N.  om  X.  N.
43anbi1d 438 . . . . . . . . . . 11  om  X.  N.  om  X.  N.  om  X.  N.  om  X.  N.
5 eqeq1 2043 . . . . . . . . . . . . . 14  <. ,  >.  <. ,  >.
65anbi1d 438 . . . . . . . . . . . . 13  <. ,  >.  <. ,  >. 
<. ,  >.  <. ,  >.
76anbi1d 438 . . . . . . . . . . . 12  <. ,  >.  <. ,  >.  .o  .o  <. ,  >.  <. ,  >.  .o  .o
874exbidv 1747 . . . . . . . . . . 11  <. ,  >.  <. ,  >.  .o  .o 
<. ,  >.  <. ,  >.  .o  .o
94, 8anbi12d 442 . . . . . . . . . 10  om  X.  N.  om  X.  N.  <. ,  >.  <. ,  >.  .o  .o  om  X.  N.  om  X.  N. 
<. ,  >.  <. ,  >.  .o  .o
10 eleq1 2097 . . . . . . . . . . . 12  om  X.  N.  om  X.  N.
1110anbi2d 437 . . . . . . . . . . 11  om  X.  N.  om  X.  N.  om  X.  N.  om  X.  N.
12 eqeq1 2043 . . . . . . . . . . . . . 14  <. ,  >.  <. ,  >.
1312anbi2d 437 . . . . . . . . . . . . 13  <. ,  >.  <. ,  >. 
<. ,  >.  <. ,  >.
1413anbi1d 438 . . . . . . . . . . . 12  <. ,  >.  <. ,  >.  .o  .o  <. ,  >.  <. ,  >.  .o  .o
15144exbidv 1747 . . . . . . . . . . 11  <. ,  >.  <. ,  >.  .o  .o 
<. ,  >.  <. ,  >.  .o  .o
1611, 15anbi12d 442 . . . . . . . . . 10  om  X.  N.  om  X.  N.  <. ,  >.  <. ,  >.  .o  .o  om  X.  N.  om  X.  N. 
<. ,  >.  <. ,  >.  .o  .o
17 df-enq0 6407 . . . . . . . . . 10 ~Q0  { <. ,  >.  |  om  X.  N.  om  X.  N.  <. ,  >.  <. ,  >.  .o  .o  }
181, 2, 9, 16, 17brab 4000 . . . . . . . . 9 ~Q0  om  X.  N.  om  X.  N.  <. ,  >.  <. ,  >.  .o  .o
19 vex 2554 . . . . . . . . . 10  h 
_V
20 eleq1 2097 . . . . . . . . . . . 12  om  X.  N.  om  X.  N.
2120anbi1d 438 . . . . . . . . . . 11  om  X.  N.  om  X.  N.  om  X.  N.  om  X.  N.
22 eqeq1 2043 . . . . . . . . . . . . . 14  <. a ,  b >.  <. a ,  b >.
2322anbi1d 438 . . . . . . . . . . . . 13  <. a ,  b >.  <. s ,  t
>.  <. a ,  b
>.  <. s ,  t >.
2423anbi1d 438 . . . . . . . . . . . 12  <. a ,  b >.  <. s ,  t
>. 
a  .o  t  b  .o  s  <. a ,  b >.  <. s ,  t
>. 
a  .o  t  b  .o  s
25244exbidv 1747 . . . . . . . . . . 11  a b s t  <. a ,  b >.  <. s ,  t
>. 
a  .o  t  b  .o  s  a b s t  <. a ,  b
>.  <. s ,  t >.  a  .o  t  b  .o  s
2621, 25anbi12d 442 . . . . . . . . . 10  om  X.  N.  om  X.  N.  a b s t  <. a ,  b >.  <. s ,  t
>. 
a  .o  t  b  .o  s  om  X.  N.  om  X.  N.  a b s t  <. a ,  b
>.  <. s ,  t >.  a  .o  t  b  .o  s
27 eleq1 2097 . . . . . . . . . . . 12  h  om  X.  N.  h  om  X.  N.
2827anbi2d 437 . . . . . . . . . . 11  h  om  X.  N.  om  X.  N.  om  X.  N.  h  om  X.  N.
29 eqeq1 2043 . . . . . . . . . . . . . 14  h  <. s ,  t >.  h  <. s ,  t >.
3029anbi2d 437 . . . . . . . . . . . . 13  h  <. a ,  b >.  <. s ,  t
>.  <. a ,  b
>.  h  <. s ,  t >.
3130anbi1d 438 . . . . . . . . . . . 12  h  <. a ,  b >.  <. s ,  t
>. 
a  .o  t  b  .o  s  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s
32314exbidv 1747 . . . . . . . . . . 11  h  a b s t  <. a ,  b >.  <. s ,  t
>. 
a  .o  t  b  .o  s  a b s t  <. a ,  b
>.  h  <. s ,  t >.  a  .o  t  b  .o  s
3328, 32anbi12d 442 . . . . . . . . . 10  h  om  X.  N.  om  X.  N.  a b s t  <. a ,  b >.  <. s ,  t
>. 
a  .o  t  b  .o  s  om  X.  N.  h  om  X.  N.  a b s t  <. a ,  b
>.  h  <. s ,  t >.  a  .o  t  b  .o  s
34 df-enq0 6407 . . . . . . . . . 10 ~Q0  { <. ,  >.  |  om  X.  N.  om  X.  N.  a b s t  <. a ,  b >.  <. s ,  t
>. 
a  .o  t  b  .o  s }
352, 19, 26, 33, 34brab 4000 . . . . . . . . 9 ~Q0  h  om  X.  N.  h  om  X.  N.  a b s t  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s
3618, 35anbi12i 433 . . . . . . . 8 ~Q0 ~Q0  h  om  X.  N.  om  X.  N.  <. ,  >.  <. ,  >.  .o  .o  om  X.  N.  h  om  X.  N.  a b s t  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s
3736biimpi 113 . . . . . . 7 ~Q0 ~Q0  h  om  X.  N.  om  X.  N.  <. ,  >.  <. ,  >.  .o  .o  om  X.  N.  h  om  X.  N.  a b s t  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s
38 an4 520 . . . . . . 7  om  X.  N.  om  X.  N.  <. ,  >.  <. ,  >.  .o  .o  om  X.  N.  h  om  X.  N.  a b s t  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  om  X.  N.  om  X.  N.  om  X.  N.  h  om  X.  N.  <. ,  >.  <. ,  >.  .o  .o  a b s t  <. a ,  b
>.  h  <. s ,  t >.  a  .o  t  b  .o  s
3937, 38sylib 127 . . . . . 6 ~Q0 ~Q0  h  om  X.  N.  om  X.  N.  om  X.  N.  h  om  X.  N.  <. ,  >.  <. ,  >.  .o  .o  a b s t  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s
40 3anass 888 . . . . . . . 8  om  X.  N.  om  X.  N.  h  om  X.  N.  om  X.  N.  om  X.  N.  h  om  X.  N.
41 anass 381 . . . . . . . . 9  om  X.  N.  om  X.  N.  om  X.  N.  h  om  X.  N.  om  X.  N.  om  X.  N.  om  X.  N.  h  om  X.  N.
42 anass 381 . . . . . . . . . 10  om  X.  N.  om  X.  N.  h  om  X.  N.  om  X.  N.  om  X.  N.  h  om  X.  N.
4342anbi2i 430 . . . . . . . . 9  om  X.  N.  om  X.  N.  om  X.  N.  h  om  X.  N.  om  X.  N.  om  X.  N.  om  X.  N.  h  om  X.  N.
44 anidm 376 . . . . . . . . . . 11  om  X.  N.  om  X.  N.  om  X.  N.
4544anbi1i 431 . . . . . . . . . 10  om  X.  N.  om  X.  N.  h  om  X.  N.  om  X.  N.  h  om  X.  N.
4645anbi2i 430 . . . . . . . . 9  om  X.  N.  om  X.  N.  om  X.  N.  h  om  X.  N.  om  X.  N.  om  X.  N.  h  om  X.  N.
4741, 43, 463bitr2i 197 . . . . . . . 8  om  X.  N.  om  X.  N.  om  X.  N.  h  om  X.  N.  om  X.  N.  om  X.  N.  h  om  X.  N.
4840, 47bitr4i 176 . . . . . . 7  om  X.  N.  om  X.  N.  h  om  X.  N.  om  X.  N.  om  X.  N.  om  X.  N.  h  om  X.  N.
4948anbi1i 431 . . . . . 6  om  X.  N.  om  X.  N.  h  om  X.  N.  <. ,  >.  <. ,  >.  .o  .o  a b s t  <. a ,  b
>.  h  <. s ,  t >.  a  .o  t  b  .o  s  om  X.  N.  om  X.  N.  om  X.  N.  h  om  X.  N.  <. ,  >.  <. ,  >.  .o  .o  a b s t  <. a ,  b
>.  h  <. s ,  t >.  a  .o  t  b  .o  s
5039, 49sylibr 137 . . . . 5 ~Q0 ~Q0  h  om  X.  N.  om  X.  N.  h  om  X.  N.  <. ,  >.  <. ,  >.  .o  .o  a b s t  <. a ,  b
>.  h  <. s ,  t >.  a  .o  t  b  .o  s
51 ee8anv 1807 . . . . . 6  a b s t  <. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  <. ,  >.  <. ,  >.  .o  .o  a b s t  <. a ,  b
>.  h  <. s ,  t >.  a  .o  t  b  .o  s
5251anbi2i 430 . . . . 5  om  X.  N.  om  X.  N.  h  om  X.  N.  a b s t  <. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  om  X.  N.  om  X.  N.  h  om  X.  N. 
<. ,  >.  <. ,  >.  .o  .o  a b s t  <. a ,  b
>.  h  <. s ,  t >.  a  .o  t  b  .o  s
5350, 52sylibr 137 . . . 4 ~Q0 ~Q0  h  om  X.  N.  om  X.  N.  h  om  X.  N.  a b s t 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s
54 19.42vvvv 1787 . . . . . . 7  a b s t  om  X.  N.  om  X.  N.  h  om  X.  N.  <. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  om  X.  N.  om  X.  N.  h  om  X.  N.  a b s t  <. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s
55542exbii 1494 . . . . . 6  a b s t  om  X.  N.  om  X.  N.  h  om  X.  N.  <. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  om  X.  N.  om  X.  N.  h  om  X.  N.  a b s t 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s
56552exbii 1494 . . . . 5  a b s t  om  X.  N.  om  X.  N.  h  om  X.  N.  <. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  om  X.  N.  om  X.  N.  h  om  X.  N.  a b s t 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s
57 19.42vvvv 1787 . . . . 5  om  X.  N.  om  X.  N.  h  om  X.  N.  a b s t  <. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  om  X.  N.  om  X.  N.  h  om  X.  N.  a b s t 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s
5856, 57bitri 173 . . . 4  a b s t  om  X.  N.  om  X.  N.  h  om  X.  N.  <. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  om  X.  N.  om  X.  N.  h  om  X.  N.  a b s t 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s
5953, 58sylibr 137 . . 3 ~Q0 ~Q0  h  a b s t  om  X.  N.  om  X.  N.  h  om  X.  N.  <. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s
60 3simpb 901 . . . . . . . . 9  om  X.  N.  om  X.  N.  h  om  X.  N.  om  X.  N.  h  om  X.  N.
6160adantr 261 . . . . . . . 8  om  X.  N.  om  X.  N.  h  om  X.  N. 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  om  X.  N.  h  om  X.  N.
62 simplll 485 . . . . . . . . . 10 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  <. ,  >.
63 simprlr 490 . . . . . . . . . 10 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  h  <. s ,  t >.
6462, 63jca 290 . . . . . . . . 9 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  <. ,  >.  h  <. s ,  t
>.
6564adantl 262 . . . . . . . 8  om  X.  N.  om  X.  N.  h  om  X.  N. 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  <. ,  >.  h  <. s ,  t >.
66 oveq1 5462 . . . . . . . . . . . . . . . 16  (/)  .o  t  (/)  .o  t
6763adantl 262 . . . . . . . . . . . . . . . . . . . . . 22  om  X.  N.  om  X.  N.  h  om  X.  N. 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  h 
<. s ,  t >.
68 simpl3 908 . . . . . . . . . . . . . . . . . . . . . 22  om  X.  N.  om  X.  N.  h  om  X.  N. 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  h  om  X.  N.
6967, 68eqeltrrd 2112 . . . . . . . . . . . . . . . . . . . . 21  om  X.  N.  om  X.  N.  h  om  X.  N. 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  <. s ,  t >.  om  X.  N.
70 opelxp 4317 . . . . . . . . . . . . . . . . . . . . 21  <. s ,  t >.  om  X.  N.  s  om  t  N.
7169, 70sylib 127 . . . . . . . . . . . . . . . . . . . 20  om  X.  N.  om  X.  N.  h  om  X.  N. 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  s  om  t  N.
7271simprd 107 . . . . . . . . . . . . . . . . . . 19  om  X.  N.  om  X.  N.  h  om  X.  N. 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  t 
N.
73 pinn 6293 . . . . . . . . . . . . . . . . . . 19  t  N.  t  om
7472, 73syl 14 . . . . . . . . . . . . . . . . . 18  om  X.  N.  om  X.  N.  h  om  X.  N. 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  t 
om
75 nnm0r 5997 . . . . . . . . . . . . . . . . . 18  t  om  (/) 
.o  t  (/)
7674, 75syl 14 . . . . . . . . . . . . . . . . 17  om  X.  N.  om  X.  N.  h  om  X.  N. 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  (/)  .o  t  (/)
7776eqeq2d 2048 . . . . . . . . . . . . . . . 16  om  X.  N.  om  X.  N.  h  om  X.  N. 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  .o  t  (/)  .o  t  .o  t  (/)
7866, 77syl5ib 143 . . . . . . . . . . . . . . 15  om  X.  N.  om  X.  N.  h  om  X.  N. 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  (/)  .o  t  (/)
79 simprr 484 . . . . . . . . . . . . . . . . . 18 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  a  .o  t  b  .o  s
80 eqtr2 2055 . . . . . . . . . . . . . . . . . . . . . 22  <. ,  >.  <. a ,  b
>.  <. ,  >.  <. a ,  b >.
81 vex 2554 . . . . . . . . . . . . . . . . . . . . . . 23 
_V
82 vex 2554 . . . . . . . . . . . . . . . . . . . . . . 23 
_V
8381, 82opth 3965 . . . . . . . . . . . . . . . . . . . . . 22  <. ,  >.  <. a ,  b >.  a  b
8480, 83sylib 127 . . . . . . . . . . . . . . . . . . . . 21  <. ,  >.  <. a ,  b
>.  a  b
85 oveq1 5462 . . . . . . . . . . . . . . . . . . . . . 22  a  .o  t  a  .o  t
86 oveq1 5462 . . . . . . . . . . . . . . . . . . . . . 22  b  .o  s  b  .o  s
8785, 86eqeqan12d 2052 . . . . . . . . . . . . . . . . . . . . 21  a  b  .o  t  .o  s  a  .o  t  b  .o  s
8884, 87syl 14 . . . . . . . . . . . . . . . . . . . 20  <. ,  >.  <. a ,  b
>.  .o  t  .o  s  a  .o  t  b  .o  s
8988ad2ant2lr 479 . . . . . . . . . . . . . . . . . . 19  <. ,  >.  <. ,  >.  <. a ,  b
>.  h  <. s ,  t >.  .o  t  .o  s  a  .o  t  b  .o  s
9089ad2ant2r 478 . . . . . . . . . . . . . . . . . 18 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  .o  t  .o  s  a  .o  t  b  .o  s
9179, 90mpbird 156 . . . . . . . . . . . . . . . . 17 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  .o  t  .o  s
9291eqeq1d 2045 . . . . . . . . . . . . . . . 16 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  .o  t  (/)  .o  s  (/)
9392adantl 262 . . . . . . . . . . . . . . 15  om  X.  N.  om  X.  N.  h  om  X.  N. 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  .o  t  (/)  .o  s  (/)
9478, 93sylibd 138 . . . . . . . . . . . . . 14  om  X.  N.  om  X.  N.  h  om  X.  N. 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  (/)  .o  s  (/)
95 simpllr 486 . . . . . . . . . . . . . . . . . . . 20 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  <. ,  >.
9695adantl 262 . . . . . . . . . . . . . . . . . . 19  om  X.  N.  om  X.  N.  h  om  X.  N. 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s 
<. ,  >.
97 simpl2 907 . . . . . . . . . . . . . . . . . . 19  om  X.  N.  om  X.  N.  h  om  X.  N. 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  om  X.  N.
9896, 97eqeltrrd 2112 . . . . . . . . . . . . . . . . . 18  om  X.  N.  om  X.  N.  h  om  X.  N. 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  <. ,  >.  om  X.  N.
99 opelxp 4317 . . . . . . . . . . . . . . . . . 18  <. ,  >.  om  X.  N.  om  N.
10098, 99sylib 127 . . . . . . . . . . . . . . . . 17  om  X.  N.  om  X.  N.  h  om  X.  N. 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  om  N.
101100simprd 107 . . . . . . . . . . . . . . . 16  om  X.  N.  om  X.  N.  h  om  X.  N. 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s 
N.
102 pinn 6293 . . . . . . . . . . . . . . . 16  N.  om
103101, 102syl 14 . . . . . . . . . . . . . . 15  om  X.  N.  om  X.  N.  h  om  X.  N. 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s 
om
10471simpld 105 . . . . . . . . . . . . . . 15  om  X.  N.  om  X.  N.  h  om  X.  N. 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  s 
om
105 nnm00 6038 . . . . . . . . . . . . . . 15  om  s  om  .o  s  (/)  (/)  s  (/)
106103, 104, 105syl2anc 391 . . . . . . . . . . . . . 14  om  X.  N.  om  X.  N.  h  om  X.  N. 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  .o  s  (/)  (/)  s  (/)
10794, 106sylibd 138 . . . . . . . . . . . . 13  om  X.  N.  om  X.  N.  h  om  X.  N. 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  (/)  (/)  s  (/)
108 elni2 6298 . . . . . . . . . . . . . . . 16  N.  om  (/)
109108simprbi 260 . . . . . . . . . . . . . . 15  N.  (/)
110101, 109syl 14 . . . . . . . . . . . . . 14  om  X.  N.  om  X.  N.  h  om  X.  N. 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  (/)
111 n0i 3223 . . . . . . . . . . . . . 14  (/)  (/)
112 biorf 662 . . . . . . . . . . . . . 14  (/) 
s  (/)  (/)  s  (/)
113110, 111, 1123syl 17 . . . . . . . . . . . . 13  om  X.  N.  om  X.  N.  h  om  X.  N. 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  s  (/)  (/)  s  (/)
114107, 113sylibrd 158 . . . . . . . . . . . 12  om  X.  N.  om  X.  N.  h  om  X.  N. 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  (/)  s  (/)
11562adantl 262 . . . . . . . . . . . . . . . . . 18  om  X.  N.  om  X.  N.  h  om  X.  N. 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s 
<. ,  >.
116 simpl1 906 . . . . . . . . . . . . . . . . . 18  om  X.  N.  om  X.  N.  h  om  X.  N. 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  om  X.  N.
117115, 116eqeltrrd 2112 . . . . . . . . . . . . . . . . 17  om  X.  N.  om  X.  N.  h  om  X.  N. 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  <. ,  >.  om  X.  N.
118 opelxp 4317 . . . . . . . . . . . . . . . . 17  <. ,  >.  om  X.  N.  om  N.
119117, 118sylib 127 . . . . . . . . . . . . . . . 16  om  X.  N.  om  X.  N.  h  om  X.  N. 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  om  N.
120119simprd 107 . . . . . . . . . . . . . . 15  om  X.  N.  om  X.  N.  h  om  X.  N. 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s 
N.
121 pinn 6293 . . . . . . . . . . . . . . 15  N.  om
122120, 121syl 14 . . . . . . . . . . . . . 14  om  X.  N.  om  X.  N.  h  om  X.  N. 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s 
om
123 nnm0 5993 . . . . . . . . . . . . . 14  om  .o  (/)  (/)
124122, 123syl 14 . . . . . . . . . . . . 13  om  X.  N.  om  X.  N.  h  om  X.  N. 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  .o  (/)  (/)
125 oveq2 5463 . . . . . . . . . . . . . 14  s  (/)  .o  s  .o  (/)
126125eqeq1d 2045 . . . . . . . . . . . . 13  s  (/)  .o  s  (/)  .o  (/)  (/)
127124, 126syl5ibrcom 146 . . . . . . . . . . . 12  om  X.  N.  om  X.  N.  h  om  X.  N. 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  s  (/)  .o  s  (/)
128114, 127syld 40 . . . . . . . . . . 11  om  X.  N.  om  X.  N.  h  om  X.  N. 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  (/)  .o  s  (/)
129 oveq2 5463 . . . . . . . . . . . . . . . 16  (/)  .o  .o  (/)
130124eqeq2d 2048 . . . . . . . . . . . . . . . 16  om  X.  N.  om  X.  N.  h  om  X.  N. 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  .o  .o  (/)  .o  (/)
131129, 130syl5ib 143 . . . . . . . . . . . . . . 15  om  X.  N.  om  X.  N.  h  om  X.  N. 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  (/)  .o  (/)
132 simprlr 490 . . . . . . . . . . . . . . . 16  om  X.  N.  om  X.  N.  h  om  X.  N. 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  .o  .o
133132eqeq1d 2045 . . . . . . . . . . . . . . 15  om  X.  N.  om  X.  N.  h  om  X.  N. 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  .o  (/)  .o  (/)
134131, 133sylibrd 158 . . . . . . . . . . . . . 14  om  X.  N.  om  X.  N.  h  om  X.  N. 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  (/)  .o  (/)
135119simpld 105 . . . . . . . . . . . . . . 15  om  X.  N.  om  X.  N.  h  om  X.  N. 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s 
om
136 nnm00 6038 . . . . . . . . . . . . . . 15  om  om  .o  (/)  (/)  (/)
137135, 103, 136syl2anc 391 . . . . . . . . . . . . . 14  om  X.  N.  om  X.  N.  h  om  X.  N. 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  .o  (/)  (/)  (/)
138134, 137sylibd 138 . . . . . . . . . . . . 13  om  X.  N.  om  X.  N.  h  om  X.  N. 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  (/)  (/)  (/)
139 biorf 662 . . . . . . . . . . . . . . 15  (/)  (/)  (/)  (/)
140 orcom 646 . . . . . . . . . . . . . . 15  (/)  (/)  (/)  (/)
141139, 140syl6bb 185 . . . . . . . . . . . . . 14  (/)  (/)  (/)  (/)
142110, 111, 1413syl 17 . . . . . . . . . . . . 13  om  X.  N.  om  X.  N.  h  om  X.  N. 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  (/)  (/)  (/)
143138, 142sylibrd 158 . . . . . . . . . . . 12  om  X.  N.  om  X.  N.  h  om  X.  N. 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  (/)  (/)
144 oveq1 5462 . . . . . . . . . . . . . 14  (/)  .o  t  (/)  .o  t
145144eqeq1d 2045 . . . . . . . . . . . . 13  (/)  .o  t  (/)  (/)  .o  t  (/)
14676, 145syl5ibrcom 146 . . . . . . . . . . . 12  om  X.  N.  om  X.  N.  h  om  X.  N. 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  (/)  .o  t  (/)
147143, 146syld 40 . . . . . . . . . . 11  om  X.  N.  om  X.  N.  h  om  X.  N. 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  (/)  .o  t  (/)
148128, 147jcad 291 . . . . . . . . . 10  om  X.  N.  om  X.  N.  h  om  X.  N. 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  (/)  .o  s  (/)  .o  t  (/)
149 eqtr3 2056 . . . . . . . . . . 11  .o  s  (/)  .o  t  (/)  .o  s  .o  t
150149eqcomd 2042 . . . . . . . . . 10  .o  s  (/)  .o  t  (/)  .o  t  .o  s
151148, 150syl6 29 . . . . . . . . 9  om  X.  N.  om  X.  N.  h  om  X.  N. 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  (/)  .o  t  .o  s
152 simplr 482 . . . . . . . . . . . . . . . . 17 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  .o  .o
15391, 152oveq12d 5473 . . . . . . . . . . . . . . . 16 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  .o  t  .o  .o  .o  s  .o  .o
154153adantl 262 . . . . . . . . . . . . . . 15  om  X.  N.  om  X.  N.  h  om  X.  N. 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  .o  t  .o  .o  .o  s  .o  .o
155100simpld 105 . . . . . . . . . . . . . . . . 17  om  X.  N.  om  X.  N.  h  om  X.  N. 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s 
om
156 nnmcl 5999 . . . . . . . . . . . . . . . . 17  om  t  om  .o  t  om
157155, 74, 156syl2anc 391 . . . . . . . . . . . . . . . 16  om  X.  N.  om  X.  N.  h  om  X.  N. 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  .o  t 
om
158 nnmcom 6007 . . . . . . . . . . . . . . . . 17  c  om  d  om  c  .o  d  d  .o  c
159158adantl 262 . . . . . . . . . . . . . . . 16  om  X.  N.  om  X.  N.  h  om  X.  N.  <. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  c  om  d  om  c  .o  d  d  .o  c
160 nnmass 6005 . . . . . . . . . . . . . . . . 17  c  om  d  om  e  om  c  .o  d  .o  e  c  .o 
d  .o  e
161160adantl 262 . . . . . . . . . . . . . . . 16  om  X.  N.  om  X.  N.  h  om  X.  N.  <. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  c  om  d  om  e 
om  c  .o  d  .o  e  c  .o 
d  .o  e
162157, 135, 103, 159, 161caov13d 5626 . . . . . . . . . . . . . . 15  om  X.  N.  om  X.  N.  h  om  X.  N. 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  .o  t  .o  .o  .o  .o  .o  t
163 nnmcl 5999 . . . . . . . . . . . . . . . . 17  om  om  .o  om
164122, 155, 163syl2anc 391 . . . . . . . . . . . . . . . 16  om  X.  N.  om  X.  N.  h  om  X.  N. 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  .o 
om
165161, 103, 104, 164caovassd 5602 . . . . . . . . . . . . . . 15  om  X.  N.  om  X.  N.  h  om  X.  N. 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  .o  s  .o  .o  .o  s  .o  .o
166154, 162, 1653eqtr3d 2077 . . . . . . . . . . . . . 14  om  X.  N.  om  X.  N.  h  om  X.  N. 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  .o  .o  .o  t  .o  s  .o  .o
167 nnmcl 5999 . . . . . . . . . . . . . . . 16  om  .o  t  om  .o  .o  t  om
168135, 157, 167syl2anc 391 . . . . . . . . . . . . . . 15  om  X.  N.  om  X.  N.  h  om  X.  N. 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  .o  .o  t 
om
169 nnmcl 5999 . . . . . . . . . . . . . . . 16  s  om  .o  om  s  .o  .o  om
170104, 164, 169syl2anc 391 . . . . . . . . . . . . . . 15  om  X.  N.  om  X.  N.  h  om  X.  N. 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  s  .o  .o  om
171 nnmcan 6028 . . . . . . . . . . . . . . 15  om  .o  .o  t  om 
s  .o  .o  om  (/)  .o  .o  .o  t  .o  s  .o  .o  .o  .o  t 
s  .o  .o
172103, 168, 170, 110, 171syl31anc 1137 . . . . . . . . . . . . . 14  om  X.  N.  om  X.  N.  h  om  X.  N. 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  .o  .o  .o  t  .o  s  .o  .o  .o  .o  t 
s  .o  .o
173166, 172mpbid 135 . . . . . . . . . . . . 13  om  X.  N.  om  X.  N.  h  om  X.  N. 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  .o  .o  t  s  .o  .o
174135, 155, 74, 159, 161caov12d 5624 . . . . . . . . . . . . 13  om  X.  N.  om  X.  N.  h  om  X.  N. 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  .o  .o  t  .o  .o  t
175104, 122, 155, 159, 161caov13d 5626 . . . . . . . . . . . . 13  om  X.  N.  om  X.  N.  h  om  X.  N. 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  s  .o  .o  .o  .o  s
176173, 174, 1753eqtr3d 2077 . . . . . . . . . . . 12  om  X.  N.  om  X.  N.  h  om  X.  N. 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  .o  .o  t  .o  .o  s
177176adantr 261 . . . . . . . . . . 11  om  X.  N.  om  X.  N.  h  om  X.  N.  <. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  (/)  .o  .o  t  .o  .o  s
178 nnmcl 5999 . . . . . . . . . . . . . 14  om  t  om  .o  t  om
179135, 74, 178syl2anc 391 . . . . . . . . . . . . 13  om  X.  N.  om  X.  N.  h  om  X.  N. 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  .o  t 
om
180 nnmcl 5999 . . . . . . . . . . . . . 14  om  s  om  .o  s  om
181122, 104, 180syl2anc 391 . . . . . . . . . . . . 13  om  X.  N.  om  X.  N.  h  om  X.  N. 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  .o  s 
om
182155, 179, 1813jca 1083 . . . . . . . . . . . 12  om  X.  N.  om  X.  N.  h  om  X.  N. 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  om  .o  t 
om  .o  s  om
183 nnmcan 6028 . . . . . . . . . . . 12  om  .o  t  om  .o  s 
om  (/)  .o  .o  t  .o  .o  s  .o  t  .o  s
184182, 183sylan 267 . . . . . . . . . . 11  om  X.  N.  om  X.  N.  h  om  X.  N.  <. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  (/)  .o  .o  t  .o  .o  s  .o  t  .o  s
185177, 184mpbid 135 . . . . . . . . . 10  om  X.  N.  om  X.  N.  h  om  X.  N.  <. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  (/)  .o  t  .o  s
186185ex 108 . . . . . . . . 9  om  X.  N.  om  X.  N.  h  om  X.  N. 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  (/)  .o  t  .o  s
187 0elnn 4283 . . . . . . . . . 10  om  (/)  (/)
188155, 187syl 14 . . . . . . . . 9  om  X.  N.  om  X.  N.  h  om  X.  N. 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  (/)  (/)
189151, 186, 188mpjaod 637 . . . . . . . 8  om  X.  N.  om  X.  N.  h  om  X.  N. 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  .o  t  .o  s
19061, 65, 189jca32 293 . . . . . . 7  om  X.  N.  om  X.  N.  h  om  X.  N. 
<. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  om  X.  N.  h  om  X.  N.  <. ,  >.  h  <. s ,  t
>.  .o  t  .o  s
1911902eximi 1489 . . . . . 6  s t  om  X.  N.  om  X.  N.  h  om  X.  N.  <. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  s t  om  X.  N.  h  om  X.  N.  <. ,  >.  h  <. s ,  t
>.  .o  t  .o  s
192191exlimivv 1773 . . . . 5  a b s t  om  X.  N.  om  X.  N.  h  om  X.  N.  <. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  s t  om  X.  N.  h  om  X.  N.  <. ,  >.  h  <. s ,  t
>.  .o  t  .o  s
193192exlimivv 1773 . . . 4  a b s t  om  X.  N.  om  X.  N.  h  om  X.  N.  <. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  s t  om  X.  N.  h  om  X.  N.  <. ,  >.  h  <. s ,  t
>.  .o  t  .o  s
1941932eximi 1489 . . 3  a b s t  om  X.  N.  om  X.  N.  h  om  X.  N.  <. ,  >.  <. ,  >.  .o  .o  <. a ,  b >.  h  <. s ,  t
>. 
a  .o  t  b  .o  s  s t  om  X.  N.  h  om  X.  N.  <. ,  >.  h  <. s ,  t
>.  .o  t  .o  s
19559, 194syl 14 . 2 ~Q0 ~Q0  h  s t  om  X.  N.  h  om  X.  N.  <. ,  >.  h  <. s ,  t
>.  .o  t  .o  s
196 19.42vvvv 1787 . . 3  s t  om  X.  N.  h  om  X.  N.  <. ,  >.  h  <. s ,  t
>.  .o  t  .o  s  om  X.  N.  h  om  X.  N.  s t  <. ,  >.  h  <. s ,  t >.  .o  t  .o  s
1975anbi1d 438 . . . . . . 7  <. ,  >.  <. s ,  t
>.  <. ,  >.  <. s ,  t >.
198197anbi1d 438 . . . . . 6  <. ,  >.  <. s ,  t
>.  .o  t  .o  s  <. ,  >.  <. s ,  t
>.  .o  t  .o  s
1991984exbidv 1747 . . . . 5  s t  <. ,  >.  <. s ,  t
>.  .o  t  .o  s  s t  <. ,  >.  <. s ,  t >.  .o  t  .o  s
2004, 199anbi12d 442 . . . 4  om  X.  N.  om  X.  N.  s t  <. ,  >.  <. s ,  t
>.  .o  t  .o  s  om  X.  N.  om  X.  N.