Theorem lmemappend ≪ | index | src | ≫ 

theorem lmemappend (a b x: nat): $ x IN a ++ b <-> x IN a \/ x IN b $;
StepHypRefExpression
1 id 
_1 = a -> _1 = a
2 1 appendeq1d 
_1 = a -> _1 ++ b = a ++ b
3 2 lmemeq2d 
_1 = a -> (x IN _1 ++ b <-> x IN a ++ b)
4 1 lmemeq2d 
_1 = a -> (x IN _1 <-> x IN a)
5 4 oreq1d 
_1 = a -> (x IN _1 \/ x IN b <-> x IN a \/ x IN b)
6 3, 5 bieqd 
_1 = a -> (x IN _1 ++ b <-> x IN _1 \/ x IN b <-> (x IN a ++ b <-> x IN a \/ x IN b))
7 id 
_1 = 0 -> _1 = 0
8 7 appendeq1d 
_1 = 0 -> _1 ++ b = 0 ++ b
9 8 lmemeq2d 
_1 = 0 -> (x IN _1 ++ b <-> x IN 0 ++ b)
10 7 lmemeq2d 
_1 = 0 -> (x IN _1 <-> x IN 0)
11 10 oreq1d 
_1 = 0 -> (x IN _1 \/ x IN b <-> x IN 0 \/ x IN b)
12 9, 11 bieqd 
_1 = 0 -> (x IN _1 ++ b <-> x IN _1 \/ x IN b <-> (x IN 0 ++ b <-> x IN 0 \/ x IN b))
13 id 
_1 = a2 -> _1 = a2
14 13 appendeq1d 
_1 = a2 -> _1 ++ b = a2 ++ b
15 14 lmemeq2d 
_1 = a2 -> (x IN _1 ++ b <-> x IN a2 ++ b)
16 13 lmemeq2d 
_1 = a2 -> (x IN _1 <-> x IN a2)
17 16 oreq1d 
_1 = a2 -> (x IN _1 \/ x IN b <-> x IN a2 \/ x IN b)
18 15, 17 bieqd 
_1 = a2 -> (x IN _1 ++ b <-> x IN _1 \/ x IN b <-> (x IN a2 ++ b <-> x IN a2 \/ x IN b))
19 id 
_1 = a1 : a2 -> _1 = a1 : a2
20 19 appendeq1d 
_1 = a1 : a2 -> _1 ++ b = a1 : a2 ++ b
21 20 lmemeq2d 
_1 = a1 : a2 -> (x IN _1 ++ b <-> x IN a1 : a2 ++ b)
22 19 lmemeq2d 
_1 = a1 : a2 -> (x IN _1 <-> x IN a1 : a2)
23 22 oreq1d 
_1 = a1 : a2 -> (x IN _1 \/ x IN b <-> x IN a1 : a2 \/ x IN b)
24 21, 23 bieqd 
_1 = a1 : a2 -> (x IN _1 ++ b <-> x IN _1 \/ x IN b <-> (x IN a1 : a2 ++ b <-> x IN a1 : a2 \/ x IN b))
25 bitr4 
(x IN 0 ++ b <-> x IN b) -> (x IN 0 \/ x IN b <-> x IN b) -> (x IN 0 ++ b <-> x IN 0 \/ x IN b)
26 lmemeq2 
0 ++ b = b -> (x IN 0 ++ b <-> x IN b)
27 append0 
0 ++ b = b
28 26, 27 ax_mp 
x IN 0 ++ b <-> x IN b
29 25, 28 ax_mp 
(x IN 0 \/ x IN b <-> x IN b) -> (x IN 0 ++ b <-> x IN 0 \/ x IN b)
30 bior1 
~x IN 0 -> (x IN 0 \/ x IN b <-> x IN b)
31 lmem0 
~x IN 0
32 30, 31 ax_mp 
x IN 0 \/ x IN b <-> x IN b
33 29, 32 ax_mp 
x IN 0 ++ b <-> x IN 0 \/ x IN b
34 lmemeq2 
a1 : a2 ++ b = a1 : (a2 ++ b) -> (x IN a1 : a2 ++ b <-> x IN a1 : (a2 ++ b))
35 appendS 
a1 : a2 ++ b = a1 : (a2 ++ b)
36 34, 35 ax_mp 
x IN a1 : a2 ++ b <-> x IN a1 : (a2 ++ b)
37 lmemS 
x IN a1 : a2 <-> x = a1 \/ x IN a2
38 37 oreq1i 
x IN a1 : a2 \/ x IN b <-> x = a1 \/ x IN a2 \/ x IN b
39 lmemS 
x IN a1 : (a2 ++ b) <-> x = a1 \/ x IN a2 ++ b
40 orass 
x = a1 \/ x IN a2 \/ x IN b <-> x = a1 \/ (x IN a2 \/ x IN b)
41 id 
(x IN a2 ++ b <-> x IN a2 \/ x IN b) -> (x IN a2 ++ b <-> x IN a2 \/ x IN b)
42 41 oreq2d 
(x IN a2 ++ b <-> x IN a2 \/ x IN b) -> (x = a1 \/ x IN a2 ++ b <-> x = a1 \/ (x IN a2 \/ x IN b))
43 39, 40, 42 bitr4g 
(x IN a2 ++ b <-> x IN a2 \/ x IN b) -> (x IN a1 : (a2 ++ b) <-> x = a1 \/ x IN a2 \/ x IN b)
44 36, 38, 43 bitr4g 
(x IN a2 ++ b <-> x IN a2 \/ x IN b) -> (x IN a1 : a2 ++ b <-> x IN a1 : a2 \/ x IN b)
45 6, 12, 18, 24, 33, 44 listind 
x IN a ++ b <-> x IN a \/ x IN b

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)