Theorem lmemappend ≪ | index | src | ≫ 

theorem lmemappend (a b x: nat): $ x IN a ++ b <-> x IN a \/ x IN b $;
StepHypRefExpression
1 eqidd 
_1 = a -> x = x
2 id 
_1 = a -> _1 = a
3 eqidd 
_1 = a -> b = b
4 2, 3 appendeqd 
_1 = a -> _1 ++ b = a ++ b
5 1, 4 lmemeqd 
_1 = a -> (x IN _1 ++ b <-> x IN a ++ b)
6 1, 2 lmemeqd 
_1 = a -> (x IN _1 <-> x IN a)
7 biidd 
_1 = a -> (x IN b <-> x IN b)
8 6, 7 oreqd 
_1 = a -> (x IN _1 \/ x IN b <-> x IN a \/ x IN b)
9 5, 8 bieqd 
_1 = a -> (x IN _1 ++ b <-> x IN _1 \/ x IN b <-> (x IN a ++ b <-> x IN a \/ x IN b))
10 eqidd 
_1 = 0 -> x = x
11 id 
_1 = 0 -> _1 = 0
12 eqidd 
_1 = 0 -> b = b
13 11, 12 appendeqd 
_1 = 0 -> _1 ++ b = 0 ++ b
14 10, 13 lmemeqd 
_1 = 0 -> (x IN _1 ++ b <-> x IN 0 ++ b)
15 10, 11 lmemeqd 
_1 = 0 -> (x IN _1 <-> x IN 0)
16 biidd 
_1 = 0 -> (x IN b <-> x IN b)
17 15, 16 oreqd 
_1 = 0 -> (x IN _1 \/ x IN b <-> x IN 0 \/ x IN b)
18 14, 17 bieqd 
_1 = 0 -> (x IN _1 ++ b <-> x IN _1 \/ x IN b <-> (x IN 0 ++ b <-> x IN 0 \/ x IN b))
19 eqidd 
_1 = a2 -> x = x
20 id 
_1 = a2 -> _1 = a2
21 eqidd 
_1 = a2 -> b = b
22 20, 21 appendeqd 
_1 = a2 -> _1 ++ b = a2 ++ b
23 19, 22 lmemeqd 
_1 = a2 -> (x IN _1 ++ b <-> x IN a2 ++ b)
24 19, 20 lmemeqd 
_1 = a2 -> (x IN _1 <-> x IN a2)
25 biidd 
_1 = a2 -> (x IN b <-> x IN b)
26 24, 25 oreqd 
_1 = a2 -> (x IN _1 \/ x IN b <-> x IN a2 \/ x IN b)
27 23, 26 bieqd 
_1 = a2 -> (x IN _1 ++ b <-> x IN _1 \/ x IN b <-> (x IN a2 ++ b <-> x IN a2 \/ x IN b))
28 eqidd 
_1 = a1 : a2 -> x = x
29 id 
_1 = a1 : a2 -> _1 = a1 : a2
30 eqidd 
_1 = a1 : a2 -> b = b
31 29, 30 appendeqd 
_1 = a1 : a2 -> _1 ++ b = a1 : a2 ++ b
32 28, 31 lmemeqd 
_1 = a1 : a2 -> (x IN _1 ++ b <-> x IN a1 : a2 ++ b)
33 28, 29 lmemeqd 
_1 = a1 : a2 -> (x IN _1 <-> x IN a1 : a2)
34 biidd 
_1 = a1 : a2 -> (x IN b <-> x IN b)
35 33, 34 oreqd 
_1 = a1 : a2 -> (x IN _1 \/ x IN b <-> x IN a1 : a2 \/ x IN b)
36 32, 35 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))
37 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)
38 lmemeq2 
0 ++ b = b -> (x IN 0 ++ b <-> x IN b)
39 append0 
0 ++ b = b
40 38, 39 ax_mp 
x IN 0 ++ b <-> x IN b
41 37, 40 ax_mp 
(x IN 0 \/ x IN b <-> x IN b) -> (x IN 0 ++ b <-> x IN 0 \/ x IN b)
42 bior1 
~x IN 0 -> (x IN 0 \/ x IN b <-> x IN b)
43 lmem0 
~x IN 0
44 42, 43 ax_mp 
x IN 0 \/ x IN b <-> x IN b
45 41, 44 ax_mp 
x IN 0 ++ b <-> x IN 0 \/ x IN b
46 lmemeq2 
a1 : a2 ++ b = a1 : (a2 ++ b) -> (x IN a1 : a2 ++ b <-> x IN a1 : (a2 ++ b))
47 appendS 
a1 : a2 ++ b = a1 : (a2 ++ b)
48 46, 47 ax_mp 
x IN a1 : a2 ++ b <-> x IN a1 : (a2 ++ b)
49 lmemS 
x IN a1 : a2 <-> x = a1 \/ x IN a2
50 49 oreq1i 
x IN a1 : a2 \/ x IN b <-> x = a1 \/ x IN a2 \/ x IN b
51 lmemS 
x IN a1 : (a2 ++ b) <-> x = a1 \/ x IN a2 ++ b
52 orass 
x = a1 \/ x IN a2 \/ x IN b <-> x = a1 \/ (x IN a2 \/ x IN b)
53 id 
(x IN a2 ++ b <-> x IN a2 \/ x IN b) -> (x IN a2 ++ b <-> x IN a2 \/ x IN b)
54 53 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))
55 51, 52, 54 bitr4g 
(x IN a2 ++ b <-> x IN a2 \/ x IN b) -> (x IN a1 : (a2 ++ b) <-> x = a1 \/ x IN a2 \/ x IN b)
56 48, 50, 55 bitr4g 
(x IN a2 ++ b <-> x IN a2 \/ x IN b) -> (x IN a1 : a2 ++ b <-> x IN a1 : a2 \/ x IN b)
57 9, 18, 27, 36, 45, 56 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)