Step | Hyp | Ref | Expression |
1 |
|
bitr4 |
(l1, l2 e. all2 (cnv R) <-> len l1 = len l2 /\ A. a1 A. a3 (nth a1 l1 = suc a3 -> A. a2 (nth a1 l2 = suc a2 -> a3, a2 e. cnv R))) ->
(l2, l1 e. all2 R <-> len l1 = len l2 /\ A. a1 A. a3 (nth a1 l1 = suc a3 -> A. a2 (nth a1 l2 = suc a2 -> a3, a2 e. cnv R))) ->
(l1, l2 e. all2 (cnv R) <-> l2, l1 e. all2 R) |
2 |
|
elall22 |
l1, l2 e. all2 (cnv R) <-> len l1 = len l2 /\ A. a1 A. a3 (nth a1 l1 = suc a3 -> A. a2 (nth a1 l2 = suc a2 -> a3, a2 e. cnv R)) |
3 |
1, 2 |
ax_mp |
(l2, l1 e. all2 R <-> len l1 = len l2 /\ A. a1 A. a3 (nth a1 l1 = suc a3 -> A. a2 (nth a1 l2 = suc a2 -> a3, a2 e. cnv R))) ->
(l1, l2 e. all2 (cnv R) <-> l2, l1 e. all2 R) |
4 |
|
bitr4 |
(l2, l1 e. all2 R <-> len l2 = len l1 /\ A. a1 A. a2 (nth a1 l2 = suc a2 -> A. a3 (nth a1 l1 = suc a3 -> a2, a3 e. R))) ->
(len l1 = len l2 /\ A. a1 A. a3 (nth a1 l1 = suc a3 -> A. a2 (nth a1 l2 = suc a2 -> a3, a2 e. cnv R)) <->
len l2 = len l1 /\ A. a1 A. a2 (nth a1 l2 = suc a2 -> A. a3 (nth a1 l1 = suc a3 -> a2, a3 e. R))) ->
(l2, l1 e. all2 R <-> len l1 = len l2 /\ A. a1 A. a3 (nth a1 l1 = suc a3 -> A. a2 (nth a1 l2 = suc a2 -> a3, a2 e. cnv R))) |
5 |
|
elall22 |
l2, l1 e. all2 R <-> len l2 = len l1 /\ A. a1 A. a2 (nth a1 l2 = suc a2 -> A. a3 (nth a1 l1 = suc a3 -> a2, a3 e. R)) |
6 |
4, 5 |
ax_mp |
(len l1 = len l2 /\ A. a1 A. a3 (nth a1 l1 = suc a3 -> A. a2 (nth a1 l2 = suc a2 -> a3, a2 e. cnv R)) <->
len l2 = len l1 /\ A. a1 A. a2 (nth a1 l2 = suc a2 -> A. a3 (nth a1 l1 = suc a3 -> a2, a3 e. R))) ->
(l2, l1 e. all2 R <-> len l1 = len l2 /\ A. a1 A. a3 (nth a1 l1 = suc a3 -> A. a2 (nth a1 l2 = suc a2 -> a3, a2 e. cnv R))) |
7 |
|
aneq |
(len l1 = len l2 <-> len l2 = len l1) ->
(A. a1 A. a3 (nth a1 l1 = suc a3 -> A. a2 (nth a1 l2 = suc a2 -> a3, a2 e. cnv R)) <->
A. a1 A. a2 (nth a1 l2 = suc a2 -> A. a3 (nth a1 l1 = suc a3 -> a2, a3 e. R))) ->
(len l1 = len l2 /\ A. a1 A. a3 (nth a1 l1 = suc a3 -> A. a2 (nth a1 l2 = suc a2 -> a3, a2 e. cnv R)) <->
len l2 = len l1 /\ A. a1 A. a2 (nth a1 l2 = suc a2 -> A. 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 |
(A. a1 A. a3 (nth a1 l1 = suc a3 -> A. a2 (nth a1 l2 = suc a2 -> a3, a2 e. cnv R)) <->
A. a1 A. a2 (nth a1 l2 = suc a2 -> A. a3 (nth a1 l1 = suc a3 -> a2, a3 e. R))) ->
(len l1 = len l2 /\ A. a1 A. a3 (nth a1 l1 = suc a3 -> A. a2 (nth a1 l2 = suc a2 -> a3, a2 e. cnv R)) <->
len l2 = len l1 /\ A. a1 A. a2 (nth a1 l2 = suc a2 -> A. a3 (nth a1 l1 = suc a3 -> a2, a3 e. R))) |
10 |
|
bitr |
(A. a3 (nth a1 l1 = suc a3 -> A. a2 (nth a1 l2 = suc a2 -> a3, a2 e. cnv R)) <-> A. a2 (nth a1 l2 = suc a2 -> A. a3 (nth a1 l1 = suc a3 -> a3, a2 e. cnv R))) ->
(A. a2 (nth a1 l2 = suc a2 -> A. a3 (nth a1 l1 = suc a3 -> a3, a2 e. cnv R)) <-> A. a2 (nth a1 l2 = suc a2 -> A. a3 (nth a1 l1 = suc a3 -> a2, a3 e. R))) ->
(A. a3 (nth a1 l1 = suc a3 -> A. a2 (nth a1 l2 = suc a2 -> a3, a2 e. cnv R)) <-> A. a2 (nth a1 l2 = suc a2 -> A. a3 (nth a1 l1 = suc a3 -> a2, a3 e. R))) |
11 |
|
ralcomb |
A. a3 (nth a1 l1 = suc a3 -> A. a2 (nth a1 l2 = suc a2 -> a3, a2 e. cnv R)) <-> A. a2 (nth a1 l2 = suc a2 -> A. a3 (nth a1 l1 = suc a3 -> a3, a2 e. cnv R)) |
12 |
10, 11 |
ax_mp |
(A. a2 (nth a1 l2 = suc a2 -> A. a3 (nth a1 l1 = suc a3 -> a3, a2 e. cnv R)) <-> A. a2 (nth a1 l2 = suc a2 -> A. a3 (nth a1 l1 = suc a3 -> a2, a3 e. R))) ->
(A. a3 (nth a1 l1 = suc a3 -> A. a2 (nth a1 l2 = suc a2 -> a3, a2 e. cnv R)) <-> A. a2 (nth a1 l2 = suc a2 -> A. a3 (nth a1 l1 = suc a3 -> a2, a3 e. R))) |
13 |
|
prcnv |
a3, a2 e. cnv R <-> a2, a3 e. R |
14 |
13 |
raleqi |
A. a3 (nth a1 l1 = suc a3 -> a3, a2 e. cnv R) <-> A. a3 (nth a1 l1 = suc a3 -> a2, a3 e. R) |
15 |
14 |
raleqi |
A. a2 (nth a1 l2 = suc a2 -> A. a3 (nth a1 l1 = suc a3 -> a3, a2 e. cnv R)) <-> A. a2 (nth a1 l2 = suc a2 -> A. a3 (nth a1 l1 = suc a3 -> a2, a3 e. R)) |
16 |
12, 15 |
ax_mp |
A. a3 (nth a1 l1 = suc a3 -> A. a2 (nth a1 l2 = suc a2 -> a3, a2 e. cnv R)) <-> A. a2 (nth a1 l2 = suc a2 -> A. a3 (nth a1 l1 = suc a3 -> a2, a3 e. R)) |
17 |
16 |
aleqi |
A. a1 A. a3 (nth a1 l1 = suc a3 -> A. a2 (nth a1 l2 = suc a2 -> a3, a2 e. cnv R)) <->
A. a1 A. a2 (nth a1 l2 = suc a2 -> A. a3 (nth a1 l1 = suc a3 -> a2, a3 e. R)) |
18 |
9, 17 |
ax_mp |
len l1 = len l2 /\ A. a1 A. a3 (nth a1 l1 = suc a3 -> A. a2 (nth a1 l2 = suc a2 -> a3, a2 e. cnv R)) <->
len l2 = len l1 /\ A. a1 A. a2 (nth a1 l2 = suc a2 -> A. a3 (nth a1 l1 = suc a3 -> a2, a3 e. R)) |
19 |
6, 18 |
ax_mp |
l2, l1 e. all2 R <-> len l1 = len l2 /\ A. a1 A. a3 (nth a1 l1 = suc a3 -> A. a2 (nth a1 l2 = suc a2 -> a3, a2 e. cnv R)) |
20 |
3, 19 |
ax_mp |
l1, l2 e. all2 (cnv R) <-> l2, l1 e. all2 R |