Step | Hyp | Ref | Expression |
1 |
|
eqidd |
_1 = l -> a = a |
2 |
|
id |
_1 = l -> _1 = l |
3 |
1, 2 |
lmemeqd |
_1 = l -> (a IN _1 <-> a IN l) |
4 |
|
eqidd |
_1 = l -> n = n |
5 |
4, 2 |
ntheqd |
_1 = l -> nth n _1 = nth n l |
6 |
|
eqidd |
_1 = l -> suc a = suc a |
7 |
5, 6 |
eqeqd |
_1 = l -> (nth n _1 = suc a <-> nth n l = suc a) |
8 |
7 |
exeqd |
_1 = l -> (E. n nth n _1 = suc a <-> E. n nth n l = suc a) |
9 |
3, 8 |
bieqd |
_1 = l -> (a IN _1 <-> E. n nth n _1 = suc a <-> (a IN l <-> E. n nth n l = suc a)) |
10 |
|
eqidd |
_1 = 0 -> a = a |
11 |
|
id |
_1 = 0 -> _1 = 0 |
12 |
10, 11 |
lmemeqd |
_1 = 0 -> (a IN _1 <-> a IN 0) |
13 |
|
eqidd |
_1 = 0 -> n = n |
14 |
13, 11 |
ntheqd |
_1 = 0 -> nth n _1 = nth n 0 |
15 |
|
eqidd |
_1 = 0 -> suc a = suc a |
16 |
14, 15 |
eqeqd |
_1 = 0 -> (nth n _1 = suc a <-> nth n 0 = suc a) |
17 |
16 |
exeqd |
_1 = 0 -> (E. n nth n _1 = suc a <-> E. n nth n 0 = suc a) |
18 |
12, 17 |
bieqd |
_1 = 0 -> (a IN _1 <-> E. n nth n _1 = suc a <-> (a IN 0 <-> E. n nth n 0 = suc a)) |
19 |
|
eqidd |
_1 = a2 -> a = a |
20 |
|
id |
_1 = a2 -> _1 = a2 |
21 |
19, 20 |
lmemeqd |
_1 = a2 -> (a IN _1 <-> a IN a2) |
22 |
|
eqidd |
_1 = a2 -> n = n |
23 |
22, 20 |
ntheqd |
_1 = a2 -> nth n _1 = nth n a2 |
24 |
|
eqidd |
_1 = a2 -> suc a = suc a |
25 |
23, 24 |
eqeqd |
_1 = a2 -> (nth n _1 = suc a <-> nth n a2 = suc a) |
26 |
25 |
exeqd |
_1 = a2 -> (E. n nth n _1 = suc a <-> E. n nth n a2 = suc a) |
27 |
21, 26 |
bieqd |
_1 = a2 -> (a IN _1 <-> E. n nth n _1 = suc a <-> (a IN a2 <-> E. n nth n a2 = suc a)) |
28 |
|
eqidd |
_1 = a1 : a2 -> a = a |
29 |
|
id |
_1 = a1 : a2 -> _1 = a1 : a2 |
30 |
28, 29 |
lmemeqd |
_1 = a1 : a2 -> (a IN _1 <-> a IN a1 : a2) |
31 |
|
eqidd |
_1 = a1 : a2 -> n = n |
32 |
31, 29 |
ntheqd |
_1 = a1 : a2 -> nth n _1 = nth n (a1 : a2) |
33 |
|
eqidd |
_1 = a1 : a2 -> suc a = suc a |
34 |
32, 33 |
eqeqd |
_1 = a1 : a2 -> (nth n _1 = suc a <-> nth n (a1 : a2) = suc a) |
35 |
34 |
exeqd |
_1 = a1 : a2 -> (E. n nth n _1 = suc a <-> E. n nth n (a1 : a2) = suc a) |
36 |
30, 35 |
bieqd |
_1 = a1 : a2 -> (a IN _1 <-> E. n nth n _1 = suc a <-> (a IN a1 : a2 <-> E. n nth n (a1 : a2) = suc a)) |
37 |
|
binth |
~a IN 0 -> ~E. n nth n 0 = suc a -> (a IN 0 <-> E. n nth n 0 = suc a) |
38 |
|
lmem0 |
~a IN 0 |
39 |
37, 38 |
ax_mp |
~E. n nth n 0 = suc a -> (a IN 0 <-> E. n nth n 0 = suc a) |
40 |
|
necom |
suc a != nth n 0 -> nth n 0 != suc a |
41 |
40 |
conv ne |
suc a != nth n 0 -> ~nth n 0 = suc a |
42 |
|
neeq2 |
nth n 0 = 0 -> (suc a != nth n 0 <-> suc a != 0) |
43 |
|
nth0 |
nth n 0 = 0 |
44 |
42, 43 |
ax_mp |
suc a != nth n 0 <-> suc a != 0 |
45 |
|
peano1 |
suc a != 0 |
46 |
44, 45 |
mpbir |
suc a != nth n 0 |
47 |
41, 46 |
ax_mp |
~nth n 0 = suc a |
48 |
47 |
nexi |
~E. n nth n 0 = suc a |
49 |
39, 48 |
ax_mp |
a IN 0 <-> E. n nth n 0 = suc a |
50 |
|
lmemS |
a IN a1 : a2 <-> a = a1 \/ a IN a2 |
51 |
|
bitr3 |
(E. n (n = 0 /\ nth n (a1 : a2) = suc a \/ ~n = 0 /\ nth n (a1 : a2) = suc a) <->
E. n (n = 0 /\ nth n (a1 : a2) = suc a) \/ E. n (~n = 0 /\ nth n (a1 : a2) = suc a)) ->
(E. n (n = 0 /\ nth n (a1 : a2) = suc a \/ ~n = 0 /\ nth n (a1 : a2) = suc a) <-> E. n nth n (a1 : a2) = suc a) ->
(E. n (n = 0 /\ nth n (a1 : a2) = suc a) \/ E. n (~n = 0 /\ nth n (a1 : a2) = suc a) <-> E. n nth n (a1 : a2) = suc a) |
52 |
|
exor |
E. n (n = 0 /\ nth n (a1 : a2) = suc a \/ ~n = 0 /\ nth n (a1 : a2) = suc a) <->
E. n (n = 0 /\ nth n (a1 : a2) = suc a) \/ E. n (~n = 0 /\ nth n (a1 : a2) = suc a) |
53 |
51, 52 |
ax_mp |
(E. n (n = 0 /\ nth n (a1 : a2) = suc a \/ ~n = 0 /\ nth n (a1 : a2) = suc a) <-> E. n nth n (a1 : a2) = suc a) ->
(E. n (n = 0 /\ nth n (a1 : a2) = suc a) \/ E. n (~n = 0 /\ nth n (a1 : a2) = suc a) <-> E. n nth n (a1 : a2) = suc a) |
54 |
|
bitr3 |
((n = 0 \/ ~n = 0) /\ nth n (a1 : a2) = suc a <-> n = 0 /\ nth n (a1 : a2) = suc a \/ ~n = 0 /\ nth n (a1 : a2) = suc a) ->
((n = 0 \/ ~n = 0) /\ nth n (a1 : a2) = suc a <-> nth n (a1 : a2) = suc a) ->
(n = 0 /\ nth n (a1 : a2) = suc a \/ ~n = 0 /\ nth n (a1 : a2) = suc a <-> nth n (a1 : a2) = suc a) |
55 |
|
andir |
(n = 0 \/ ~n = 0) /\ nth n (a1 : a2) = suc a <-> n = 0 /\ nth n (a1 : a2) = suc a \/ ~n = 0 /\ nth n (a1 : a2) = suc a |
56 |
54, 55 |
ax_mp |
((n = 0 \/ ~n = 0) /\ nth n (a1 : a2) = suc a <-> nth n (a1 : a2) = suc a) ->
(n = 0 /\ nth n (a1 : a2) = suc a \/ ~n = 0 /\ nth n (a1 : a2) = suc a <-> nth n (a1 : a2) = suc a) |
57 |
|
bian1 |
n = 0 \/ ~n = 0 -> ((n = 0 \/ ~n = 0) /\ nth n (a1 : a2) = suc a <-> nth n (a1 : a2) = suc a) |
58 |
|
em |
n = 0 \/ ~n = 0 |
59 |
57, 58 |
ax_mp |
(n = 0 \/ ~n = 0) /\ nth n (a1 : a2) = suc a <-> nth n (a1 : a2) = suc a |
60 |
56, 59 |
ax_mp |
n = 0 /\ nth n (a1 : a2) = suc a \/ ~n = 0 /\ nth n (a1 : a2) = suc a <-> nth n (a1 : a2) = suc a |
61 |
60 |
exeqi |
E. n (n = 0 /\ nth n (a1 : a2) = suc a \/ ~n = 0 /\ nth n (a1 : a2) = suc a) <-> E. n nth n (a1 : a2) = suc a |
62 |
53, 61 |
ax_mp |
E. n (n = 0 /\ nth n (a1 : a2) = suc a) \/ E. n (~n = 0 /\ nth n (a1 : a2) = suc a) <-> E. n nth n (a1 : a2) = suc a |
63 |
|
bicom |
(E. n (n = 0 /\ nth n (a1 : a2) = suc a) <-> a = a1) -> (a = a1 <-> E. n (n = 0 /\ nth n (a1 : a2) = suc a)) |
64 |
|
eqcomb |
a1 = a <-> a = a1 |
65 |
|
peano2 |
suc a1 = suc a <-> a1 = a |
66 |
|
nthZ |
nth 0 (a1 : a2) = suc a1 |
67 |
|
ntheq1 |
n = 0 -> nth n (a1 : a2) = nth 0 (a1 : a2) |
68 |
66, 67 |
syl6eq |
n = 0 -> nth n (a1 : a2) = suc a1 |
69 |
68 |
eqeq1d |
n = 0 -> (nth n (a1 : a2) = suc a <-> suc a1 = suc a) |
70 |
65, 69 |
syl6bb |
n = 0 -> (nth n (a1 : a2) = suc a <-> a1 = a) |
71 |
64, 70 |
syl6bb |
n = 0 -> (nth n (a1 : a2) = suc a <-> a = a1) |
72 |
71 |
exeqe |
E. n (n = 0 /\ nth n (a1 : a2) = suc a) <-> a = a1 |
73 |
63, 72 |
ax_mp |
a = a1 <-> E. n (n = 0 /\ nth n (a1 : a2) = suc a) |
74 |
73 |
a1i |
(a IN a2 <-> E. n nth n a2 = suc a) -> (a = a1 <-> E. n (n = 0 /\ nth n (a1 : a2) = suc a)) |
75 |
|
bi1 |
(a IN a2 <-> E. n nth n a2 = suc a <-> (a IN a2 <-> E. n (~n = 0 /\ nth n (a1 : a2) = suc a))) ->
(a IN a2 <-> E. n nth n a2 = suc a) ->
(a IN a2 <-> E. n (~n = 0 /\ nth n (a1 : a2) = suc a)) |
76 |
|
bieq2 |
(E. n nth n a2 = suc a <-> E. n (~n = 0 /\ nth n (a1 : a2) = suc a)) ->
(a IN a2 <-> E. n nth n a2 = suc a <-> (a IN a2 <-> E. n (~n = 0 /\ nth n (a1 : a2) = suc a))) |
77 |
|
bitr4 |
(E. n nth n a2 = suc a <-> E. a3 nth a3 a2 = suc a) ->
(E. n (~n = 0 /\ nth n (a1 : a2) = suc a) <-> E. a3 nth a3 a2 = suc a) ->
(E. n nth n a2 = suc a <-> E. n (~n = 0 /\ nth n (a1 : a2) = suc a)) |
78 |
|
ntheq1 |
n = a3 -> nth n a2 = nth a3 a2 |
79 |
78 |
eqeq1d |
n = a3 -> (nth n a2 = suc a <-> nth a3 a2 = suc a) |
80 |
79 |
cbvex |
E. n nth n a2 = suc a <-> E. a3 nth a3 a2 = suc a |
81 |
77, 80 |
ax_mp |
(E. n (~n = 0 /\ nth n (a1 : a2) = suc a) <-> E. a3 nth a3 a2 = suc a) -> (E. n nth n a2 = suc a <-> E. n (~n = 0 /\ nth n (a1 : a2) = suc a)) |
82 |
|
bitr |
(E. n (~n = 0 /\ nth n (a1 : a2) = suc a) <-> E. a3 E. n (n = suc a3 /\ nth n (a1 : a2) = suc a)) ->
(E. a3 E. n (n = suc a3 /\ nth n (a1 : a2) = suc a) <-> E. a3 nth a3 a2 = suc a) ->
(E. n (~n = 0 /\ nth n (a1 : a2) = suc a) <-> E. a3 nth a3 a2 = suc a) |
83 |
|
exsuc |
n != 0 <-> E. a3 n = suc a3 |
84 |
83 |
conv ne |
~n = 0 <-> E. a3 n = suc a3 |
85 |
84 |
a1i |
nth n (a1 : a2) = suc a -> (~n = 0 <-> E. a3 n = suc a3) |
86 |
85 |
biexan1a |
~n = 0 /\ nth n (a1 : a2) = suc a <-> E. a3 (n = suc a3 /\ nth n (a1 : a2) = suc a) |
87 |
86 |
biexexi |
E. n (~n = 0 /\ nth n (a1 : a2) = suc a) <-> E. a3 E. n (n = suc a3 /\ nth n (a1 : a2) = suc a) |
88 |
82, 87 |
ax_mp |
(E. a3 E. n (n = suc a3 /\ nth n (a1 : a2) = suc a) <-> E. a3 nth a3 a2 = suc a) -> (E. n (~n = 0 /\ nth n (a1 : a2) = suc a) <-> E. a3 nth a3 a2 = suc a) |
89 |
|
nthS |
nth (suc a3) (a1 : a2) = nth a3 a2 |
90 |
|
ntheq1 |
n = suc a3 -> nth n (a1 : a2) = nth (suc a3) (a1 : a2) |
91 |
89, 90 |
syl6eq |
n = suc a3 -> nth n (a1 : a2) = nth a3 a2 |
92 |
91 |
eqeq1d |
n = suc a3 -> (nth n (a1 : a2) = suc a <-> nth a3 a2 = suc a) |
93 |
92 |
exeqe |
E. n (n = suc a3 /\ nth n (a1 : a2) = suc a) <-> nth a3 a2 = suc a |
94 |
93 |
exeqi |
E. a3 E. n (n = suc a3 /\ nth n (a1 : a2) = suc a) <-> E. a3 nth a3 a2 = suc a |
95 |
88, 94 |
ax_mp |
E. n (~n = 0 /\ nth n (a1 : a2) = suc a) <-> E. a3 nth a3 a2 = suc a |
96 |
81, 95 |
ax_mp |
E. n nth n a2 = suc a <-> E. n (~n = 0 /\ nth n (a1 : a2) = suc a) |
97 |
76, 96 |
ax_mp |
a IN a2 <-> E. n nth n a2 = suc a <-> (a IN a2 <-> E. n (~n = 0 /\ nth n (a1 : a2) = suc a)) |
98 |
75, 97 |
ax_mp |
(a IN a2 <-> E. n nth n a2 = suc a) -> (a IN a2 <-> E. n (~n = 0 /\ nth n (a1 : a2) = suc a)) |
99 |
74, 98 |
oreqd |
(a IN a2 <-> E. n nth n a2 = suc a) -> (a = a1 \/ a IN a2 <-> E. n (n = 0 /\ nth n (a1 : a2) = suc a) \/ E. n (~n = 0 /\ nth n (a1 : a2) = suc a)) |
100 |
62, 99 |
syl6bb |
(a IN a2 <-> E. n nth n a2 = suc a) -> (a = a1 \/ a IN a2 <-> E. n nth n (a1 : a2) = suc a) |
101 |
50, 100 |
syl5bb |
(a IN a2 <-> E. n nth n a2 = suc a) -> (a IN a1 : a2 <-> E. n nth n (a1 : a2) = suc a) |
102 |
9, 18, 27, 36, 49, 101 |
listind |
a IN l <-> E. n nth n l = suc a |