Theorem all2snoc1 ≪ | index | src | ≫ 

theorem all2snoc1 (R: set) (a: nat) {b: nat} (l1 l2: nat) {l2_: nat}:
  $ l1 |> a, l2 e. all2 R <->
    E. l2_ E. b (l2 = l2_ |> b /\ (a, b e. R /\ l1, l2_ e. all2 R)) $;
StepHypRefExpression
1 bitr3 
(rev (l1 |> a), rev l2 e. all2 R <-> l1 |> a, l2 e. all2 R) ->
  (rev (l1 |> a), rev l2 e. all2 R <-> E. l2_ E. b (l2 = l2_ |> b /\ (a, b e. R /\ l1, l2_ e. all2 R))) ->
  (l1 |> a, l2 e. all2 R <-> E. l2_ E. b (l2 = l2_ |> b /\ (a, b e. R /\ l1, l2_ e. all2 R)))
2 all2rev 
rev (l1 |> a), rev l2 e. all2 R <-> l1 |> a, l2 e. all2 R
3 1, 2 ax_mp 
(rev (l1 |> a), rev l2 e. all2 R <-> E. l2_ E. b (l2 = l2_ |> b /\ (a, b e. R /\ l1, l2_ e. all2 R))) ->
  (l1 |> a, l2 e. all2 R <-> E. l2_ E. b (l2 = l2_ |> b /\ (a, b e. R /\ l1, l2_ e. all2 R)))
4 bitr 
(rev (l1 |> a), rev l2 e. all2 R <-> a : rev l1, rev l2 e. all2 R) ->
  (a : rev l1, rev l2 e. all2 R <-> E. l2_ E. b (l2 = l2_ |> b /\ (a, b e. R /\ l1, l2_ e. all2 R))) ->
  (rev (l1 |> a), rev l2 e. all2 R <-> E. l2_ E. b (l2 = l2_ |> b /\ (a, b e. R /\ l1, l2_ e. all2 R)))
5 eleq1 
rev (l1 |> a), rev l2 = a : rev l1, rev l2 -> (rev (l1 |> a), rev l2 e. all2 R <-> a : rev l1, rev l2 e. all2 R)
6 preq1 
rev (l1 |> a) = a : rev l1 -> rev (l1 |> a), rev l2 = a : rev l1, rev l2
7 revsnoc 
rev (l1 |> a) = a : rev l1
8 6, 7 ax_mp 
rev (l1 |> a), rev l2 = a : rev l1, rev l2
9 5, 8 ax_mp 
rev (l1 |> a), rev l2 e. all2 R <-> a : rev l1, rev l2 e. all2 R
10 4, 9 ax_mp 
(a : rev l1, rev l2 e. all2 R <-> E. l2_ E. b (l2 = l2_ |> b /\ (a, b e. R /\ l1, l2_ e. all2 R))) ->
  (rev (l1 |> a), rev l2 e. all2 R <-> E. l2_ E. b (l2 = l2_ |> b /\ (a, b e. R /\ l1, l2_ e. all2 R)))
11 bitr 
(a : rev l1, rev l2 e. all2 R <-> E. b E. _1 (rev l2 = b : _1 /\ (a, b e. R /\ rev l1, _1 e. all2 R))) ->
  (E. b E. _1 (rev l2 = b : _1 /\ (a, b e. R /\ rev l1, _1 e. all2 R)) <-> E. l2_ E. b (l2 = l2_ |> b /\ (a, b e. R /\ l1, l2_ e. all2 R))) ->
  (a : rev l1, rev l2 e. all2 R <-> E. l2_ E. b (l2 = l2_ |> b /\ (a, b e. R /\ l1, l2_ e. all2 R)))
12 all2S1 
a : rev l1, rev l2 e. all2 R <-> E. b E. _1 (rev l2 = b : _1 /\ (a, b e. R /\ rev l1, _1 e. all2 R))
13 11, 12 ax_mp 
(E. b E. _1 (rev l2 = b : _1 /\ (a, b e. R /\ rev l1, _1 e. all2 R)) <-> E. l2_ E. b (l2 = l2_ |> b /\ (a, b e. R /\ l1, l2_ e. all2 R))) ->
  (a : rev l1, rev l2 e. all2 R <-> E. l2_ E. b (l2 = l2_ |> b /\ (a, b e. R /\ l1, l2_ e. all2 R)))
14 bitr 
(E. _1 (rev l2 = b : _1 /\ (a, b e. R /\ rev l1, _1 e. all2 R)) <-> E. l2_ (l2 = l2_ |> b /\ (a, b e. R /\ rev l1, rev l2_ e. all2 R))) ->
  (E. l2_ (l2 = l2_ |> b /\ (a, b e. R /\ rev l1, rev l2_ e. all2 R)) <-> E. l2_ (l2 = l2_ |> b /\ (a, b e. R /\ l1, l2_ e. all2 R))) ->
  (E. _1 (rev l2 = b : _1 /\ (a, b e. R /\ rev l1, _1 e. all2 R)) <-> E. l2_ (l2 = l2_ |> b /\ (a, b e. R /\ l1, l2_ e. all2 R)))
15 aneq 
(l2 = rev _1 |> b <-> rev l2 = b : _1) ->
  (a, b e. R /\ rev l1, rev (rev _1) e. all2 R <-> a, b e. R /\ rev l1, _1 e. all2 R) ->
  (l2 = rev _1 |> b /\ (a, b e. R /\ rev l1, rev (rev _1) e. all2 R) <-> rev l2 = b : _1 /\ (a, b e. R /\ rev l1, _1 e. all2 R))
16 bitr3 
(rev l2 = rev (rev _1 |> b) <-> l2 = rev _1 |> b) -> (rev l2 = rev (rev _1 |> b) <-> rev l2 = b : _1) -> (l2 = rev _1 |> b <-> rev l2 = b : _1)
17 revinj 
rev l2 = rev (rev _1 |> b) <-> l2 = rev _1 |> b
18 16, 17 ax_mp 
(rev l2 = rev (rev _1 |> b) <-> rev l2 = b : _1) -> (l2 = rev _1 |> b <-> rev l2 = b : _1)
19 eqeq2 
rev (rev _1 |> b) = b : _1 -> (rev l2 = rev (rev _1 |> b) <-> rev l2 = b : _1)
20 eqtr3 
rev (rev (b : _1)) = rev (rev _1 |> b) -> rev (rev (b : _1)) = b : _1 -> rev (rev _1 |> b) = b : _1
21 reveq 
rev (b : _1) = rev _1 |> b -> rev (rev (b : _1)) = rev (rev _1 |> b)
22 revS 
rev (b : _1) = rev _1 |> b
23 21, 22 ax_mp 
rev (rev (b : _1)) = rev (rev _1 |> b)
24 20, 23 ax_mp 
rev (rev (b : _1)) = b : _1 -> rev (rev _1 |> b) = b : _1
25 revrev 
rev (rev (b : _1)) = b : _1
26 24, 25 ax_mp 
rev (rev _1 |> b) = b : _1
27 19, 26 ax_mp 
rev l2 = rev (rev _1 |> b) <-> rev l2 = b : _1
28 18, 27 ax_mp 
l2 = rev _1 |> b <-> rev l2 = b : _1
29 15, 28 ax_mp 
(a, b e. R /\ rev l1, rev (rev _1) e. all2 R <-> a, b e. R /\ rev l1, _1 e. all2 R) ->
  (l2 = rev _1 |> b /\ (a, b e. R /\ rev l1, rev (rev _1) e. all2 R) <-> rev l2 = b : _1 /\ (a, b e. R /\ rev l1, _1 e. all2 R))
30 eleq1 
rev l1, rev (rev _1) = rev l1, _1 -> (rev l1, rev (rev _1) e. all2 R <-> rev l1, _1 e. all2 R)
31 preq2 
rev (rev _1) = _1 -> rev l1, rev (rev _1) = rev l1, _1
32 revrev 
rev (rev _1) = _1
33 31, 32 ax_mp 
rev l1, rev (rev _1) = rev l1, _1
34 30, 33 ax_mp 
rev l1, rev (rev _1) e. all2 R <-> rev l1, _1 e. all2 R
35 34 aneq2i 
a, b e. R /\ rev l1, rev (rev _1) e. all2 R <-> a, b e. R /\ rev l1, _1 e. all2 R
36 29, 35 ax_mp 
l2 = rev _1 |> b /\ (a, b e. R /\ rev l1, rev (rev _1) e. all2 R) <-> rev l2 = b : _1 /\ (a, b e. R /\ rev l1, _1 e. all2 R)
37 id 
l2_ = rev _1 -> l2_ = rev _1
38 37 snoceq1d 
l2_ = rev _1 -> l2_ |> b = rev _1 |> b
39 38 eqeq2d 
l2_ = rev _1 -> (l2 = l2_ |> b <-> l2 = rev _1 |> b)
40 37 reveqd 
l2_ = rev _1 -> rev l2_ = rev (rev _1)
41 40 preq2d 
l2_ = rev _1 -> rev l1, rev l2_ = rev l1, rev (rev _1)
42 41 eleq1d 
l2_ = rev _1 -> (rev l1, rev l2_ e. all2 R <-> rev l1, rev (rev _1) e. all2 R)
43 42 aneq2d 
l2_ = rev _1 -> (a, b e. R /\ rev l1, rev l2_ e. all2 R <-> a, b e. R /\ rev l1, rev (rev _1) e. all2 R)
44 39, 43 aneqd 
l2_ = rev _1 -> (l2 = l2_ |> b /\ (a, b e. R /\ rev l1, rev l2_ e. all2 R) <-> l2 = rev _1 |> b /\ (a, b e. R /\ rev l1, rev (rev _1) e. all2 R))
45 44 iexe 
l2 = rev _1 |> b /\ (a, b e. R /\ rev l1, rev (rev _1) e. all2 R) -> E. l2_ (l2 = l2_ |> b /\ (a, b e. R /\ rev l1, rev l2_ e. all2 R))
46 36, 45 sylbir 
rev l2 = b : _1 /\ (a, b e. R /\ rev l1, _1 e. all2 R) -> E. l2_ (l2 = l2_ |> b /\ (a, b e. R /\ rev l1, rev l2_ e. all2 R))
47 46 eex 
E. _1 (rev l2 = b : _1 /\ (a, b e. R /\ rev l1, _1 e. all2 R)) -> E. l2_ (l2 = l2_ |> b /\ (a, b e. R /\ rev l1, rev l2_ e. all2 R))
48 bitr3 
(rev l2 = rev (l2_ |> b) <-> rev l2 = b : rev l2_) -> (rev l2 = rev (l2_ |> b) <-> l2 = l2_ |> b) -> (rev l2 = b : rev l2_ <-> l2 = l2_ |> b)
49 eqeq2 
rev (l2_ |> b) = b : rev l2_ -> (rev l2 = rev (l2_ |> b) <-> rev l2 = b : rev l2_)
50 revsnoc 
rev (l2_ |> b) = b : rev l2_
51 49, 50 ax_mp 
rev l2 = rev (l2_ |> b) <-> rev l2 = b : rev l2_
52 48, 51 ax_mp 
(rev l2 = rev (l2_ |> b) <-> l2 = l2_ |> b) -> (rev l2 = b : rev l2_ <-> l2 = l2_ |> b)
53 revinj 
rev l2 = rev (l2_ |> b) <-> l2 = l2_ |> b
54 52, 53 ax_mp 
rev l2 = b : rev l2_ <-> l2 = l2_ |> b
55 54 aneq1i 
rev l2 = b : rev l2_ /\ (a, b e. R /\ rev l1, rev l2_ e. all2 R) <-> l2 = l2_ |> b /\ (a, b e. R /\ rev l1, rev l2_ e. all2 R)
56 id 
_1 = rev l2_ -> _1 = rev l2_
57 56 conseq2d 
_1 = rev l2_ -> b : _1 = b : rev l2_
58 57 eqeq2d 
_1 = rev l2_ -> (rev l2 = b : _1 <-> rev l2 = b : rev l2_)
59 56 preq2d 
_1 = rev l2_ -> rev l1, _1 = rev l1, rev l2_
60 59 eleq1d 
_1 = rev l2_ -> (rev l1, _1 e. all2 R <-> rev l1, rev l2_ e. all2 R)
61 60 aneq2d 
_1 = rev l2_ -> (a, b e. R /\ rev l1, _1 e. all2 R <-> a, b e. R /\ rev l1, rev l2_ e. all2 R)
62 58, 61 aneqd 
_1 = rev l2_ -> (rev l2 = b : _1 /\ (a, b e. R /\ rev l1, _1 e. all2 R) <-> rev l2 = b : rev l2_ /\ (a, b e. R /\ rev l1, rev l2_ e. all2 R))
63 62 iexe 
rev l2 = b : rev l2_ /\ (a, b e. R /\ rev l1, rev l2_ e. all2 R) -> E. _1 (rev l2 = b : _1 /\ (a, b e. R /\ rev l1, _1 e. all2 R))
64 55, 63 sylbir 
l2 = l2_ |> b /\ (a, b e. R /\ rev l1, rev l2_ e. all2 R) -> E. _1 (rev l2 = b : _1 /\ (a, b e. R /\ rev l1, _1 e. all2 R))
65 64 eex 
E. l2_ (l2 = l2_ |> b /\ (a, b e. R /\ rev l1, rev l2_ e. all2 R)) -> E. _1 (rev l2 = b : _1 /\ (a, b e. R /\ rev l1, _1 e. all2 R))
66 47, 65 ibii 
E. _1 (rev l2 = b : _1 /\ (a, b e. R /\ rev l1, _1 e. all2 R)) <-> E. l2_ (l2 = l2_ |> b /\ (a, b e. R /\ rev l1, rev l2_ e. all2 R))
67 14, 66 ax_mp 
(E. l2_ (l2 = l2_ |> b /\ (a, b e. R /\ rev l1, rev l2_ e. all2 R)) <-> E. l2_ (l2 = l2_ |> b /\ (a, b e. R /\ l1, l2_ e. all2 R))) ->
  (E. _1 (rev l2 = b : _1 /\ (a, b e. R /\ rev l1, _1 e. all2 R)) <-> E. l2_ (l2 = l2_ |> b /\ (a, b e. R /\ l1, l2_ e. all2 R)))
68 all2rev 
rev l1, rev l2_ e. all2 R <-> l1, l2_ e. all2 R
69 68 aneq2i 
a, b e. R /\ rev l1, rev l2_ e. all2 R <-> a, b e. R /\ l1, l2_ e. all2 R
70 69 aneq2i 
l2 = l2_ |> b /\ (a, b e. R /\ rev l1, rev l2_ e. all2 R) <-> l2 = l2_ |> b /\ (a, b e. R /\ l1, l2_ e. all2 R)
71 70 exeqi 
E. l2_ (l2 = l2_ |> b /\ (a, b e. R /\ rev l1, rev l2_ e. all2 R)) <-> E. l2_ (l2 = l2_ |> b /\ (a, b e. R /\ l1, l2_ e. all2 R))
72 67, 71 ax_mp 
E. _1 (rev l2 = b : _1 /\ (a, b e. R /\ rev l1, _1 e. all2 R)) <-> E. l2_ (l2 = l2_ |> b /\ (a, b e. R /\ l1, l2_ e. all2 R))
73 72 biexexi 
E. b E. _1 (rev l2 = b : _1 /\ (a, b e. R /\ rev l1, _1 e. all2 R)) <-> E. l2_ E. b (l2 = l2_ |> b /\ (a, b e. R /\ l1, l2_ e. all2 R))
74 13, 73 ax_mp 
a : rev l1, rev l2 e. all2 R <-> E. l2_ E. b (l2 = l2_ |> b /\ (a, b e. R /\ l1, l2_ e. all2 R))
75 10, 74 ax_mp 
rev (l1 |> a), rev l2 e. all2 R <-> E. l2_ E. b (l2 = l2_ |> b /\ (a, b e. R /\ l1, l2_ e. all2 R))
76 3, 75 ax_mp 
l1 |> a, l2 e. all2 R <-> E. l2_ E. b (l2 = l2_ |> b /\ (a, b e. R /\ l1, l2_ e. all2 R))

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp, itru), axs_pred_calc (ax_gen, ax_4, ax_5, ax_6, ax_7, ax_10, ax_11, ax_12), axs_set (elab, ax_8), axs_the (theid, the0), axs_peano (peano1, peano2, peano5, addeq, muleq, add0, addS, mul0, mulS)