Theorem dmsrecaux ≪ | index | src | ≫ 

theorem dmsrecaux (S: set) (n: nat): $ Dom (srecaux S n) == upto n $;
StepHypRefExpression
1 id 
x = n -> x = n
2 1 srecauxeq2d 
x = n -> srecaux S x = srecaux S n
3 2 nseqd 
x = n -> srecaux S x == srecaux S n
4 3 dmeqd 
x = n -> Dom (srecaux S x) == Dom (srecaux S n)
5 1 uptoeqd 
x = n -> upto x = upto n
6 5 nseqd 
x = n -> upto x == upto n
7 4, 6 eqseqd 
x = n -> (Dom (srecaux S x) == upto x <-> Dom (srecaux S n) == upto n)
8 id 
x = 0 -> x = 0
9 8 srecauxeq2d 
x = 0 -> srecaux S x = srecaux S 0
10 9 nseqd 
x = 0 -> srecaux S x == srecaux S 0
11 10 dmeqd 
x = 0 -> Dom (srecaux S x) == Dom (srecaux S 0)
12 8 uptoeqd 
x = 0 -> upto x = upto 0
13 12 nseqd 
x = 0 -> upto x == upto 0
14 11, 13 eqseqd 
x = 0 -> (Dom (srecaux S x) == upto x <-> Dom (srecaux S 0) == upto 0)
15 id 
x = y -> x = y
16 15 srecauxeq2d 
x = y -> srecaux S x = srecaux S y
17 16 nseqd 
x = y -> srecaux S x == srecaux S y
18 17 dmeqd 
x = y -> Dom (srecaux S x) == Dom (srecaux S y)
19 15 uptoeqd 
x = y -> upto x = upto y
20 19 nseqd 
x = y -> upto x == upto y
21 18, 20 eqseqd 
x = y -> (Dom (srecaux S x) == upto x <-> Dom (srecaux S y) == upto y)
22 id 
x = suc y -> x = suc y
23 22 srecauxeq2d 
x = suc y -> srecaux S x = srecaux S (suc y)
24 23 nseqd 
x = suc y -> srecaux S x == srecaux S (suc y)
25 24 dmeqd 
x = suc y -> Dom (srecaux S x) == Dom (srecaux S (suc y))
26 22 uptoeqd 
x = suc y -> upto x = upto (suc y)
27 26 nseqd 
x = suc y -> upto x == upto (suc y)
28 25, 27 eqseqd 
x = suc y -> (Dom (srecaux S x) == upto x <-> Dom (srecaux S (suc y)) == upto (suc y))
29 eqstr 
Dom (srecaux S 0) == Dom 0 -> Dom 0 == upto 0 -> Dom (srecaux S 0) == upto 0
30 dmeq 
srecaux S 0 == 0 -> Dom (srecaux S 0) == Dom 0
31 nseq 
srecaux S 0 = 0 -> srecaux S 0 == 0
32 srecaux0 
srecaux S 0 = 0
33 31, 32 ax_mp 
srecaux S 0 == 0
34 30, 33 ax_mp 
Dom (srecaux S 0) == Dom 0
35 29, 34 ax_mp 
Dom 0 == upto 0 -> Dom (srecaux S 0) == upto 0
36 eqstr4 
Dom 0 == 0 -> upto 0 == 0 -> Dom 0 == upto 0
37 dm0 
Dom 0 == 0
38 36, 37 ax_mp 
upto 0 == 0 -> Dom 0 == upto 0
39 nseq 
upto 0 = 0 -> upto 0 == 0
40 upto0 
upto 0 = 0
41 39, 40 ax_mp 
upto 0 == 0
42 38, 41 ax_mp 
Dom 0 == upto 0
43 35, 42 ax_mp 
Dom (srecaux S 0) == upto 0
44 eqstr 
Dom (srecaux S (suc y)) == Dom (write (srecaux S y) y (S @ srecaux S y)) ->
  Dom (write (srecaux S y) y (S @ srecaux S y)) == Dom (srecaux S y) u. sn y ->
  Dom (srecaux S (suc y)) == Dom (srecaux S y) u. sn y
45 dmeq 
srecaux S (suc y) == write (srecaux S y) y (S @ srecaux S y) -> Dom (srecaux S (suc y)) == Dom (write (srecaux S y) y (S @ srecaux S y))
46 srecauxS 
srecaux S (suc y) == write (srecaux S y) y (S @ srecaux S y)
47 45, 46 ax_mp 
Dom (srecaux S (suc y)) == Dom (write (srecaux S y) y (S @ srecaux S y))
48 44, 47 ax_mp 
Dom (write (srecaux S y) y (S @ srecaux S y)) == Dom (srecaux S y) u. sn y -> Dom (srecaux S (suc y)) == Dom (srecaux S y) u. sn y
49 dmwrite 
Dom (write (srecaux S y) y (S @ srecaux S y)) == Dom (srecaux S y) u. sn y
50 48, 49 ax_mp 
Dom (srecaux S (suc y)) == Dom (srecaux S y) u. sn y
51 bitr 
(z e. upto (suc y) <-> z < suc y) -> (z < suc y <-> z e. upto y u. sn y) -> (z e. upto (suc y) <-> z e. upto y u. sn y)
52 elupto 
z e. upto (suc y) <-> z < suc y
53 51, 52 ax_mp 
(z < suc y <-> z e. upto y u. sn y) -> (z e. upto (suc y) <-> z e. upto y u. sn y)
54 bitr3 
(z <= y <-> z < suc y) -> (z <= y <-> z e. upto y u. sn y) -> (z < suc y <-> z e. upto y u. sn y)
55 leltsuc 
z <= y <-> z < suc y
56 54, 55 ax_mp 
(z <= y <-> z e. upto y u. sn y) -> (z < suc y <-> z e. upto y u. sn y)
57 bitr4 
(z <= y <-> z < y \/ z = y) -> (z e. upto y u. sn y <-> z < y \/ z = y) -> (z <= y <-> z e. upto y u. sn y)
58 leloe 
z <= y <-> z < y \/ z = y
59 57, 58 ax_mp 
(z e. upto y u. sn y <-> z < y \/ z = y) -> (z <= y <-> z e. upto y u. sn y)
60 bitr 
(z e. upto y u. sn y <-> z e. upto y \/ z e. sn y) -> (z e. upto y \/ z e. sn y <-> z < y \/ z = y) -> (z e. upto y u. sn y <-> z < y \/ z = y)
61 elun 
z e. upto y u. sn y <-> z e. upto y \/ z e. sn y
62 60, 61 ax_mp 
(z e. upto y \/ z e. sn y <-> z < y \/ z = y) -> (z e. upto y u. sn y <-> z < y \/ z = y)
63 oreq 
(z e. upto y <-> z < y) -> (z e. sn y <-> z = y) -> (z e. upto y \/ z e. sn y <-> z < y \/ z = y)
64 elupto 
z e. upto y <-> z < y
65 63, 64 ax_mp 
(z e. sn y <-> z = y) -> (z e. upto y \/ z e. sn y <-> z < y \/ z = y)
66 elsn 
z e. sn y <-> z = y
67 65, 66 ax_mp 
z e. upto y \/ z e. sn y <-> z < y \/ z = y
68 62, 67 ax_mp 
z e. upto y u. sn y <-> z < y \/ z = y
69 59, 68 ax_mp 
z <= y <-> z e. upto y u. sn y
70 56, 69 ax_mp 
z < suc y <-> z e. upto y u. sn y
71 53, 70 ax_mp 
z e. upto (suc y) <-> z e. upto y u. sn y
72 71 eqri 
upto (suc y) == upto y u. sn y
73 uneq1 
Dom (srecaux S y) == upto y -> Dom (srecaux S y) u. sn y == upto y u. sn y
74 50, 72, 73 eqstr4g 
Dom (srecaux S y) == upto y -> Dom (srecaux S (suc y)) == upto (suc y)
75 7, 14, 21, 28, 43, 74 ind 
Dom (srecaux S n) == upto n

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)