Theorem exsnoc ≪ | index | src | ≫ 

theorem exsnoc {a: nat} (l: nat) {l2: nat}:
  $ l != 0 <-> E. l2 E. a l = l2 |> a $;
StepHypRefExpression
1 bitr3 
(~rev l = 0 <-> l != 0) -> (~rev l = 0 <-> E. l2 E. a l = l2 |> a) -> (l != 0 <-> E. l2 E. a l = l2 |> a)
2 noteq 
(rev l = 0 <-> l = 0) -> (~rev l = 0 <-> ~l = 0)
3 2 conv ne 
(rev l = 0 <-> l = 0) -> (~rev l = 0 <-> l != 0)
4 reveq0 
rev l = 0 <-> l = 0
5 3, 4 ax_mp 
~rev l = 0 <-> l != 0
6 1, 5 ax_mp 
(~rev l = 0 <-> E. l2 E. a l = l2 |> a) -> (l != 0 <-> E. l2 E. a l = l2 |> a)
7 bitr 
(~rev l = 0 <-> E. a E. a1 rev l = a : a1) -> (E. a E. a1 rev l = a : a1 <-> E. l2 E. a l = l2 |> a) -> (~rev l = 0 <-> E. l2 E. a l = l2 |> a)
8 excons 
rev l != 0 <-> E. a E. a1 rev l = a : a1
9 8 conv ne 
~rev l = 0 <-> E. a E. a1 rev l = a : a1
10 7, 9 ax_mp 
(E. a E. a1 rev l = a : a1 <-> E. l2 E. a l = l2 |> a) -> (~rev l = 0 <-> E. l2 E. a l = l2 |> a)
11 bitr 
(E. a1 rev l = a : a1 <-> E. a1 l = rev a1 |> a) -> (E. a1 l = rev a1 |> a <-> E. l2 l = l2 |> a) -> (E. a1 rev l = a : a1 <-> E. l2 l = l2 |> a)
12 bitr 
(rev l = a : a1 <-> rev l = rev (rev a1 |> a)) -> (rev l = rev (rev a1 |> a) <-> l = rev a1 |> a) -> (rev l = a : a1 <-> l = rev a1 |> a)
13 eqeq2 
a : a1 = rev (rev a1 |> a) -> (rev l = a : a1 <-> rev l = rev (rev a1 |> a))
14 eqtr3 
rev (rev (a : a1)) = a : a1 -> rev (rev (a : a1)) = rev (rev a1 |> a) -> a : a1 = rev (rev a1 |> a)
15 revrev 
rev (rev (a : a1)) = a : a1
16 14, 15 ax_mp 
rev (rev (a : a1)) = rev (rev a1 |> a) -> a : a1 = rev (rev a1 |> a)
17 reveq 
rev (a : a1) = rev a1 |> a -> rev (rev (a : a1)) = rev (rev a1 |> a)
18 revS 
rev (a : a1) = rev a1 |> a
19 17, 18 ax_mp 
rev (rev (a : a1)) = rev (rev a1 |> a)
20 16, 19 ax_mp 
a : a1 = rev (rev a1 |> a)
21 13, 20 ax_mp 
rev l = a : a1 <-> rev l = rev (rev a1 |> a)
22 12, 21 ax_mp 
(rev l = rev (rev a1 |> a) <-> l = rev a1 |> a) -> (rev l = a : a1 <-> l = rev a1 |> a)
23 revinj 
rev l = rev (rev a1 |> a) <-> l = rev a1 |> a
24 22, 23 ax_mp 
rev l = a : a1 <-> l = rev a1 |> a
25 24 exeqi 
E. a1 rev l = a : a1 <-> E. a1 l = rev a1 |> a
26 11, 25 ax_mp 
(E. a1 l = rev a1 |> a <-> E. l2 l = l2 |> a) -> (E. a1 rev l = a : a1 <-> E. l2 l = l2 |> a)
27 snoceq1 
l2 = rev a1 -> l2 |> a = rev a1 |> a
28 27 eqeq2d 
l2 = rev a1 -> (l = l2 |> a <-> l = rev a1 |> a)
29 28 iexe 
l = rev a1 |> a -> E. l2 l = l2 |> a
30 29 eex 
E. a1 l = rev a1 |> a -> E. l2 l = l2 |> a
31 revrev 
rev (rev l2) = l2
32 reveq 
a1 = rev l2 -> rev a1 = rev (rev l2)
33 31, 32 syl6eq 
a1 = rev l2 -> rev a1 = l2
34 33 snoceq1d 
a1 = rev l2 -> rev a1 |> a = l2 |> a
35 34 eqeq2d 
a1 = rev l2 -> (l = rev a1 |> a <-> l = l2 |> a)
36 35 iexe 
l = l2 |> a -> E. a1 l = rev a1 |> a
37 36 eex 
E. l2 l = l2 |> a -> E. a1 l = rev a1 |> a
38 30, 37 ibii 
E. a1 l = rev a1 |> a <-> E. l2 l = l2 |> a
39 26, 38 ax_mp 
E. a1 rev l = a : a1 <-> E. l2 l = l2 |> a
40 39 biexexi 
E. a E. a1 rev l = a : a1 <-> E. l2 E. a l = l2 |> a
41 10, 40 ax_mp 
~rev l = 0 <-> E. l2 E. a l = l2 |> a
42 6, 41 ax_mp 
l != 0 <-> E. l2 E. a l = l2 |> a

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)