Theorem srecpauxval ≪ | index | src | ≫ 

theorem srecpauxval (A: set) {i: nat} (n: nat):
  $ srecpaux A n = nat (n, sep (upto n) {i | srecp A i} e. A) $;
StepHypRefExpression
1 eqtr 
srecpaux A n = (\ f, nat (size (Dom f), lower {x | true (f @ x)} e. A)) @ lower ((\ i, srecpaux A i) |` upto n) ->
  (\ f, nat (size (Dom f), lower {x | true (f @ x)} e. A)) @ lower ((\ i, srecpaux A i) |` upto n) = nat (n, sep (upto n) {i | srecp A i} e. A) ->
  srecpaux A n = nat (n, sep (upto n) {i | srecp A i} e. A)
2 srecval 
srec (\ f, nat (size (Dom f), lower {x | true (f @ x)} e. A)) n =
  (\ f, nat (size (Dom f), lower {x | true (f @ x)} e. A)) @ (\. i e. upto n, srec (\ f, nat (size (Dom f), lower {x | true (f @ x)} e. A)) i)
3 2 conv rlam, srecpaux 
srecpaux A n = (\ f, nat (size (Dom f), lower {x | true (f @ x)} e. A)) @ lower ((\ i, srecpaux A i) |` upto n)
4 1, 3 ax_mp 
(\ f, nat (size (Dom f), lower {x | true (f @ x)} e. A)) @ lower ((\ i, srecpaux A i) |` upto n) = nat (n, sep (upto n) {i | srecp A i} e. A) ->
  srecpaux A n = nat (n, sep (upto n) {i | srecp A i} e. A)
5 eqtr4 
(\ f, nat (size (Dom f), lower {x | true (f @ x)} e. A)) @ lower ((\ i, srecpaux A i) |` upto n) =
    nat (n, lower {x | true (((\ i, srecpaux A i) |` upto n) @ x)} e. A) ->
  nat (n, sep (upto n) {i | srecp A i} e. A) = nat (n, lower {x | true (((\ i, srecpaux A i) |` upto n) @ x)} e. A) ->
  (\ f, nat (size (Dom f), lower {x | true (f @ x)} e. A)) @ lower ((\ i, srecpaux A i) |` upto n) = nat (n, sep (upto n) {i | srecp A i} e. A)
6 sreclem 
f = \. i e. upto n, srecpaux A i -> size (Dom f) = n
7 6 conv rlam 
f = lower ((\ i, srecpaux A i) |` upto n) -> size (Dom f) = n
8 bi2 
(f == (\ i, srecpaux A i) |` upto n <-> f = lower ((\ i, srecpaux A i) |` upto n)) ->
  f = lower ((\ i, srecpaux A i) |` upto n) ->
  f == (\ i, srecpaux A i) |` upto n
9 eqlower2 
finite ((\ i, srecpaux A i) |` upto n) -> (f == (\ i, srecpaux A i) |` upto n <-> f = lower ((\ i, srecpaux A i) |` upto n))
10 finlam 
finite (upto n) -> finite ((\ i, srecpaux A i) |` upto n)
11 finns 
finite (upto n)
12 10, 11 ax_mp 
finite ((\ i, srecpaux A i) |` upto n)
13 9, 12 ax_mp 
f == (\ i, srecpaux A i) |` upto n <-> f = lower ((\ i, srecpaux A i) |` upto n)
14 8, 13 ax_mp 
f = lower ((\ i, srecpaux A i) |` upto n) -> f == (\ i, srecpaux A i) |` upto n
15 14 appeq1d 
f = lower ((\ i, srecpaux A i) |` upto n) -> f @ x = ((\ i, srecpaux A i) |` upto n) @ x
16 15 trueeqd 
f = lower ((\ i, srecpaux A i) |` upto n) -> (true (f @ x) <-> true (((\ i, srecpaux A i) |` upto n) @ x))
17 16 abeqd 
f = lower ((\ i, srecpaux A i) |` upto n) -> {x | true (f @ x)} == {x | true (((\ i, srecpaux A i) |` upto n) @ x)}
18 17 lowereqd 
f = lower ((\ i, srecpaux A i) |` upto n) -> lower {x | true (f @ x)} = lower {x | true (((\ i, srecpaux A i) |` upto n) @ x)}
19 7, 18 preqd 
f = lower ((\ i, srecpaux A i) |` upto n) -> size (Dom f), lower {x | true (f @ x)} = n, lower {x | true (((\ i, srecpaux A i) |` upto n) @ x)}
20 19 eleq1d 
f = lower ((\ i, srecpaux A i) |` upto n) -> (size (Dom f), lower {x | true (f @ x)} e. A <-> n, lower {x | true (((\ i, srecpaux A i) |` upto n) @ x)} e. A)
21 20 nateqd 
f = lower ((\ i, srecpaux A i) |` upto n) ->
  nat (size (Dom f), lower {x | true (f @ x)} e. A) = nat (n, lower {x | true (((\ i, srecpaux A i) |` upto n) @ x)} e. A)
22 21 applame 
(\ f, nat (size (Dom f), lower {x | true (f @ x)} e. A)) @ lower ((\ i, srecpaux A i) |` upto n) =
  nat (n, lower {x | true (((\ i, srecpaux A i) |` upto n) @ x)} e. A)
23 5, 22 ax_mp 
nat (n, sep (upto n) {i | srecp A i} e. A) = nat (n, lower {x | true (((\ i, srecpaux A i) |` upto n) @ x)} e. A) ->
  (\ f, nat (size (Dom f), lower {x | true (f @ x)} e. A)) @ lower ((\ i, srecpaux A i) |` upto n) = nat (n, sep (upto n) {i | srecp A i} e. A)
24 nateq 
(n, sep (upto n) {i | srecp A i} e. A <-> n, lower {x | true (((\ i, srecpaux A i) |` upto n) @ x)} e. A) ->
  nat (n, sep (upto n) {i | srecp A i} e. A) = nat (n, lower {x | true (((\ i, srecpaux A i) |` upto n) @ x)} e. A)
25 eleq1 
n, sep (upto n) {i | srecp A i} = n, lower {x | true (((\ i, srecpaux A i) |` upto n) @ x)} ->
  (n, sep (upto n) {i | srecp A i} e. A <-> n, lower {x | true (((\ i, srecpaux A i) |` upto n) @ x)} e. A)
26 preq2 
sep (upto n) {i | srecp A i} = lower {x | true (((\ i, srecpaux A i) |` upto n) @ x)} ->
  n, sep (upto n) {i | srecp A i} = n, lower {x | true (((\ i, srecpaux A i) |` upto n) @ x)}
27 eqtr3 
lower (sep (upto n) {i | srecp A i}) = sep (upto n) {i | srecp A i} ->
  lower (sep (upto n) {i | srecp A i}) = lower {x | true (((\ i, srecpaux A i) |` upto n) @ x)} ->
  sep (upto n) {i | srecp A i} = lower {x | true (((\ i, srecpaux A i) |` upto n) @ x)}
28 lowerns 
lower (sep (upto n) {i | srecp A i}) = sep (upto n) {i | srecp A i}
29 27, 28 ax_mp 
lower (sep (upto n) {i | srecp A i}) = lower {x | true (((\ i, srecpaux A i) |` upto n) @ x)} ->
  sep (upto n) {i | srecp A i} = lower {x | true (((\ i, srecpaux A i) |` upto n) @ x)}
30 lowereq 
sep (upto n) {i | srecp A i} == {x | true (((\ i, srecpaux A i) |` upto n) @ x)} ->
  lower (sep (upto n) {i | srecp A i}) = lower {x | true (((\ i, srecpaux A i) |` upto n) @ x)}
31 bitr 
(x e. sep (upto n) {i | srecp A i} <-> x e. upto n /\ x e. {i | srecp A i}) ->
  (x e. upto n /\ x e. {i | srecp A i} <-> true (((\ i, srecpaux A i) |` upto n) @ x)) ->
  (x e. sep (upto n) {i | srecp A i} <-> true (((\ i, srecpaux A i) |` upto n) @ x))
32 elsep 
x e. sep (upto n) {i | srecp A i} <-> x e. upto n /\ x e. {i | srecp A i}
33 31, 32 ax_mp 
(x e. upto n /\ x e. {i | srecp A i} <-> true (((\ i, srecpaux A i) |` upto n) @ x)) ->
  (x e. sep (upto n) {i | srecp A i} <-> true (((\ i, srecpaux A i) |` upto n) @ x))
34 anl 
x e. upto n /\ x e. {i | srecp A i} -> x e. upto n
35 eleq2 
Dom ((\ i, srecpaux A i) |` upto n) == upto n -> (x e. Dom ((\ i, srecpaux A i) |` upto n) <-> x e. upto n)
36 dmreslam 
Dom ((\ i, srecpaux A i) |` upto n) == upto n
37 35, 36 ax_mp 
x e. Dom ((\ i, srecpaux A i) |` upto n) <-> x e. upto n
38 con1 
(~x e. Dom ((\ i, srecpaux A i) |` upto n) -> ((\ i, srecpaux A i) |` upto n) @ x = 0) ->
  ~((\ i, srecpaux A i) |` upto n) @ x = 0 ->
  x e. Dom ((\ i, srecpaux A i) |` upto n)
39 38 conv ne, true 
(~x e. Dom ((\ i, srecpaux A i) |` upto n) -> ((\ i, srecpaux A i) |` upto n) @ x = 0) ->
  true (((\ i, srecpaux A i) |` upto n) @ x) ->
  x e. Dom ((\ i, srecpaux A i) |` upto n)
40 ndmapp 
~x e. Dom ((\ i, srecpaux A i) |` upto n) -> ((\ i, srecpaux A i) |` upto n) @ x = 0
41 39, 40 ax_mp 
true (((\ i, srecpaux A i) |` upto n) @ x) -> x e. Dom ((\ i, srecpaux A i) |` upto n)
42 37, 41 sylib 
true (((\ i, srecpaux A i) |` upto n) @ x) -> x e. upto n
43 bian1 
x e. upto n -> (x e. upto n /\ x e. {i | srecp A i} <-> x e. {i | srecp A i})
44 srecpeq2 
i = x -> (srecp A i <-> srecp A x)
45 44 elabe 
x e. {i | srecp A i} <-> srecp A x
46 srecpauxeq2 
i = x -> srecpaux A i = srecpaux A x
47 46 applame 
(\ i, srecpaux A i) @ x = srecpaux A x
48 resapp 
x e. upto n -> ((\ i, srecpaux A i) |` upto n) @ x = (\ i, srecpaux A i) @ x
49 47, 48 syl6eq 
x e. upto n -> ((\ i, srecpaux A i) |` upto n) @ x = srecpaux A x
50 49 trueeqd 
x e. upto n -> (true (((\ i, srecpaux A i) |` upto n) @ x) <-> true (srecpaux A x))
51 50 conv srecp 
x e. upto n -> (true (((\ i, srecpaux A i) |` upto n) @ x) <-> srecp A x)
52 45, 51 syl6bbr 
x e. upto n -> (true (((\ i, srecpaux A i) |` upto n) @ x) <-> x e. {i | srecp A i})
53 43, 52 bitr4d 
x e. upto n -> (x e. upto n /\ x e. {i | srecp A i} <-> true (((\ i, srecpaux A i) |` upto n) @ x))
54 34, 42, 53 rbid 
x e. upto n /\ x e. {i | srecp A i} <-> true (((\ i, srecpaux A i) |` upto n) @ x)
55 33, 54 ax_mp 
x e. sep (upto n) {i | srecp A i} <-> true (((\ i, srecpaux A i) |` upto n) @ x)
56 55 eqab2i 
sep (upto n) {i | srecp A i} == {x | true (((\ i, srecpaux A i) |` upto n) @ x)}
57 30, 56 ax_mp 
lower (sep (upto n) {i | srecp A i}) = lower {x | true (((\ i, srecpaux A i) |` upto n) @ x)}
58 29, 57 ax_mp 
sep (upto n) {i | srecp A i} = lower {x | true (((\ i, srecpaux A i) |` upto n) @ x)}
59 26, 58 ax_mp 
n, sep (upto n) {i | srecp A i} = n, lower {x | true (((\ i, srecpaux A i) |` upto n) @ x)}
60 25, 59 ax_mp 
n, sep (upto n) {i | srecp A i} e. A <-> n, lower {x | true (((\ i, srecpaux A i) |` upto n) @ x)} e. A
61 24, 60 ax_mp 
nat (n, sep (upto n) {i | srecp A i} e. A) = nat (n, lower {x | true (((\ i, srecpaux A i) |` upto n) @ x)} e. A)
62 23, 61 ax_mp 
(\ f, nat (size (Dom f), lower {x | true (f @ x)} e. A)) @ lower ((\ i, srecpaux A i) |` upto n) = nat (n, sep (upto n) {i | srecp A i} e. A)
63 4, 62 ax_mp 
srecpaux A n = nat (n, sep (upto n) {i | srecp A i} e. 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)