Step | Hyp | Ref | Expression |
1 |
|
id |
_1 = l1 -> _1 = l1 |
2 |
1 |
anwl |
_1 = l1 /\ _2 = l2 -> _1 = l1 |
3 |
2 |
leneqd |
_1 = l1 /\ _2 = l2 -> len _1 = len l1 |
4 |
|
id |
_2 = l2 -> _2 = l2 |
5 |
4 |
anwr |
_1 = l1 /\ _2 = l2 -> _2 = l2 |
6 |
5 |
leneqd |
_1 = l1 /\ _2 = l2 -> len _2 = len l2 |
7 |
3, 6 |
eqeqd |
_1 = l1 /\ _2 = l2 -> (len _1 = len _2 <-> len l1 = len l2) |
8 |
|
eqidd |
_1 = l1 /\ _2 = l2 -> n = n |
9 |
8, 2 |
ntheqd |
_1 = l1 /\ _2 = l2 -> nth n _1 = nth n l1 |
10 |
|
eqidd |
_1 = l1 /\ _2 = l2 -> suc x = suc x |
11 |
9, 10 |
eqeqd |
_1 = l1 /\ _2 = l2 -> (nth n _1 = suc x <-> nth n l1 = suc x) |
12 |
8, 5 |
ntheqd |
_1 = l1 /\ _2 = l2 -> nth n _2 = nth n l2 |
13 |
|
eqidd |
_1 = l1 /\ _2 = l2 -> suc y = suc y |
14 |
12, 13 |
eqeqd |
_1 = l1 /\ _2 = l2 -> (nth n _2 = suc y <-> nth n l2 = suc y) |
15 |
|
biidd |
_1 = l1 /\ _2 = l2 -> (x, y e. R <-> x, y e. R) |
16 |
14, 15 |
imeqd |
_1 = l1 /\ _2 = l2 -> (nth n _2 = suc y -> x, y e. R <-> nth n l2 = suc y -> x, y e. R) |
17 |
11, 16 |
imeqd |
_1 = l1 /\ _2 = l2 -> (nth n _1 = suc x -> nth n _2 = suc y -> x, y e. R <-> nth n l1 = suc x -> nth n l2 = suc y -> x, y e. R) |
18 |
17 |
aleqd |
_1 = l1 /\ _2 = l2 -> (A. y (nth n _1 = suc x -> nth n _2 = suc y -> x, y e. R) <-> A. y (nth n l1 = suc x -> nth n l2 = suc y -> x, y e. R)) |
19 |
18 |
aleqd |
_1 = l1 /\ _2 = l2 -> (A. x A. y (nth n _1 = suc x -> nth n _2 = suc y -> x, y e. R) <-> A. x A. y (nth n l1 = suc x -> nth n l2 = suc y -> x, y e. R)) |
20 |
19 |
aleqd |
_1 = l1 /\ _2 = l2 ->
(A. n A. x A. y (nth n _1 = suc x -> nth n _2 = suc y -> x, y e. R) <-> A. n A. x A. y (nth n l1 = suc x -> nth n l2 = suc y -> x, y e. R)) |
21 |
7, 20 |
aneqd |
_1 = l1 /\ _2 = l2 ->
(len _1 = len _2 /\ A. n A. x A. y (nth n _1 = suc x -> nth n _2 = suc y -> x, y e. R) <->
len l1 = len l2 /\ A. n A. x A. y (nth n l1 = suc x -> nth n l2 = suc y -> x, y e. R)) |
22 |
21 |
elabed |
_1 = l1 ->
(l2 e. {_2 | len _1 = len _2 /\ A. n A. x A. y (nth n _1 = suc x -> nth n _2 = suc y -> x, y e. R)} <->
len l1 = len l2 /\ A. n A. x A. y (nth n l1 = suc x -> nth n l2 = suc y -> x, y e. R)) |
23 |
22 |
elsabe |
l1, l2 e. S\ _1, {_2 | len _1 = len _2 /\ A. n A. x A. y (nth n _1 = suc x -> nth n _2 = suc y -> x, y e. R)} <->
len l1 = len l2 /\ A. n A. x A. y (nth n l1 = suc x -> nth n l2 = suc y -> x, y e. R) |
24 |
23 |
conv all2 |
l1, l2 e. all2 R <-> len l1 = len l2 /\ A. n A. x A. y (nth n l1 = suc x -> nth n l2 = suc y -> x, y e. R) |