Theorem lmemlt ≪ | index | src | ≫ 

theorem lmemlt (a l: nat): $ a IN l -> a < l $;
StepHypRefExpression
1 id 
_1 = l -> _1 = l
2 1 lmemeq2d 
_1 = l -> (a IN _1 <-> a IN l)
3 1 lteq2d 
_1 = l -> (a < _1 <-> a < l)
4 2, 3 imeqd 
_1 = l -> (a IN _1 -> a < _1 <-> a IN l -> a < l)
5 id 
_1 = 0 -> _1 = 0
6 5 lmemeq2d 
_1 = 0 -> (a IN _1 <-> a IN 0)
7 5 lteq2d 
_1 = 0 -> (a < _1 <-> a < 0)
8 6, 7 imeqd 
_1 = 0 -> (a IN _1 -> a < _1 <-> a IN 0 -> a < 0)
9 id 
_1 = a2 -> _1 = a2
10 9 lmemeq2d 
_1 = a2 -> (a IN _1 <-> a IN a2)
11 9 lteq2d 
_1 = a2 -> (a < _1 <-> a < a2)
12 10, 11 imeqd 
_1 = a2 -> (a IN _1 -> a < _1 <-> a IN a2 -> a < a2)
13 id 
_1 = a1 : a2 -> _1 = a1 : a2
14 13 lmemeq2d 
_1 = a1 : a2 -> (a IN _1 <-> a IN a1 : a2)
15 13 lteq2d 
_1 = a1 : a2 -> (a < _1 <-> a < a1 : a2)
16 14, 15 imeqd 
_1 = a1 : a2 -> (a IN _1 -> a < _1 <-> a IN a1 : a2 -> a < a1 : a2)
17 absurd 
~a IN 0 -> a IN 0 -> a < 0
18 lmem0 
~a IN 0
19 17, 18 ax_mp 
a IN 0 -> a < 0
20 lmemS 
a IN a1 : a2 <-> a = a1 \/ a IN a2
21 ltconsid1 
a1 < a1 : a2
22 lteq1 
a = a1 -> (a < a1 : a2 <-> a1 < a1 : a2)
23 21, 22 mpbiri 
a = a1 -> a < a1 : a2
24 23 a1i 
(a IN a2 -> a < a2) -> a = a1 -> a < a1 : a2
25 ltconsid2 
a2 < a1 : a2
26 lttr 
a < a2 -> a2 < a1 : a2 -> a < a1 : a2
27 25, 26 mpi 
a < a2 -> a < a1 : a2
28 27 imim2i 
(a IN a2 -> a < a2) -> a IN a2 -> a < a1 : a2
29 24, 28 eord 
(a IN a2 -> a < a2) -> a = a1 \/ a IN a2 -> a < a1 : a2
30 20, 29 syl5bi 
(a IN a2 -> a < a2) -> a IN a1 : a2 -> a < a1 : a2
31 4, 8, 12, 16, 19, 30 listind 
a IN l -> a < l

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp, itru), axs_pred_calc (ax_gen, ax_4, ax_5, ax_6, ax_7, ax_10, ax_11, ax_12), axs_set (elab, ax_8), axs_the (theid, the0), axs_peano (peano1, peano2, peano5, addeq, muleq, add0, addS, mul0, mulS)