Theorem dmsrecaux ≪ | index | src | ≫ 

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