all2nex - ../examples/peano.mm1

Step	Hyp	Ref	Expression
1		bitr	(l1, l2 e. all2 (Compl R) <-> len l1 = len l2 /\ A. a1 A. a2 A. a3 (nth a1 l1 = suc a2 -> nth a1 l2 = suc a3 -> a2, a3 e. Compl R)) -> (len l1 = len l2 /\ A. a1 A. a2 A. a3 (nth a1 l1 = suc a2 -> nth a1 l2 = suc a3 -> a2, a3 e. Compl R) <-> len l1 = len l2 /\ ~l1, l2 e. ex2 R) -> (l1, l2 e. all2 (Compl R) <-> len l1 = len l2 /\ ~l1, l2 e. ex2 R)
2		elall2	l1, l2 e. all2 (Compl R) <-> len l1 = len l2 /\ A. a1 A. a2 A. a3 (nth a1 l1 = suc a2 -> nth a1 l2 = suc a3 -> a2, a3 e. Compl R)
3	1, 2	ax_mp	(len l1 = len l2 /\ A. a1 A. a2 A. a3 (nth a1 l1 = suc a2 -> nth a1 l2 = suc a3 -> a2, a3 e. Compl R) <-> len l1 = len l2 /\ ~l1, l2 e. ex2 R) -> (l1, l2 e. all2 (Compl R) <-> len l1 = len l2 /\ ~l1, l2 e. ex2 R)
4		aneq2a	(len l1 = len l2 -> (A. a1 A. a2 A. a3 (nth a1 l1 = suc a2 -> nth a1 l2 = suc a3 -> a2, a3 e. Compl R) <-> ~l1, l2 e. ex2 R)) -> (len l1 = len l2 /\ A. a1 A. a2 A. a3 (nth a1 l1 = suc a2 -> nth a1 l2 = suc a3 -> a2, a3 e. Compl R) <-> len l1 = len l2 /\ ~l1, l2 e. ex2 R)
5		bitr3	(A. a1 ~E. a2 E. a3 (nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 /\ a2, a3 e. R) <-> ~E. a1 E. a2 E. a3 (nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 /\ a2, a3 e. R)) -> (A. a1 ~E. a2 E. a3 (nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 /\ a2, a3 e. R) <-> A. a1 A. a2 A. a3 (nth a1 l1 = suc a2 -> nth a1 l2 = suc a3 -> a2, a3 e. Compl R)) -> (~E. a1 E. a2 E. a3 (nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 /\ a2, a3 e. R) <-> A. a1 A. a2 A. a3 (nth a1 l1 = suc a2 -> nth a1 l2 = suc a3 -> a2, a3 e. Compl R))
6		alnex	A. a1 ~E. a2 E. a3 (nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 /\ a2, a3 e. R) <-> ~E. a1 E. a2 E. a3 (nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 /\ a2, a3 e. R)
7	5, 6	ax_mp	(A. a1 ~E. a2 E. a3 (nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 /\ a2, a3 e. R) <-> A. a1 A. a2 A. a3 (nth a1 l1 = suc a2 -> nth a1 l2 = suc a3 -> a2, a3 e. Compl R)) -> (~E. a1 E. a2 E. a3 (nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 /\ a2, a3 e. R) <-> A. a1 A. a2 A. a3 (nth a1 l1 = suc a2 -> nth a1 l2 = suc a3 -> a2, a3 e. Compl R))
8		bitr3	(A. a2 ~E. a3 (nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 /\ a2, a3 e. R) <-> ~E. a2 E. a3 (nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 /\ a2, a3 e. R)) -> (A. a2 ~E. a3 (nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 /\ a2, a3 e. R) <-> A. a2 A. a3 (nth a1 l1 = suc a2 -> nth a1 l2 = suc a3 -> a2, a3 e. Compl R)) -> (~E. a2 E. a3 (nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 /\ a2, a3 e. R) <-> A. a2 A. a3 (nth a1 l1 = suc a2 -> nth a1 l2 = suc a3 -> a2, a3 e. Compl R))
9		alnex	A. a2 ~E. a3 (nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 /\ a2, a3 e. R) <-> ~E. a2 E. a3 (nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 /\ a2, a3 e. R)
10	8, 9	ax_mp	(A. a2 ~E. a3 (nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 /\ a2, a3 e. R) <-> A. a2 A. a3 (nth a1 l1 = suc a2 -> nth a1 l2 = suc a3 -> a2, a3 e. Compl R)) -> (~E. a2 E. a3 (nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 /\ a2, a3 e. R) <-> A. a2 A. a3 (nth a1 l1 = suc a2 -> nth a1 l2 = suc a3 -> a2, a3 e. Compl R))
11		bitr3	(A. a3 ~(nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 /\ a2, a3 e. R) <-> ~E. a3 (nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 /\ a2, a3 e. R)) -> (A. a3 ~(nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 /\ a2, a3 e. R) <-> A. a3 (nth a1 l1 = suc a2 -> nth a1 l2 = suc a3 -> a2, a3 e. Compl R)) -> (~E. a3 (nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 /\ a2, a3 e. R) <-> A. a3 (nth a1 l1 = suc a2 -> nth a1 l2 = suc a3 -> a2, a3 e. Compl R))
12		alnex	A. a3 ~(nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 /\ a2, a3 e. R) <-> ~E. a3 (nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 /\ a2, a3 e. R)
13	11, 12	ax_mp	(A. a3 ~(nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 /\ a2, a3 e. R) <-> A. a3 (nth a1 l1 = suc a2 -> nth a1 l2 = suc a3 -> a2, a3 e. Compl R)) -> (~E. a3 (nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 /\ a2, a3 e. R) <-> A. a3 (nth a1 l1 = suc a2 -> nth a1 l2 = suc a3 -> a2, a3 e. Compl R))
14		bitr	(~(nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 /\ a2, a3 e. R) <-> nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 -> ~a2, a3 e. R) -> (nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 -> ~a2, a3 e. R <-> nth a1 l1 = suc a2 -> nth a1 l2 = suc a3 -> a2, a3 e. Compl R) -> (~(nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 /\ a2, a3 e. R) <-> nth a1 l1 = suc a2 -> nth a1 l2 = suc a3 -> a2, a3 e. Compl R)
15		notan2	~(nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 /\ a2, a3 e. R) <-> nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 -> ~a2, a3 e. R
16	14, 15	ax_mp	(nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 -> ~a2, a3 e. R <-> nth a1 l1 = suc a2 -> nth a1 l2 = suc a3 -> a2, a3 e. Compl R) -> (~(nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 /\ a2, a3 e. R) <-> nth a1 l1 = suc a2 -> nth a1 l2 = suc a3 -> a2, a3 e. Compl R)
17		bitr3	(nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 -> a2, a3 e. Compl R <-> nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 -> ~a2, a3 e. R) -> (nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 -> a2, a3 e. Compl R <-> nth a1 l1 = suc a2 -> nth a1 l2 = suc a3 -> a2, a3 e. Compl R) -> (nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 -> ~a2, a3 e. R <-> nth a1 l1 = suc a2 -> nth a1 l2 = suc a3 -> a2, a3 e. Compl R)
18		elcpl	a2, a3 e. Compl R <-> ~a2, a3 e. R
19	18	imeq2i	nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 -> a2, a3 e. Compl R <-> nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 -> ~a2, a3 e. R
20	17, 19	ax_mp	(nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 -> a2, a3 e. Compl R <-> nth a1 l1 = suc a2 -> nth a1 l2 = suc a3 -> a2, a3 e. Compl R) -> (nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 -> ~a2, a3 e. R <-> nth a1 l1 = suc a2 -> nth a1 l2 = suc a3 -> a2, a3 e. Compl R)
21		impexp	nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 -> a2, a3 e. Compl R <-> nth a1 l1 = suc a2 -> nth a1 l2 = suc a3 -> a2, a3 e. Compl R
22	20, 21	ax_mp	nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 -> ~a2, a3 e. R <-> nth a1 l1 = suc a2 -> nth a1 l2 = suc a3 -> a2, a3 e. Compl R
23	16, 22	ax_mp	~(nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 /\ a2, a3 e. R) <-> nth a1 l1 = suc a2 -> nth a1 l2 = suc a3 -> a2, a3 e. Compl R
24	23	aleqi	A. a3 ~(nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 /\ a2, a3 e. R) <-> A. a3 (nth a1 l1 = suc a2 -> nth a1 l2 = suc a3 -> a2, a3 e. Compl R)
25	13, 24	ax_mp	~E. a3 (nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 /\ a2, a3 e. R) <-> A. a3 (nth a1 l1 = suc a2 -> nth a1 l2 = suc a3 -> a2, a3 e. Compl R)
26	25	aleqi	A. a2 ~E. a3 (nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 /\ a2, a3 e. R) <-> A. a2 A. a3 (nth a1 l1 = suc a2 -> nth a1 l2 = suc a3 -> a2, a3 e. Compl R)
27	10, 26	ax_mp	~E. a2 E. a3 (nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 /\ a2, a3 e. R) <-> A. a2 A. a3 (nth a1 l1 = suc a2 -> nth a1 l2 = suc a3 -> a2, a3 e. Compl R)
28	27	aleqi	A. a1 ~E. a2 E. a3 (nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 /\ a2, a3 e. R) <-> A. a1 A. a2 A. a3 (nth a1 l1 = suc a2 -> nth a1 l2 = suc a3 -> a2, a3 e. Compl R)
29	7, 28	ax_mp	~E. a1 E. a2 E. a3 (nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 /\ a2, a3 e. R) <-> A. a1 A. a2 A. a3 (nth a1 l1 = suc a2 -> nth a1 l2 = suc a3 -> a2, a3 e. Compl R)
30		elex2	l1, l2 e. ex2 R <-> len l1 = len l2 /\ E. a1 E. a2 E. a3 (nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 /\ a2, a3 e. R)
31		bian1	len l1 = len l2 -> (len l1 = len l2 /\ E. a1 E. a2 E. a3 (nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 /\ a2, a3 e. R) <-> E. a1 E. a2 E. a3 (nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 /\ a2, a3 e. R))
32	30, 31	syl5bb	len l1 = len l2 -> (l1, l2 e. ex2 R <-> E. a1 E. a2 E. a3 (nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 /\ a2, a3 e. R))
33	32	bicomd	len l1 = len l2 -> (E. a1 E. a2 E. a3 (nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 /\ a2, a3 e. R) <-> l1, l2 e. ex2 R)
34	33	noteqd	len l1 = len l2 -> (~E. a1 E. a2 E. a3 (nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 /\ a2, a3 e. R) <-> ~l1, l2 e. ex2 R)
35	29, 34	syl5bbr	len l1 = len l2 -> (A. a1 A. a2 A. a3 (nth a1 l1 = suc a2 -> nth a1 l2 = suc a3 -> a2, a3 e. Compl R) <-> ~l1, l2 e. ex2 R)
36	4, 35	ax_mp	len l1 = len l2 /\ A. a1 A. a2 A. a3 (nth a1 l1 = suc a2 -> nth a1 l2 = suc a3 -> a2, a3 e. Compl R) <-> len l1 = len l2 /\ ~l1, l2 e. ex2 R
37	3, 36	ax_mp	l1, l2 e. all2 (Compl R) <-> len l1 = len l2 /\ ~l1, l2 e. ex2 R

1

(l1, l2 e. all2 (Compl R) <-> len l1 = len l2 /\ A. a1 A. a2 A. a3 (nth a1 l1 = suc a2 -> nth a1 l2 = suc a3 -> a2, a3 e. Compl R)) ->
  (len l1 = len l2 /\ A. a1 A. a2 A. a3 (nth a1 l1 = suc a2 -> nth a1 l2 = suc a3 -> a2, a3 e. Compl R) <-> len l1 = len l2 /\ ~l1, l2 e. ex2 R) ->
  (l1, l2 e. all2 (Compl R) <-> len l1 = len l2 /\ ~l1, l2 e. ex2 R)

2

elall2

l1, l2 e. all2 (Compl R) <-> len l1 = len l2 /\ A. a1 A. a2 A. a3 (nth a1 l1 = suc a2 -> nth a1 l2 = suc a3 -> a2, a3 e. Compl R)

3

1, 2

ax_mp

(len l1 = len l2 /\ A. a1 A. a2 A. a3 (nth a1 l1 = suc a2 -> nth a1 l2 = suc a3 -> a2, a3 e. Compl R) <-> len l1 = len l2 /\ ~l1, l2 e. ex2 R) ->
  (l1, l2 e. all2 (Compl R) <-> len l1 = len l2 /\ ~l1, l2 e. ex2 R)

4

aneq2a

(len l1 = len l2 -> (A. a1 A. a2 A. a3 (nth a1 l1 = suc a2 -> nth a1 l2 = suc a3 -> a2, a3 e. Compl R) <-> ~l1, l2 e. ex2 R)) ->
  (len l1 = len l2 /\ A. a1 A. a2 A. a3 (nth a1 l1 = suc a2 -> nth a1 l2 = suc a3 -> a2, a3 e. Compl R) <-> len l1 = len l2 /\ ~l1, l2 e. ex2 R)

5

bitr3

(A. a1 ~E. a2 E. a3 (nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 /\ a2, a3 e. R) <-> ~E. a1 E. a2 E. a3 (nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 /\ a2, a3 e. R))
  ->
  (A. a1 ~E. a2 E. a3 (nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 /\ a2, a3 e. R) <->
    A. a1 A. a2 A. a3 (nth a1 l1 = suc a2 -> nth a1 l2 = suc a3 -> a2, a3 e. Compl R)) ->
  (~E. a1 E. a2 E. a3 (nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 /\ a2, a3 e. R) <->
    A. a1 A. a2 A. a3 (nth a1 l1 = suc a2 -> nth a1 l2 = suc a3 -> a2, a3 e. Compl R))

6

alnex

A. a1 ~E. a2 E. a3 (nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 /\ a2, a3 e. R) <-> ~E. a1 E. a2 E. a3 (nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 /\ a2, a3 e. R)

7

5, 6

ax_mp

(A. a1 ~E. a2 E. a3 (nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 /\ a2, a3 e. R) <->
    A. a1 A. a2 A. a3 (nth a1 l1 = suc a2 -> nth a1 l2 = suc a3 -> a2, a3 e. Compl R)) ->
  (~E. a1 E. a2 E. a3 (nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 /\ a2, a3 e. R) <->
    A. a1 A. a2 A. a3 (nth a1 l1 = suc a2 -> nth a1 l2 = suc a3 -> a2, a3 e. Compl R))

8

bitr3

(A. a2 ~E. a3 (nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 /\ a2, a3 e. R) <-> ~E. a2 E. a3 (nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 /\ a2, a3 e. R)) ->
  (A. a2 ~E. a3 (nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 /\ a2, a3 e. R) <-> A. a2 A. a3 (nth a1 l1 = suc a2 -> nth a1 l2 = suc a3 -> a2, a3 e. Compl R)) ->
  (~E. a2 E. a3 (nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 /\ a2, a3 e. R) <-> A. a2 A. a3 (nth a1 l1 = suc a2 -> nth a1 l2 = suc a3 -> a2, a3 e. Compl R))

9

alnex

A. a2 ~E. a3 (nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 /\ a2, a3 e. R) <-> ~E. a2 E. a3 (nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 /\ a2, a3 e. R)

10

8, 9

ax_mp

(A. a2 ~E. a3 (nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 /\ a2, a3 e. R) <-> A. a2 A. a3 (nth a1 l1 = suc a2 -> nth a1 l2 = suc a3 -> a2, a3 e. Compl R)) ->
  (~E. a2 E. a3 (nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 /\ a2, a3 e. R) <-> A. a2 A. a3 (nth a1 l1 = suc a2 -> nth a1 l2 = suc a3 -> a2, a3 e. Compl R))

11

bitr3

(A. a3 ~(nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 /\ a2, a3 e. R) <-> ~E. a3 (nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 /\ a2, a3 e. R)) ->
  (A. a3 ~(nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 /\ a2, a3 e. R) <-> A. a3 (nth a1 l1 = suc a2 -> nth a1 l2 = suc a3 -> a2, a3 e. Compl R)) ->
  (~E. a3 (nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 /\ a2, a3 e. R) <-> A. a3 (nth a1 l1 = suc a2 -> nth a1 l2 = suc a3 -> a2, a3 e. Compl R))

12

alnex

A. a3 ~(nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 /\ a2, a3 e. R) <-> ~E. a3 (nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 /\ a2, a3 e. R)

13

11, 12

ax_mp

(A. a3 ~(nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 /\ a2, a3 e. R) <-> A. a3 (nth a1 l1 = suc a2 -> nth a1 l2 = suc a3 -> a2, a3 e. Compl R)) ->
  (~E. a3 (nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 /\ a2, a3 e. R) <-> A. a3 (nth a1 l1 = suc a2 -> nth a1 l2 = suc a3 -> a2, a3 e. Compl R))

14

bitr

(~(nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 /\ a2, a3 e. R) <-> nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 -> ~a2, a3 e. R) ->
  (nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 -> ~a2, a3 e. R <-> nth a1 l1 = suc a2 -> nth a1 l2 = suc a3 -> a2, a3 e. Compl R) ->
  (~(nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 /\ a2, a3 e. R) <-> nth a1 l1 = suc a2 -> nth a1 l2 = suc a3 -> a2, a3 e. Compl R)

15

notan2

~(nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 /\ a2, a3 e. R) <-> nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 -> ~a2, a3 e. R

16

14, 15

ax_mp

(nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 -> ~a2, a3 e. R <-> nth a1 l1 = suc a2 -> nth a1 l2 = suc a3 -> a2, a3 e. Compl R) ->
  (~(nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 /\ a2, a3 e. R) <-> nth a1 l1 = suc a2 -> nth a1 l2 = suc a3 -> a2, a3 e. Compl R)

17

bitr3

(nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 -> a2, a3 e. Compl R <-> nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 -> ~a2, a3 e. R) ->
  (nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 -> a2, a3 e. Compl R <-> nth a1 l1 = suc a2 -> nth a1 l2 = suc a3 -> a2, a3 e. Compl R) ->
  (nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 -> ~a2, a3 e. R <-> nth a1 l1 = suc a2 -> nth a1 l2 = suc a3 -> a2, a3 e. Compl R)

18

elcpl

a2, a3 e. Compl R <-> ~a2, a3 e. R

19

18

imeq2i

nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 -> a2, a3 e. Compl R <-> nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 -> ~a2, a3 e. R

20

17, 19

ax_mp

(nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 -> a2, a3 e. Compl R <-> nth a1 l1 = suc a2 -> nth a1 l2 = suc a3 -> a2, a3 e. Compl R) ->
  (nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 -> ~a2, a3 e. R <-> nth a1 l1 = suc a2 -> nth a1 l2 = suc a3 -> a2, a3 e. Compl R)

21

impexp

nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 -> a2, a3 e. Compl R <-> nth a1 l1 = suc a2 -> nth a1 l2 = suc a3 -> a2, a3 e. Compl R

22

20, 21

ax_mp

nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 -> ~a2, a3 e. R <-> nth a1 l1 = suc a2 -> nth a1 l2 = suc a3 -> a2, a3 e. Compl R

23

16, 22

ax_mp

~(nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 /\ a2, a3 e. R) <-> nth a1 l1 = suc a2 -> nth a1 l2 = suc a3 -> a2, a3 e. Compl R

24

23

aleqi

A. a3 ~(nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 /\ a2, a3 e. R) <-> A. a3 (nth a1 l1 = suc a2 -> nth a1 l2 = suc a3 -> a2, a3 e. Compl R)

25

13, 24

ax_mp

~E. a3 (nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 /\ a2, a3 e. R) <-> A. a3 (nth a1 l1 = suc a2 -> nth a1 l2 = suc a3 -> a2, a3 e. Compl R)

26

25

aleqi

A. a2 ~E. a3 (nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 /\ a2, a3 e. R) <-> A. a2 A. a3 (nth a1 l1 = suc a2 -> nth a1 l2 = suc a3 -> a2, a3 e. Compl R)

27

10, 26

ax_mp

~E. a2 E. a3 (nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 /\ a2, a3 e. R) <-> A. a2 A. a3 (nth a1 l1 = suc a2 -> nth a1 l2 = suc a3 -> a2, a3 e. Compl R)

28

27

aleqi

A. a1 ~E. a2 E. a3 (nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 /\ a2, a3 e. R) <->
  A. a1 A. a2 A. a3 (nth a1 l1 = suc a2 -> nth a1 l2 = suc a3 -> a2, a3 e. Compl R)

29

7, 28

ax_mp

~E. a1 E. a2 E. a3 (nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 /\ a2, a3 e. R) <->
  A. a1 A. a2 A. a3 (nth a1 l1 = suc a2 -> nth a1 l2 = suc a3 -> a2, a3 e. Compl R)

30

elex2

l1, l2 e. ex2 R <-> len l1 = len l2 /\ E. a1 E. a2 E. a3 (nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 /\ a2, a3 e. R)

31

bian1

len l1 = len l2 ->
  (len l1 = len l2 /\ E. a1 E. a2 E. a3 (nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 /\ a2, a3 e. R) <->
    E. a1 E. a2 E. a3 (nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 /\ a2, a3 e. R))

32

30, 31

syl5bb

len l1 = len l2 -> (l1, l2 e. ex2 R <-> E. a1 E. a2 E. a3 (nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 /\ a2, a3 e. R))

33

32

bicomd

len l1 = len l2 -> (E. a1 E. a2 E. a3 (nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 /\ a2, a3 e. R) <-> l1, l2 e. ex2 R)

34

33

noteqd

len l1 = len l2 -> (~E. a1 E. a2 E. a3 (nth a1 l1 = suc a2 /\ nth a1 l2 = suc a3 /\ a2, a3 e. R) <-> ~l1, l2 e. ex2 R)

35

29, 34

syl5bbr

len l1 = len l2 -> (A. a1 A. a2 A. a3 (nth a1 l1 = suc a2 -> nth a1 l2 = suc a3 -> a2, a3 e. Compl R) <-> ~l1, l2 e. ex2 R)

36

4, 35

ax_mp

len l1 = len l2 /\ A. a1 A. a2 A. a3 (nth a1 l1 = suc a2 -> nth a1 l2 = suc a3 -> a2, a3 e. Compl R) <-> len l1 = len l2 /\ ~l1, l2 e. ex2 R

37

3, 36

ax_mp

l1, l2 e. all2 (Compl R) <-> len l1 = len l2 /\ ~l1, l2 e. ex2 R

Theorem all2nex ≪ | index | src | ≫

Axiom use