Step | Hyp | Ref | Expression |
1 |
|
bitr4 |
(l1, l2 e. ex2 (cnv R) <-> len l1 = len l2 /\ E. a1 E. a3 (nth a1 l1 = suc a3 /\ E. a2 (nth a1 l2 = suc a2 /\ a3, a2 e. cnv R))) ->
(l2, l1 e. ex2 R <-> len l1 = len l2 /\ E. a1 E. a3 (nth a1 l1 = suc a3 /\ E. a2 (nth a1 l2 = suc a2 /\ a3, a2 e. cnv R))) ->
(l1, l2 e. ex2 (cnv R) <-> l2, l1 e. ex2 R) |
2 |
|
elex22 |
l1, l2 e. ex2 (cnv R) <-> len l1 = len l2 /\ E. a1 E. a3 (nth a1 l1 = suc a3 /\ E. a2 (nth a1 l2 = suc a2 /\ a3, a2 e. cnv R)) |
3 |
1, 2 |
ax_mp |
(l2, l1 e. ex2 R <-> len l1 = len l2 /\ E. a1 E. a3 (nth a1 l1 = suc a3 /\ E. a2 (nth a1 l2 = suc a2 /\ a3, a2 e. cnv R))) ->
(l1, l2 e. ex2 (cnv R) <-> l2, l1 e. ex2 R) |
4 |
|
bitr4 |
(l2, l1 e. ex2 R <-> len l2 = len l1 /\ E. a1 E. a2 (nth a1 l2 = suc a2 /\ E. a3 (nth a1 l1 = suc a3 /\ a2, a3 e. R))) ->
(len l1 = len l2 /\ E. a1 E. a3 (nth a1 l1 = suc a3 /\ E. a2 (nth a1 l2 = suc a2 /\ a3, a2 e. cnv R)) <->
len l2 = len l1 /\ E. a1 E. a2 (nth a1 l2 = suc a2 /\ E. a3 (nth a1 l1 = suc a3 /\ a2, a3 e. R))) ->
(l2, l1 e. ex2 R <-> len l1 = len l2 /\ E. a1 E. a3 (nth a1 l1 = suc a3 /\ E. a2 (nth a1 l2 = suc a2 /\ a3, a2 e. cnv R))) |
5 |
|
elex22 |
l2, l1 e. ex2 R <-> len l2 = len l1 /\ E. a1 E. a2 (nth a1 l2 = suc a2 /\ E. a3 (nth a1 l1 = suc a3 /\ a2, a3 e. R)) |
6 |
4, 5 |
ax_mp |
(len l1 = len l2 /\ E. a1 E. a3 (nth a1 l1 = suc a3 /\ E. a2 (nth a1 l2 = suc a2 /\ a3, a2 e. cnv R)) <->
len l2 = len l1 /\ E. a1 E. a2 (nth a1 l2 = suc a2 /\ E. a3 (nth a1 l1 = suc a3 /\ a2, a3 e. R))) ->
(l2, l1 e. ex2 R <-> len l1 = len l2 /\ E. a1 E. a3 (nth a1 l1 = suc a3 /\ E. a2 (nth a1 l2 = suc a2 /\ a3, a2 e. cnv R))) |
7 |
|
aneq |
(len l1 = len l2 <-> len l2 = len l1) ->
(E. a1 E. a3 (nth a1 l1 = suc a3 /\ E. a2 (nth a1 l2 = suc a2 /\ a3, a2 e. cnv R)) <->
E. a1 E. a2 (nth a1 l2 = suc a2 /\ E. a3 (nth a1 l1 = suc a3 /\ a2, a3 e. R))) ->
(len l1 = len l2 /\ E. a1 E. a3 (nth a1 l1 = suc a3 /\ E. a2 (nth a1 l2 = suc a2 /\ a3, a2 e. cnv R)) <->
len l2 = len l1 /\ E. a1 E. a2 (nth a1 l2 = suc a2 /\ E. a3 (nth a1 l1 = suc a3 /\ a2, a3 e. R))) |
8 |
|
eqcomb |
len l1 = len l2 <-> len l2 = len l1 |
9 |
7, 8 |
ax_mp |
(E. a1 E. a3 (nth a1 l1 = suc a3 /\ E. a2 (nth a1 l2 = suc a2 /\ a3, a2 e. cnv R)) <->
E. a1 E. a2 (nth a1 l2 = suc a2 /\ E. a3 (nth a1 l1 = suc a3 /\ a2, a3 e. R))) ->
(len l1 = len l2 /\ E. a1 E. a3 (nth a1 l1 = suc a3 /\ E. a2 (nth a1 l2 = suc a2 /\ a3, a2 e. cnv R)) <->
len l2 = len l1 /\ E. a1 E. a2 (nth a1 l2 = suc a2 /\ E. a3 (nth a1 l1 = suc a3 /\ a2, a3 e. R))) |
10 |
|
bitr |
(E. a3 (nth a1 l1 = suc a3 /\ E. a2 (nth a1 l2 = suc a2 /\ a3, a2 e. cnv R)) <-> E. a2 (nth a1 l2 = suc a2 /\ E. a3 (nth a1 l1 = suc a3 /\ a3, a2 e. cnv R))) ->
(E. a2 (nth a1 l2 = suc a2 /\ E. a3 (nth a1 l1 = suc a3 /\ a3, a2 e. cnv R)) <-> E. a2 (nth a1 l2 = suc a2 /\ E. a3 (nth a1 l1 = suc a3 /\ a2, a3 e. R))) ->
(E. a3 (nth a1 l1 = suc a3 /\ E. a2 (nth a1 l2 = suc a2 /\ a3, a2 e. cnv R)) <-> E. a2 (nth a1 l2 = suc a2 /\ E. a3 (nth a1 l1 = suc a3 /\ a2, a3 e. R))) |
11 |
|
rexcomb |
E. a3 (nth a1 l1 = suc a3 /\ E. a2 (nth a1 l2 = suc a2 /\ a3, a2 e. cnv R)) <-> E. a2 (nth a1 l2 = suc a2 /\ E. a3 (nth a1 l1 = suc a3 /\ a3, a2 e. cnv R)) |
12 |
10, 11 |
ax_mp |
(E. a2 (nth a1 l2 = suc a2 /\ E. a3 (nth a1 l1 = suc a3 /\ a3, a2 e. cnv R)) <-> E. a2 (nth a1 l2 = suc a2 /\ E. a3 (nth a1 l1 = suc a3 /\ a2, a3 e. R))) ->
(E. a3 (nth a1 l1 = suc a3 /\ E. a2 (nth a1 l2 = suc a2 /\ a3, a2 e. cnv R)) <-> E. a2 (nth a1 l2 = suc a2 /\ E. a3 (nth a1 l1 = suc a3 /\ a2, a3 e. R))) |
13 |
|
prcnv |
a3, a2 e. cnv R <-> a2, a3 e. R |
14 |
13 |
rexeqi |
E. a3 (nth a1 l1 = suc a3 /\ a3, a2 e. cnv R) <-> E. a3 (nth a1 l1 = suc a3 /\ a2, a3 e. R) |
15 |
14 |
rexeqi |
E. a2 (nth a1 l2 = suc a2 /\ E. a3 (nth a1 l1 = suc a3 /\ a3, a2 e. cnv R)) <-> E. a2 (nth a1 l2 = suc a2 /\ E. a3 (nth a1 l1 = suc a3 /\ a2, a3 e. R)) |
16 |
12, 15 |
ax_mp |
E. a3 (nth a1 l1 = suc a3 /\ E. a2 (nth a1 l2 = suc a2 /\ a3, a2 e. cnv R)) <-> E. a2 (nth a1 l2 = suc a2 /\ E. a3 (nth a1 l1 = suc a3 /\ a2, a3 e. R)) |
17 |
16 |
exeqi |
E. a1 E. a3 (nth a1 l1 = suc a3 /\ E. a2 (nth a1 l2 = suc a2 /\ a3, a2 e. cnv R)) <->
E. a1 E. a2 (nth a1 l2 = suc a2 /\ E. a3 (nth a1 l1 = suc a3 /\ a2, a3 e. R)) |
18 |
9, 17 |
ax_mp |
len l1 = len l2 /\ E. a1 E. a3 (nth a1 l1 = suc a3 /\ E. a2 (nth a1 l2 = suc a2 /\ a3, a2 e. cnv R)) <->
len l2 = len l1 /\ E. a1 E. a2 (nth a1 l2 = suc a2 /\ E. a3 (nth a1 l1 = suc a3 /\ a2, a3 e. R)) |
19 |
6, 18 |
ax_mp |
l2, l1 e. ex2 R <-> len l1 = len l2 /\ E. a1 E. a3 (nth a1 l1 = suc a3 /\ E. a2 (nth a1 l2 = suc a2 /\ a3, a2 e. cnv R)) |
20 |
3, 19 |
ax_mp |
l1, l2 e. ex2 (cnv R) <-> l2, l1 e. ex2 R |